study-lean 次回: 実数を定義するためのドキュメントリーディングから https://leanprover-github-io.translate.goog/theorem_proving_in_lean4/dependent_type_theory.html?_x_tr_sl=en&_x_tr_tl=ja&_x_tr_hl=en&_x_tr_pto=wapp#definitions 暗黙の引数のLst.consを定義するところから https://leanprover.github.io/theorem_proving_in_lean4/ 平均情報量(エントロピー)、交差エントロピー、カルバック・ライブラー情報量のwikipediaからのまとめから LEANで確率空間から sum 以前証明した何かをleanでかく exp sigma コインの裏表の期待値 probability 期待値を定義したので平均情報量から 他使えるかもしれないリンク https://leanprover.github.io/introduction_to_lean/