1.6 情報不等式(Jensen と相対エントロピー)

ここまでに現れた不等式は三つある.一様分布がエントロピーを最大化すること(定理 1.1.5),条件付けが不確かさを増やさないこと(定理 1.2.4),相互情報量の非負性(命題 1.3.2)である.いずれもないしの凹性に補題 1.1.9 を当てる,という同じ形をしていた.これらは一つの不等式の特別な場合として束ねられる.同じアルファベット上の二つの分布に対する

𝐷(𝑝‖𝑞):=∑𝑥𝑝(𝑥)log⁡𝑝(𝑥)𝑞(𝑥)≥0

がそれで,左辺のを 相対エントロピー(KL ダイバージェンス),この不等式を情報不等式(Gibbs の不等式)と呼ぶ.相対エントロピーは「真の分布を,誤った想定で記述したときに払う符号長の超過分」と読める量で,それが負にならない(誤った想定は得をしない)というのが情報不等式の意味である.を一様分布にとれば定理 1.1.5,を同時分布・を周辺の積にとれば命題 1.3.2 が再現される.以降のデータ処理不等式・最大エントロピーもここに帰着する,本章の屋台骨である.

情報不等式

定理 1.6.1(情報不等式 / Gibbs). 同じアルファベット上の分布について.等号はのとき,かつそのときに限る.

証明. はじめに,なのにとなるがある場合を見る.そのようなでは,その項はとなって,主張は自明である(このときなので等号も成り立たない).の項はと約束し,和に寄与しない.以下,残る本質的な場合,すなわちならばである場合を考える.

補題 1.1.7 の対数不等式(等号はに限る)をに当てはめる.の各で

𝑝(𝑥)log⁡𝑞(𝑥)𝑝(𝑥)≤𝑝(𝑥)(𝑞(𝑥)𝑝(𝑥)−1)log⁡𝑒=(𝑞(𝑥)−𝑝(𝑥))log⁡𝑒.

のでは左辺は約束により 0,右辺はなので,この不等式はそのまま成り立つ.よって全にわたって和をとれて,右辺は.左辺はだから,−𝐷(𝑝 ‖ 𝑞) ≤0,すなわち.

等号は,全で項別の不等式が等号になるときに限る.の点ではすなわち,つまり.の点では左辺 0・右辺で,だから,これもである.両方を合わせてを得る.逆になら各項が 0 で.◼

補題 1.1.7 ただ一つで閉じている点に注目したい.定理 1.1.5 が 補題 1.1.8 のの凹性を使ったのに対し,こちらはの凹性の側,すなわち 補題 1.1.6 から出した接線の形を使っている.1.1 節が証明した二つの狭義凹性が,章の二本の柱にそれぞれ効いていることになる.

符号長で読む. この量は符号長として読むのがいちばん腑に落ちる.記号をとの列(符号語)に書き換えて送るとき,よく出る記号ほど短い符号語を割り当てれば,平均の長さは短くなる.第4章で示すように,記号が確率で出ると信じる人にとっての最適な割り当ては,およそ文字ぶんの符号語である.ところが実際にが出る確率はなので,この人が実際に払う平均符号長はである.真の分布を知っている人が払うとの差をとると,

−∑𝑥𝑝(𝑥)log⁡𝑞(𝑥)−(−∑𝑥𝑝(𝑥)log⁡𝑝(𝑥))=∑𝑥𝑝(𝑥)log⁡𝑝(𝑥)𝑞(𝑥)=𝐷(𝑝‖𝑞)

がちょうどになる.つまり相対エントロピーは 「だと思い込んで符号化したために余計に払う符号長」 である.情報不等式は「思い込みで得をすることはない」,等号条件は「損をしないのは正しく知っていたときだけ」と読める.

距離ではない. 「隔たり」と呼んでいるがは距離ではない.一般にとは一致せず(図 1.6.1),三角不等式も一般には成り立たない.上の符号長の読みからすると当然で,「が真でと思い込む」損と「が真でと思い込む」損は別物である.とくにが 0 をとる点でが正の値をとるとになる:起こらないと決めつけていたことが実際に起きると,その符号語には長さが割り当てられていない.

図 1.6.1. をの二値分布に固定し,をの二値分布として動かしたときのと.どちらもでになる.

すでに見た不等式の再確認. を一様分布にとるととなり,がそのまま定理 1.1.5(𝐻 ≤log⁡𝑀)である.また,とおくとは定義 1.3.1 の相互情報量そのものなので,命題 1.3.2 の非負性が再現される.別々に証明した不等式が一つの根に束ねられたことになる.

形式化: 一様分布との関係 klDiv_uniformOn_univ_toReal_eq (ソース)

形式化: 非負性 klDivPmf_nonneg (ソース),等号条件klDivPmf_eq_zero_iff_pmf (ソース)

注記

本ライブラリは確率質量関数(pmf)形に対して非負性を独立に形式化している.測度論版のは 1.3 節で述べたとおり,拡張非負実数値であることからほぼ型レベルで従う別ルートで得る.

この実数値の pmf 形は,参照分布が 0 をとる点でも有限値を返すので,本文の証明が最初に扱った「値が正の無限大になる」場合を表していない.無限大を含む形は測度論版の相対エントロピーの側にある.

等号条件の形式化は,参照分布が全点で正である場合に限って述べてある(本文の主張はこの限定を必要としない).

情報理論入門(Lean による形式証明つき)・GitHub