前回の記事ではLean4での離散確率の形式化としてPMF (Probability Mass Function, 確率質量関数)について紹介し、コイントスをPMFで記述して、表や裏が出る確率が1/2であることを証明しました。
今回はコインを2回投げる試行のPMFによる記述方法を紹介し、いくつかの確率事象の確率を証明します。
最初の例はコイントスを2回行い、2回連続で同じ面が出る、という確率事象(と確率)をtwo_coins_eqという名前のPMFとして定義します。
noncomputable
def two_coins_eq : PMF (ZMod 2) :=
do
let b1 ← coin_toss
let b2 ← coin_toss
pure (b1+b2)
-- b1+b2=0 only when b1=b2
いきなり随分と見慣れないシンタックスが登場しました。大雑把にはdoの中でletと←で既存のPMFを使った試行とその結果を記述します。そしてpureの中でそれらを組み合わせた確率事象を定義します。正確にはMonadというLean4の言語機構が利用されているのですが、それはまた別の機会に説明したいと思います。
ここではdoの中で前回定義したcoin_toss : PMF(ZMod 2)を利用しています。coin_tossは確率1/2で表か裏が出る普通のコイントスです。let b1 ← coin_tossの部分でコイントスを1 回試行し、結果の表裏を表すZMod 2型の値(0 or 1)がb1に入ります。その次のlet b2 ← coin_tossでもう1回コイントスの試行を行いその結果がb2に入ります。
b1+b2はZMod 2で考えているのでb1=b2=0 or b1=b2=1の時に0になります。b1≠b2の時には1となります。このことを考慮すると、pure (b1+b2)の行で2回のコイントスの結果が同じになる(b1+b2=0)確率事象が記述できたことがわかります。
two_coins_eqというPMFはこの2回コイントスをして結果が連続で同じかどうかの確率事象からその確率への関数です。確率事象 0 (2回とも同じ面がでた）の確率はtwo_coins_eq 0、確率事象 1 (2回のコイントスで異なる面がでた) の確率はtwo_coins_eq 1とかけます。
2回とも同じ面が出る確率は1/2ということを証明して見ましょう。この証明の中で次のようなZMod 2の計算を補題として使います。
lemma sum_zmod2 {f : ZMod 2 → ENNReal} : (∑' (a : ZMod 2), f a) = (f 0) + (f 1) := by ...
証明はちょっと長いのでこの記事の最後に貼っておきます。
この補題を使うとtwo_coins_eq 0=1/2を次のように証明できます。
example : two_coins_eq 0 = 1/2 := by
rw [two_coins_eq]
simp_all [bind,sum_zmod2,coin_toss_prob,pure]
have : (0:(ZMod 2))=(1:(ZMod 2))+(1:(ZMod 2)) := by rfl
simp [this]
field_simp
詳細は説明しませんが、two_coins_eqの定義及び補題sum_zmod2, coin_toss_prob(前回証明した補題です)などを使って証明したい命題を書き換えます。field_simpの直前では証明のゴールはこんな式になっています。
⊢ 2⁻¹ * 2⁻¹ + 2⁻¹ * 2⁻¹ = 2⁻¹
最後に体の簡約計算(field_simp)で証明が終了します。
次回はコイントスを2回行った時の別の確率事象の確率を証明します。
補題sum_zmod2の証明
lemma sum_zmod2 {f : ZMod 2 → ENNReal} : (∑' (a : ZMod 2), f a) = (f 0) + (f 1) := by
rw [tsum_eq_sum (s := Finset.univ)]
rw [Finset.sum_eq_add]
· decide
· intro c hc1 hc2
simp [Finset.univ,Fintype.elems,List.finRange] at hc1
by_contra
fin_cases c
<;> simp_all
· intro h2
simp [Finset.univ,Fintype.elems,List.finRange] at h2
· intro h3
simp [Finset.univ,Fintype.elems,List.finRange] at h3
· intro b hb
simp [Finset.univ,Fintype.elems,List.finRange] at hb
fin_cases b
<;> simp_all
