Maxima で綴る数学の旅

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