事象と条件付き確率¶
Mathlib に「事象」という専用の型はありません．
事象は s : Set Ω として表し，多くの定理では MeasurableSet s を仮定します．
確率は単に測度の適用 P s です．
条件付き確率は P[s | t] と書けます．
これは条件付き測度 P[|t] を事象 s に適用したものです．
定義を展開すると，条件にしている集合 t が可測であるとき，
P[s | t] = (P t)⁻¹ * P (t ∩ s) になります．
分母が 0 の場合も，ℝ≥0∞ の逆元を使った全域的な定義として扱われます．
section Events
variable {Ω : Type*} [MeasurableSpace Ω]
variable {P : Measure Ω}
variable {s t : Set Ω}
#check MeasurableSet
#check ProbabilityTheory.cond
#check (P[|t])
#check (P[s | t])
example : P[s | t] = P[|t] s := by
rfl
example (ht : MeasurableSet t) : P[s | t] = (P t)⁻¹ * P (t ∩ s) := by
rw [cond_apply ht]
end Events
演習問題¶
条件付き確率の定義を展開してください．