1.1 エントロピー

確率変数 $𝑋$ を観測する前，その結果にはどれだけの「不確かさ」があるだろうか．あるいは観測したとき，私たちはどれだけの「情報」を得るのだろうか．エントロピーは，この素朴な問いに一つの定量的な答えを与える量である．

良い不確かさの尺度に何を期待するか，条件を並べてみよう．確実な事象（ある値を確率 1 でとる）は不確かさ 0 であってほしい．とりうる値が多く，かつそれらが均等に起こりやすいほど不確かさは大きいはずだ．そして独立な二つの実験を同時に行ったときの不確かさは，それぞれの不確かさの和であってほしい（加法性）．

この最後の要請が，式の形をほとんど決めてしまう．まず，確率 $𝑝$ で起きる一つの事象を観測したときに得られる情報の量を $𝑠 (𝑝)$ と書こう．めったに起きないことが起きたときほど驚きは大きいので $𝑠$ は減少関数で，確実に起きること（ $𝑝 = 1$ ）には驚きがないから $𝑠 (1) = 0$ である．ここに加法性を課す．独立な二つの実験で確率 $𝑝$ の事象と確率 $𝑞$ の事象が同時に起きたとき，その同時事象の確率は $𝑝 𝑞$ であり，得た情報は二つの情報の和であってほしい：

𝑠 (𝑝 𝑞) = 𝑠 (𝑝) + 𝑠 (𝑞) .

「掛け算を足し算に変える」というこの性質を持つ単調な関数は，定数倍を除いて対数しかない．これは Cauchy の関数方程式として知られる古典的な事実で，本書では証明しない（単調性は上で $𝑠$ に課した減少性がそのまま与える）．よって $𝑠 (𝑝) = - l o g 𝑝$ と書ける（ $0 < 𝑝 \leq 1$ で $- l o g 𝑝 \geq 0$ となるよう符号を選んだ．定数倍の自由度は対数の底の選び方に吸収される）．

$𝑠 (𝑝) = - l o g 𝑝$ は「その値が出たときの驚き」であって，まだ観測前の不確かさではない．観測前にわかっているのは分布だけなので，実際に出る値ごとの驚きを，その値が出る確率で平均する．これが次のエントロピーである．なお Shannon は，いま並べた三つの要請（確実な事象で 0・値が多く均等なほど大・加法性）に連続性を加えると，尺度が定数倍を除いてこの形に限ることを示した（Shannon の公理的特徴づけ）．

定義

定義 1.1.1（エントロピー）. 有限アルファベット $X$ 上に分布する離散確率変数 $𝑋$ （分布 $𝑝 (𝑥)$ ）の エントロピー を

𝐻 (𝑋) = - \sum 𝑥 \in X 𝑝 (𝑥) l o g 𝑝 (𝑥)

で定める． $𝑝 (𝑥) = 0$ の項は $𝑡 l o g 𝑡 \to 0$ （ $𝑡 ↓ 0$ ）にならい $0 l o g 0 = 0$ と約束する．

はじめに見たとおり， $- l o g 𝑝 (𝑥)$ は「 $𝑥$ が出たときの驚き」であり， $𝐻 (𝑋)$ はその驚きを $𝑋$ 自身の分布で平均した 平均驚き量 である． $\sum 𝑥 𝑝 (𝑥) \cdot (驚き)$ という形をしているだけで，新しい要素は何もない．分布が一点に集中していれば出る値は決まっていて驚きが起きず $𝐻 = 0$ ，分布が平らに広がっているほどどの値が出てもそこそこ驚くので $𝐻$ は大きくなる．後で「符号長」として読み直すこともできる．確率 $𝑝 (𝑥)$ の記号におよそ $- l o g 𝑝 (𝑥)$ 文字ぶんの符号語を割り当てるのが最適で，そのとき平均符号長がちょうど $𝐻 (𝑋)$ になる．なぜそれが最適なのかは第2章の情報源符号化定理で示す． $𝑞$ を信じて符号化する人なら，同じ読み方で払う平均符号長は $- \sum 𝑥 𝑝 (𝑥) l o g 𝑞 (𝑥)$ になる．いまは先の見通しとして聞き流してよい．

エントロピーは $𝑋$ の値そのものではなく分布 $𝑝$ のみに依存する量であることに注意したい． $𝑋$ の値を別の名前に読み替えても（たとえば目の数 $1, \dots, 6$ を色の名前に置き換えても） $𝐻 (𝑋)$ は変わらない．記号 $𝐻 (𝑋)$ は慣用だが，より正確には $𝐻 (𝑝)$ と書くべき汎関数である．

形式化上の注記. $- 𝑡 l o g 𝑡$ は Mathlib の関数 negMulLog を用いる． $0 l o g 0 = 0$ は Mathlib が $l o g 0 = 0$ と定めていることから自動的に従い，場合分けは要らない．確率変数は測度空間上の可測写像として表現し，分布 $𝑝$ は像測度を通じて与えられる．

形式化: entropy (ソース)

例

例 1.1.2（ベルヌーイ分布）. $𝑋$ が確率 $𝑝$ で $1$ ，確率 $1 - 𝑝$ で $0$ をとるとき，

𝐻 (𝑋) = - 𝑝 l o g 𝑝 - (1 - 𝑝) l o g (1 - 𝑝) = : 𝐻 𝑏 (𝑝) .

この $𝐻 𝑏$ を 二値エントロピー関数 と呼ぶ． $𝐻 𝑏 (0) = 𝐻 𝑏 (1) = 0$ （結果が確定していて不確かさがない）であり， $𝑝 = 1 / 2$ で最大値 $l o g 2$ をとる（最も予測しづらい公平なコイン）． $𝐻 𝑏$ は $[0, 1]$ 上で凹かつ $𝑝 = 1 / 2$ を軸に左右対称である．二値エントロピーは 1.10 節のファノの不等式でふたたび主役として現れる．

例 1.1.3（一様分布）. $𝑋$ が $X$ （要素数 $| X | = 𝑀$ ）上で一様，すなわち各 $𝑥$ で $𝑝 (𝑥) = 1 / 𝑀$ のとき，

𝐻 (𝑋) = - \sum 𝑥 1 𝑀 l o g 1 𝑀 = l o g 𝑀 .

どの値も等しく確率 $1 / 𝑀$ なので驚きはどれも $l o g 𝑀$ で一定であり，平均をとっても $l o g 𝑀$ のままである．底を 2 にとれば $l o g 2 𝑀$ ビットになる．これは $𝑀 = 2 𝑘$ 個の等確率な結果を区別するのに $𝑘$ ビット必要，という素朴な勘定と一致する．あとで見るように（定理 1.1.5），これは要素数 $𝑀$ のアルファベット上で達成可能なエントロピーの最大値 である．

以降，単位が要る箇所では $l o g$ の底を 2 にとり， $l o g 2 𝑀$ の値を ビット と呼ぶ．底を $1$ より大きい範囲で変えても以下のすべての等式・不等式はそのまま成り立つ（単位の名前だけが変わる）．

規模感. 公平なコイン 1 枚は $l o g 2$ （1 ビット），公平なサイコロ 1 個は $l o g 6$ （約 2.58 ビット），英字 26 文字が一様なら $l o g 26$ （約 4.70 ビット）．実際の英文は文字の出現が偏り，さらに前後の文字に依存するので，1 文字あたりの不確かさはこれよりずっと小さい．その「偏りと依存でどれだけ下がるか」を測るのが本章の残りと第3章の主題である．

性質1：非負性

命題 1.1.4. 定義 1.1.1 の設定（有限アルファベット $X$ 上の $𝑋$ ）で $𝐻 (𝑋) \geq 0$ ．等号は $𝑋$ がある一点に確率 1 で集中するときに限り成り立つ．

証明. 各 $𝑥$ について $0 \leq 𝑝 (𝑥) \leq 1$ だから $l o g 𝑝 (𝑥) \leq 0$ ，したがって $- 𝑝 (𝑥) l o g 𝑝 (𝑥) \geq 0$ ．和をとっても非負である（ $𝑝 (𝑥) = 0$ の項は約束により 0）．

等号 $𝐻 (𝑋) = 0$ は，非負項の和が 0 であることだから，すべての $𝑥$ で $- 𝑝 (𝑥) l o g 𝑝 (𝑥) = 0$ を要する． $0 < 𝑝 (𝑥) < 1$ の $𝑥$ があれば $- 𝑝 (𝑥) l o g 𝑝 (𝑥) > 0$ となり矛盾．ゆえに各 $𝑝 (𝑥)$ は $0$ または $1$ であり，総和が 1 という条件と合わせると，ちょうど一つの $𝑥$ で $𝑝 (𝑥) = 1$ ． $◼$

命題 1.1.4 は「不確かさが負になることはなく，不確かさ 0 とは結果が確定していること」という当然の事実を述べている．当然に見えるが，これは「驚きは負にならない」（ $0 \leq 𝑝 (𝑥) \leq 1$ なので $- l o g 𝑝 (𝑥) \geq 0$ ）ことの言い換えであり，平均をとる前の各項がすでに非負である，という構造から来ている．逆に $𝐻 (𝑋) = 0$ なら「どの値が出ても驚かない」＝「出る値が決まっている」ということになる．

形式化上の注記. 形式化されているのは非負性だけで，等号条件（ $𝐻 (𝑋) = 0$ と一点集中の同値）に対応する単独の宣言は無い．

形式化: 非負性 entropy_nonneg (ソース)

性質2：一様分布が最大化する（ $𝐻 (𝑋) \leq l o g | X |$ ）

定理 1.1.5. $| X | = 𝑀$ のとき $𝐻 (𝑋) \leq l o g 𝑀$ ．等号は $𝑋$ が $X$ 上で一様分布のときに限り成り立つ．

この定理は「アルファベットの大きさが不確かさの上限を決め，その上限は均等に散らばったときに達成される」という主張である．偏りは予測の手がかりであり，手がかりがあるぶんだけ不確かさは減る．だから偏りのない一様分布がいちばん予測しづらい，と読める．例 1.1.2 の二値エントロピー $𝐻 𝑏$ が $𝑝 = 1 / 2$ で最大になったのは，この定理の $𝑀 = 2$ の場合にほかならない．

これは情報理論で繰り返し使われる基本的な上界で，たとえば「 $𝑀$ 個の記号で送れる情報量は 1 記号あたり高々 $l o g 𝑀$ 」という符号化の素朴な限界を裏づける．裏返せば， $l o g 𝑀$ と実際の $𝐻 (𝑋)$ の差が「偏りのぶんだけ圧縮できる余地」であり，この差をきちんと測る量が 1.6 節で出てくる．

本書では，この定理を予備知識なしの数学的帰納法で証明する．必要な解析的事実は凹性（下に張り出さず，弦が常にグラフの下に来ること）だけで，Jensen の不等式のような道具は既知として持ち込まず，その有限版を帰納法でその場で組み立てる．

使うのは次の二つの関数についての事実で，どれも本節で証明する．

𝜑 (𝑡) = - 𝑡 l o g 𝑡 (𝑡 \geq 0, 𝜑 (0) : = 0), l o g 𝑡 (𝑡 > 0) .

証明のために微積分から二つの判定法を借りる．一つめは「開区間の上で 2 階微分が負なら，その区間で狭義凹である」，二つめは「微分可能な狭義凹関数のグラフは，接点を除いて接線より真に下にある」である．当てる相手はどちらも上の二つの関数だけで，依存するのは補題 1.1.6・補題 1.1.7・補題 1.1.8 の証明だけである．初等関数の微分の計算規則と，連続関数の積が連続であることも既知とする．対数そのものについては，底を $1$ より大きくとることと， $l o g 1 = 0$ ， $l o g 𝑠 𝑎 = 𝑎 l o g 𝑠$ （ $𝑠 > 0$ ）という定義から直ちに出る規則だけを使う．本節が借りるのはこれだけで， $l o g$ と $𝜑$ の性質はすべてそこから出す．

補題 1.1.6（対数の狭義凹性）. $l o g$ は $(0, \infty)$ の上で狭義凹である．

証明. $l o g 𝑡$ の 2 階微分は $- (l o g 𝑒) / 𝑡 2$ である．底は $1$ より大きいので $l o g 𝑒 > 0$ であり， $𝑡 > 0$ では 2 階微分が負である．借りた一つめの判定法から狭義凹性が従う． $◻$

補題 1.1.7（対数の接線不等式）. どの $𝑡 > 0$ についても

l o g 𝑡 \leq (𝑡 - 1) l o g 𝑒

が成り立ち，等号は $𝑡 = 1$ に限る．

証明. $l o g 𝑡$ の導関数は $(l o g 𝑒) / 𝑡$ だから， $𝑡 = 1$ での接線は $𝑦 = (𝑡 - 1) l o g 𝑒$ である．補題 1.1.6 と，借りた二つめの判定法（微分可能な狭義凹関数のグラフは接点を除いて接線より真に下にある）を合わせると，接点 $𝑡 = 1$ を除いて真の不等号が成り立つ． $◻$

底を $𝑒$ にとれば $l o g 𝑒 = 1$ なので右辺は $𝑡 - 1$ になるが，単位が要る箇所でとる底 $2$ では $l o g 𝑒 = 1.4426 \dots$ で，因子を落とすと不等式は偽になる（ $𝑡 = 1.5$ で $l o g 2 1.5 = 0.585 \dots > 0.5$ ）．底を $1$ より大きくとるかぎり $l o g 𝑒 > 0$ なので，この不等式に非負の重みを掛けて足すという使い方をするかぎり，因子は結論の向きを変えない．この一本は 1.6 節以降で繰り返し使う．命題 1.1.4 の証明で使った $l o g$ の符号もここから出る． $0 < 𝑡 < 1$ なら $𝑡 - 1 < 0$ と $l o g 𝑒 > 0$ から $l o g 𝑡 < 0$ である．

補題 1.1.8（ $𝜑$ の連続性と狭義凹性）. $𝜑 (𝑡) = - 𝑡 l o g 𝑡$ （ $𝑡 \geq 0$ ， $𝜑 (0) : = 0$ ）は $[0, \infty)$ の全体で連続であり， $[0, \infty)$ の上で狭義凹である（端点 $0$ を含む弦についても不等号は狭義である）．

証明. 連続性から見る． $𝑡 > 0$ では連続関数の積だから連続である． $𝑡 = 0$ での連続性を示す． $0 < 𝑡 < 1$ では補題 1.1.7 より $l o g 𝑡 \leq (𝑡 - 1) l o g 𝑒 < 0$ だから $𝜑 (𝑡) > 0$ である．補題 1.1.7 を $𝑡 - 1 / 2 > 1$ に当てると $- 12 l o g 𝑡 \leq (𝑡 - 1 / 2 - 1) l o g 𝑒 \leq 𝑡 - 1 / 2 l o g 𝑒$ であり，両辺に $2 𝑡 > 0$ を掛けて

0 < 𝜑 (𝑡) = - 𝑡 l o g 𝑡 \leq 2 \sqrt 𝑡 l o g 𝑒 (0 < 𝑡 < 1)

を得る．右辺は $𝑡 ↓ 0$ で $0$ に収束するから，挟み撃ちにより $𝜑 (𝑡) \to 0 = 𝜑 (0)$ である．

$(0, \infty)$ での狭義凹性に移る． $𝜑$ の 2 階微分は $- (l o g 𝑒) / 𝑡$ であり， $l o g 𝑒 > 0$ と $𝑡 > 0$ から負である．借りた一つめの判定法による．

端点 $0$ を含む弦に移る． $𝜑$ は $𝑡 = 0$ で微分可能でないので，この弦は判定法の外にある． $𝑏 > 0$ を固定し，弦との差 $𝑔 (𝑡) : = 𝜑 (𝑡) - 𝜑 (0) - 𝑡 (𝜑 (𝑏) - 𝜑 (0)) / 𝑏$ を $[0, 𝑏]$ の上で考える． $𝑔$ はいま示した連続性から連続で， $𝜑$ から一次式を引いただけだから $(0, 𝑏)$ で狭義凹であり， $𝑔 (0) = 𝑔 (𝑏) = 0$ である． $𝑡 \in (0, 𝑏)$ と $0 < 𝜀 < 𝑡$ に対し， $[𝜀, 𝑏]$ 上の凹性から $𝑔 (𝑡)$ は $𝑔 (𝜀)$ と $𝑔 (𝑏)$ を結ぶ線分の $𝑡$ での値以上であり，その値は $𝜀 ↓ 0$ で $0$ に収束するから， $𝑔 \geq 0$ が $[0, 𝑏]$ の全体で成り立つ．極限が保つのは広義の不等号だけなので，狭義性はここから改めて出す． $𝑐 \in (0, 𝑏)$ に対して $0 < 𝑐 1 < 𝑐 < 𝑐 2 < 𝑏$ と $𝑐 = 𝜆 𝑐 1 + (1 - 𝜆) 𝑐 2$ （ $0 < 𝜆 < 1$ ）をとれば， $𝑔$ の狭義凹性から $𝑔 (𝑐) > 𝜆 𝑔 (𝑐 1) + (1 - 𝜆) 𝑔 (𝑐 2) \geq 0$ となり，端点 $0$ を含む弦についても狭義の不等式が成り立つ． $◻$

形式化上の注記（本節の三つの補題）. 補題 1.1.6・補題 1.1.7・補題 1.1.8 に対応する単独の宣言は本書のリポジトリには無い．どれも Mathlib の宣言（Real.strictConcaveOn_log_Ioi，Real.log_le_sub_one_of_pos，Real.continuous_negMulLog，Real.strictConcaveOn_negMulLog）として在り，本書の形式化はそれを各所の証明で直接呼んでいる．

端点込みの狭義性は，定理 1.1.5 の等号条件で確率 0 の記号を排除するのに実際に効く．補題 1.1.8 の凹性を 2 点の形で書くと， $𝑎, 𝑏 \in [0, \infty)$ と $𝜆 \in [0, 1]$ に対して

𝜑 (𝜆 𝑎 + (1 - 𝜆) 𝑏) \geq 𝜆 𝜑 (𝑎) + (1 - 𝜆) 𝜑 (𝑏), (*)

であり， $𝑎 \neq 𝑏$ かつ $0 < 𝜆 < 1$ のとき不等号は狭義である．

補題 1.1.9（有限 Jensen の不等式・帰納法版）. $𝜑$ を区間 $𝐼$ 上の凹関数とする．有限個の点 $𝑡 1, \dots, 𝑡 𝑛 \in 𝐼$ と重み $𝑤 1, \dots, 𝑤 𝑛 \geq 0$ （ $\sum 𝑖 𝑤 𝑖 = 1$ ）に対して

𝑛 \sum 𝑖 = 1 𝑤 𝑖 𝜑 (𝑡 𝑖) \leq 𝜑 (𝑛 \sum 𝑖 = 1 𝑤 𝑖 𝑡 𝑖) .

さらに $𝜑$ が狭義凹なら，等号は正の重みをもつ点 $𝑡 𝑖$ がすべて互いに等しいとき，かつそのときに限る．

証明（ $𝑛$ についての数学的帰納法）. $𝑛 = 1$ のときは $𝑤 1 = 1$ なので両辺とも $𝜑 (𝑡 1)$ であり，等号が成り立って条件も自明である．

$𝑛 = 2$ のときはまさに凹性の 2 点形 $(*)$ そのものである（ $𝜆 = 𝑤 1$ ， $1 - 𝜆 = 𝑤 2$ ）．狭義凹なら $𝑡 1 \neq 𝑡 2$ かつ両重み正で狭義不等号になる．

以下， $𝑛$ 点で補題が成り立つと仮定して $𝑛 + 1$ 点を示す．重み $𝑤 1, \dots, 𝑤 𝑛 + 1 \geq 0$ （和 1）が与えられたとき，もし $𝑤 𝑛 + 1 = 1$ なら他は 0 で両辺 $𝜑 (𝑡 𝑛 + 1)$ となり成立．そうでなければ $𝑊 : = 1 - 𝑤 𝑛 + 1 = \sum 𝑛 𝑖 = 1 𝑤 𝑖 > 0$ とおき， $𝑣 𝑖 : = 𝑤 𝑖 / 𝑊$ （ $𝑖 = 1, \dots, 𝑛$ ， $\sum 𝑖 𝑣 𝑖 = 1$ ）と正規化する．内側の凸結合 $𝑠 : = \sum 𝑛 𝑖 = 1 𝑣 𝑖 𝑡 𝑖$ は $𝐼$ に属する（区間は凸結合で閉じている）．全体の重心は

𝑛 + 1 \sum 𝑖 = 1 𝑤 𝑖 𝑡 𝑖 = 𝑊 𝑠 + 𝑤 𝑛 + 1 𝑡 𝑛 + 1

と 2 点 $𝑠, 𝑡 𝑛 + 1$ の凸結合（重み $𝑊, 𝑤 𝑛 + 1$ ）に書ける．ここで 2 点凹性 $(*)$ と $𝑛$ 点への帰納法の仮定 $𝜑 (𝑠) \geq \sum 𝑛 𝑖 = 1 𝑣 𝑖 𝜑 (𝑡 𝑖)$ を順に使うと

𝜑 (𝑛 + 1 \sum 𝑖 = 1 𝑤 𝑖 𝑡 𝑖) \geq 𝑊 𝜑 (𝑠) + 𝑤 𝑛 + 1 𝜑 (𝑡 𝑛 + 1) \geq 𝑊 𝑛 \sum 𝑖 = 1 𝑣 𝑖 𝜑 (𝑡 𝑖) + 𝑤 𝑛 + 1 𝜑 (𝑡 𝑛 + 1) = 𝑛 + 1 \sum 𝑖 = 1 𝑤 𝑖 𝜑 (𝑡 𝑖),

最後の等号は $𝑊 𝑣 𝑖 = 𝑤 𝑖$ による．これで $𝑛 + 1$ 点でも不等式が成り立つ．

等号条件（狭義凹）. 上の連鎖で 2 箇所の $\geq$ がいずれも等号になるときのみ全体が等号になる．

$𝑤 𝑛 + 1 = 0$ のときは， $(*)$ の重みの一方が 0 なので第 1 の $\geq$ はつねに等号であり，条件は第 2 の不等式だけから決まる．帰納法の仮定の等号条件により，それは「正の重みをもつ $𝑡 𝑖 (𝑖 \leq 𝑛)$ が互いに等しい」（ $𝑡 𝑛 + 1$ は重み 0 なので条件に入らない）であって，主張のとおりである．

$𝑤 𝑛 + 1 > 0$ のときを見る．第 1 の $(*)$ が等号になるのは， $𝜑$ が狭義凹で両重み $𝑊, 𝑤 𝑛 + 1$ がともに正だから， $𝑠 = 𝑡 𝑛 + 1$ のとき，かつそのときに限る．第 2 の不等式が等号になるのは，帰納法の仮定により正の重みをもつ $𝑡 𝑖 (𝑖 \leq 𝑛)$ が互いに等しいとき，かつそのときに限る．後者が成り立つとき，その共通の値を $𝑐$ と書けば $𝑠 = \sum 𝑖 𝑣 𝑖 𝑡 𝑖 = 𝑐$ である（ $𝑣 𝑖$ は $𝑖 \leq 𝑛$ 上の重みで総和 1，正の重みをもつ点はすべて $𝑐$ ）．したがって前者の条件 $𝑠 = 𝑡 𝑛 + 1$ は $𝑐 = 𝑡 𝑛 + 1$ と同じことになり，二つを合わせると「正の重みをもつ点が $𝑡 𝑛 + 1$ を含めてすべて一致する」となる． $◻$

証明（定理 1.1.5）. エントロピーは定義から $𝜑$ の和である：

𝐻 (𝑋) = - \sum 𝑥 𝑝 (𝑥) l o g 𝑝 (𝑥) = \sum 𝑥 𝜑 (𝑝 (𝑥)) .

補題 1.1.9 を，重み $𝑤 𝑥 = 1 / 𝑀$ （一様），点 $𝑡 𝑥 = 𝑝 (𝑥)$ ととって適用する．各 $𝑝 (𝑥) \geq 0$ は $𝜑$ の定義域 $[0, \infty)$ に入るので，質量 0 の記号を場合分けして除く必要もない． $\sum 𝑥 (1 / 𝑀) 𝑝 (𝑥) = 1 / 𝑀$ だから

1 𝑀 \sum 𝑥 𝜑 (𝑝 (𝑥)) \leq 𝜑 (\sum 𝑥 1 𝑀 𝑝 (𝑥)) = 𝜑 (1 𝑀) = - 1 𝑀 l o g 1 𝑀 = 1 𝑀 l o g 𝑀 .

両辺を $𝑀$ 倍すれば $𝐻 (𝑋) \leq l o g 𝑀$ ．等号は $𝜑$ が狭義凹なので，補題の等号条件により，正の重み（ここではすべての $𝑥$ で $𝑤 𝑥 = 1 / 𝑀 > 0$ ）をもつ点 $𝑝 (𝑥)$ が $𝑥$ によらず一定のとき，すなわち $\sum 𝑥 𝑝 (𝑥) = 1$ と合わせて $𝑝 (𝑥) = 1 / 𝑀$ ，つまり $𝑋$ が一様分布のときに限る． $◼$

形式化上の注記（証明ルートの相違）. 本文は有限 Jensen を点の個数に関する帰納法で組み立てた．これに対し Lean の形式化 entropy_le_log_card は，Mathlib の凹関数ライブラリ（ハイポグラフの凸性と凸結合の所属に基づく ConcaveOn.le_map_sum，凹性は Real.concaveOn_negMulLog，等号条件では狭義版のReal.strictConcaveOn_negMulLog と StrictConcaveOn.map_sum_eq_iff）をそのまま呼び出す別ルートで同じ定理を証明している．最後に「全記号の質量が $1 / 𝑀$ 」から像測度の一致への橋渡しに Measure.ext_of_singleton を用いる．証明手順は本文と Lean で異なるが，結論である定理は同一であり，形式化はその正しさを無条件に保証する．底にある解析的事実が $𝜑$ の狭義凹性である点は両者で共通する．なお $𝐷 (𝑝 ‖ 一様) = l o g 𝑀 - 𝐻 (𝑋)$ という相対エントロピー経由の別証明も形式化されているが，本文の帰納法も Lean の主定理もそれには依存しない．

形式化: 主定理 entropy_le_log_card，等号条件 entropy_eq_log_card_iff (ソース)

InformationTheory — 形式化検証つき情報理論教科書（レビュー版）．数式は MathJax + AMS Euler で事前レンダリング．

1.1 エントロピー

定義

例

性質1：非負性

性質2：一様分布が最大化する（𝐻(𝑋) ≤log⁡|X|）

性質2：一様分布が最大化する（ $𝐻 (𝑋) \leq l o g | X |$ ）