今日はちょっと別件でネット検索していたらびっくりすることに気がつきました。 テレンスタオ教授（フィールズ賞受賞者、UCLA）が２週間ほど前からユーチューブを始めていて、3本の動画を投稿されています。全部、Lean4の使い方ビデオでした。 www.youtube.c…

前回はコインを2回投げる試行のPMF（確率質量関数）による記述方法を紹介し、2回とも同じ面がでる確率事象の記述の仕方と確率を証明しました。 今回は同じように2回投げる試行で2回とも表が出る確率事象の記述を行い、その確率が1/4であることを証明します。…

前回の記事ではLean4での離散確率の形式化としてPMF (Probability Mass Function, 確率質量関数)について紹介し、コイントスをPMFで記述して、表や裏が出る確率が1/2であることを証明しました。 今回はコインを2回投げる試行のPMFによる記述方法を紹介し、い…

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