Mathlib probability study note documentation
============================================

このドキュメントはMathlib4の[確率論](https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/Probability)と[測度論](https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/MeasureTheory)の内容を理解するための勉強ノートです. 基礎的な部分(特に定義)を理解することを目標にします.

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

## Filter

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

## MeasureTheory

### Outer Measure

[MeasureTheory.OuterMeasure.Defs](MeasureTheory/OuterMeasure/Defs.md) - 外測度の定義  
[MeasureTheory.OuterMeasure.AE](MeasureTheory/OuterMeasure/AE.md) - Almost everywhereの定義  
[MeasureTheory.OuterMeasure.OfFunction](MeasureTheory/OuterMeasure/OfFunction.md) - 外測度の別定義  
[MeasureTheory.OuterMeasure.Induced](MeasureTheory/OuterMeasure/Induced.md) - 外測度の可測集合への制限  

### MeasurableSpace

[MeasureTheory.MeasurableSpace.Defs](MeasureTheory/MeasurableSpace/Defs.md) - 可測空間, 可測関数の定義  
[MeasureTheory.MeasurableSpace.Basic](MeasureTheory/MeasurableSpace/Basic.md) - 可測空間の基本的な性質  

### Measure

[MeasureTheory.Measure.MeasureSpaceDef](MeasureTheory/Measure/MeasureSpaceDef.md) - 測度の定義  
[MeasureTheory.Measure.GiryMonad](MeasureTheory/Measure/GiryMonad.md) - Giry monad

### Function

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

## ProbabilityTheory

[ProbabilityTheory.ConditionalProbability](ProbabilityTheory/ConditionalProbability.md) - 条件付き確率の定義   

### Kernel

[ProbabilityTheory.Kernel.Defs](ProbabilityTheory/Kernel/Defs.md) - カーネルの定義  

### Independence

[ProbabilityTheory.Independence.Kernel](ProbabilityTheory/Independence/Kernel.md) - カーネルによる独立性の定義  
[ProbabilityTheory.Independence.Basic](ProbabilityTheory/Independence/Basic.md) - 測度から独立性の定義