Mathlib probability study note documentation

このドキュメントはMathlib4の確率論と測度論の内容を理解するための勉強ノートです. 基礎的な部分(特に定義)を理解することを目標にします.

このドキュメントの管理者は非数学科の学生であり, 数学の専門家ではありません. そのため, 数学的な誤りや不正確な表現が含まれている可能性があります. もし誤りを見つけた場合は, Issueを立てていただけると幸いです. またこのノートブックへの貢献を歓迎しています.

Filter

Filter.Defs - フィルタに関する概念
Filter.Basic - フィルタの基本的な性質
Filter.AtTopBot - フィルタの上限と下限
Filter.Topology - 位相空間におけるフィルタ

MeasureTheory

Outer Measure

MeasureTheory.OuterMeasure.Defs - 外測度の定義
MeasureTheory.OuterMeasure.AE - Almost everywhereの定義
MeasureTheory.OuterMeasure.OfFunction - 外測度の別定義
MeasureTheory.OuterMeasure.Induced - 外測度の可測集合への制限

MeasurableSpace

MeasureTheory.MeasurableSpace.Defs - 可測空間, 可測関数の定義
MeasureTheory.MeasurableSpace.Basic - 可測空間の基本的な性質

Measure

MeasureTheory.Measure.MeasureSpaceDef - 測度の定義
MeasureTheory.Measure.GiryMonad - Giry monad

Function

MeasureTheory.Function.SimpleFunc - 単関数の定義
MeasureTheory.Function.Lebesgue - lintegral
MeasureTheory.Function.HasFiniteIntegral - 絶対可積分性の定義
MeasureTheory.Function.Integrable - 可積分性の定義
MeasureTheory.Function.StronglyMeasurable - 強可測性の定義

ProbabilityTheory

ProbabilityTheory.ConditionalProbability - 条件付き確率の定義

Kernel

ProbabilityTheory.Kernel.Defs - カーネルの定義

Independence

ProbabilityTheory.Independence.Kernel - カーネルによる独立性の定義
ProbabilityTheory.Independence.Basic - 測度から独立性の定義