-数学- 確率とLean4 - Maxima で綴る数学の旅

少し事情があって?Lean4での確率の取り扱いについて勉強をしています。とは言っても決して本格的な確率論(測度論をベースにした確率密度関数や確率分布など)ではなく、算数や中学校で習うレベルの確率の話です。いわゆるコイントスの確率やサイコロの確率などです。

これらは離散的な事象の確率として確率質量関数という形でまとめられており、Lean4ではPMF (Probability Mass Function)という形で形式化されています。確率質量関数などと言われるとやはり専門用語にしか見えませんが、ようは離散的な確率事象に確率を割り当てる仕組みです。例えばコイントスでは確率事象は「表が出る」「裏が出る」の２つで、それぞれに1/2を割り当てるのが確率質量関数です。

Lean 4ではPMF(Probability Mass Functionの頭文字をとったもの)がすでに定義されています。PMFはベースとなる集合と各要素の確率を割り当てる関数で定義されます。さらにPMFであるためにはベースとなる集合は少なくとも１つ要素があり、また各要素に割り当てられた確率の総和は1である必要があります。

具体的にやってみましょう。コイントスの「裏が出る」「表が出る」を0, 1で表すことにします。0, 1はちょうどZMod 2型の元なのでZMod 2型を使うことにしてLean4でコイントスのPMFを定義するとこんな感じになります。

import Mathlib.Probability.Distributions.Uniform

noncomputable
def coin_toss : PMF (ZMod 2) :=
PMF.ofMultiset ({0, 1}:(Multiset (ZMod 2))) (by exact Ne.symm (ne_of_beq_false rfl))

PMF.ofMultisetはベースとなる(多重)集合を指定してPMFを作ります。その際にベースとなる(多重)集合が空集合でないことの証明が必要です。上記の定義ではby 以降の部分がその証明になっています。

また各要素に　1/( (多重)集合の要素の個数)　の確率を等しく割り当てる関数が自動的に生成されます。上記のコイントスの例では{0,1}のそれぞれについて1/2の確率がわりあてられます。この関数が定義できるためにベースとなる(多重)集合が空ではない必要があるのですね。

ここで定義したcoin_toss自体が確率事象から確率への関数です。確率事象としては0:(ZMod 2), 1:(ZMod 2), いずれの事象でも確率は1/2:ENNRealとなります。ENNReal型は閉区間[0, ∞]に値を取り、確率などを表現するのに使われます。

結局ZMod2型の任意の値（といっても0 or 1ですが）に対してその確率は1/2のはずです。証明して見ましょう。

lemma coin_toss_prob : ∀ g:(ZMod 2), coin_toss g = 1/2 := by
intro g -- ⊢ coin_toss g = 1 / 2
simp [coin_toss] -- ⊢ ↑(Multiset.count g (0 ::ₘ {1})) / 2 = 2⁻¹
fin_cases g <;>simp_all

2行目、3行目のコメントにそこでのゴールを示しています。3行目のゴール式の分数の分子はg (実際には0 or 1)が{0, 1}の中に現れる個数を数えています。4行目のfin_cases gでg=0の場合とg=1の場合に分けて証明を進めています。

この補題を使って、coin_toss 0=1/2, coin_toss 1=1/2を示して見ましょう。