確率空間と確率測度¶
Mathlib では，測度論の Measure Ω をそのまま使い，確率測度であることを型クラス IsProbabilityMeasure P で表します．
定義上，IsProbabilityMeasure P は P univ = 1 を主張する命題です．
ここで P s の値は ℝ≥0∞，つまり拡張非負実数です．
確率測度の場合は全体の測度が 1 なので，各事象の確率は ∞ にはなりません．
#check Measure
#check IsProbabilityMeasure
#check ProbabilityMeasure
#check measure_univ
#check measure_ne_top
#check measure_lt_top
section ProbabilitySpaces
variable {Ω : Type*} [MeasurableSpace Ω]
variable {P : Measure Ω} [IsProbabilityMeasure P]
example : P univ = 1 := by
simp
example (s : Set Ω) : P s ≤ 1 := by
exact prob_le_one
example (s : Set Ω) : P s ≠ ∞ := by
simp
example (s : Set Ω) : P s < ∞ := by
simp
example (s : Set Ω) : ℝ≥0∞ :=
P s
end ProbabilitySpaces
ProbabilityMeasure Ω という型もあります．
これは確率測度を subtype として束ねた型で，確率測度全体の空間や弱収束などを扱うときに使われます．
普通の定理を書くときは，P : Measure Ω と [IsProbabilityMeasure P] を仮定する形の方が，既存の測度論ライブラリと合わせやすいです．
標本空間に標準の測度を持たせたい場合は [MeasureSpace Ω] を使います．
この標準測度は volume で，確率論のスコープを開くと ℙ と書けます．
ただし，ℙ が確率測度であることは別に [IsProbabilityMeasure (ℙ : Measure Ω)] と仮定します．
section CanonicalMeasure
variable {Ω : Type*} [MeasureSpace Ω] [IsProbabilityMeasure (ℙ : Measure Ω)]
example : (ℙ : Measure Ω) univ = 1 := by
simp
example (s : Set Ω) : (ℙ : Measure Ω) s ≤ 1 := by
exact prob_le_one
end CanonicalMeasure
演習問題¶
確率測度では全体の測度が 1 であることを確認してください．