まとめ

Mathlib の確率論は，測度論の上に構築されています． 確率空間は Ω，MeasurableSpace Ω，P : Measure Ω，IsProbabilityMeasure P に分けて読みます． 事象は Set Ω，確率変数は可測関数，分布は P.map X，期待値は積分です．

離散確率では PMF が便利ですが，定理としては Measure と DiscreteMeasurableSpace の形で書く方が既存ライブラリと接続しやすいことがあります． 条件付き確率や条件付き分布に進むと，Markov kernel が自然に現れます． 確率論の Mathlib コードを読むときは，確率論固有の用語と測度論の語彙がどの型で対応しているかを確認してください．