1.7 対数和不等式

前節で相対エントロピーの非負性を得た.次節ではもう一段進んで「相対エントロピーは粗くまとめると減る」ことを示したいのだが,その心臓部だけを先に,確率とは無関係な純粋な不等式として切り出しておく.そうしておくと,次節の証明が一行で済む.

切り出す形はこうである.非負のと正のに対し,「比をまとめてから測る」より「個別に測って足す」ほうが大きい.を「真の重み」,を「想定の重み」と思えば,前節ので総和 1 という縛りを外し,個の項に分けて述べたものにあたる.

定理 1.7.1(対数和不等式). 非負と正𝑖 =1,,𝑛)に対し,の項はのときは左辺を 0 と約束すると

(𝑖𝑎𝑖)log𝑖𝑎𝑖𝑖𝑏𝑖𝑖𝑎𝑖log𝑎𝑖𝑏𝑖.

等号は,すべての比が等しいときに限る.

これはの凸性(= 補題 1.1.8の狭義凹性)を,重みつきで述べ直したものである.情報不等式や,相対エントロピーが「まとめる」操作で減ること(次節のデータ処理不等式の心臓部)が,この一枚から従う.

なぜ「まとめると減る」に効くのかを見ておこう.左辺はたちとたちをそれぞれ足し合わせてから比を測った量,右辺はごとに比を測ってあとから足した量である.不等号の向きは,まとめたほうが小さい,すなわちの区別を捨てると差が見えにくくなることを言っている.を「写像で同じ値に潰される点たち」だと思えば,これがそのまま次節の「で粗くまとめると相対エントロピーは減る」になる.等号がすべての比が等しいときに限る,というのも符合する:潰される点たちが真の重みと想定の重みを同じ割合で持っているなら,潰しても情報は失われない.

証明. とおき,𝜆𝑖 :=𝑏𝑖/𝑏𝑖𝜆𝑖 =1𝜆𝑖 0),とする.凸関数補題 1.1.8の凹性の符号反転)に対する有限 Jensen は,補題 1.1.9に適用して符号を返したものである.これは重み・点に対し

𝜓(𝑖𝜆𝑖𝑡𝑖)𝑖𝜆𝑖𝜓(𝑡𝑖)()

を与える.両辺を具体的に計算する.重心はなので,左辺は

𝜓(𝑖𝑎𝑖𝑏)=𝑖𝑎𝑖𝑏log𝑖𝑎𝑖𝑏.

右辺は

𝑖𝜆𝑖𝜓(𝑡𝑖)=𝑖𝑏𝑖𝑏𝑎𝑖𝑏𝑖log𝑎𝑖𝑏𝑖=1𝑏𝑖𝑎𝑖log𝑎𝑖𝑏𝑖.

の両辺を倍すると,より

(𝑖𝑎𝑖)log𝑖𝑎𝑖𝑖𝑏𝑖𝑖𝑎𝑖log𝑎𝑖𝑏𝑖.

等号は補題 1.1.9 の等号条件(は狭義凸)より,正の重みをもつがすべて等しいときに限る.

形式化上の注記. 形式化されているのは不等式だけで,等号条件(すべての比が等しいこと)に対応する単独の宣言は無い.という絶対連続条件まで許す形も別に用意してある.

形式化: 不等式 log_sum_inequality (ソース),絶対連続条件を許す形log_sum_inequality_negMulLog (ソース)

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