前回はコインを2回投げる試行のPMF（確率質量関数）による記述方法を紹介し、2回とも同じ面がでる確率事象の記述の仕方と確率を証明しました。
今回は同じように2回投げる試行で2回とも表が出る確率事象の記述を行い、その確率が1/4であることを証明します。
noncomputable
def two_coins_one_one : PMF (ZMod 2) :=
do
let b1 ← coin_toss
let b2 ← coin_toss
pure (b1*b2)
-- b1*b2=1 only when b1=1 and b2=1
この場合にはpureの引数にはZMod 2型の積を使ってb1*b2としています。コメントにもあるようにb1*b2=1となるのはb1=b2=1（どちらも表）の場合だけです。どちらかが0ならば積は0になります。
これで確率事象を記述できました。どちらも表の確率は1/4ですが、その証明を行いましょう。
noncomputable
example : two_coins_one_one 1 = 1/4 := by
rw [two_coins_one_one]
simp_all [bind,sum_zmod2,coin_toss_prob,pure]
refine ENNReal.eq_inv_of_mul_eq_one_left ?_
have : (4:ENNReal)=(2:ENNReal)*(2:ENNReal) := by ring_nf
rw [this]
rw [mul_comm,mul_assoc,ENNReal.mul_inv_cancel_left,ENNReal.mul_inv_cancel]
<;>norm_num
証明の方法は前回と大差ありません。まず記述したPMFを使って証明したい命題を書き換えます。bindを使ってモナドの記述を関数呼び出しに書き換えます。さらに総和を書き換え、1回のコイントスで表が出る確率は1/2である、という補題を使い、煎じ詰めます。simp_allの行とrefineの行の間でゴールはこのようになります。
2⁻¹ * 2⁻¹ * 4 = 1
この段階では確率や確率質量関数やモナドなどの知識は使い終わっていて、ただの計算式の証明が残っているだけです。この式がReal型ならおそらくnorm_numタクティク一発で終わるのですが、ENNReal型という０以上無限大以下の実数の型です。そのため既存の道具立てが弱いので補って証明を進めます。
4=2*2を補題として使うとゴールが
⊢ 2⁻¹ * 2⁻¹ * (2 * 2) = 1
になります。ENNReal型では「その値が無限大でなければ」割り算と掛け算の簡約ができます。この場合、2⁻¹ * 2=1のような計算を進めた場合あとで2 ≠ ⊤を別途証明しなければなりません。それが最後の行の<;>norm_numで行われています。
今回の確率のお話はここまでです。
