7.5 連続な相対エントロピーと相互情報量

7.3 節で見たとおり，微分エントロピーの数値そのものは目盛の取り方で動く．意味をもつのは同じ目盛で測った量の差である．第1章で相対エントロピー $𝐷 (𝑝 ‖ 𝑞)$ と相互情報量 $𝐼 (𝑋; 𝑌)$ を導入したとき，どちらも二つの分布の比の対数を平均する形をしていた（1.6 節と定義 1.3.1）．比の形は，分母と分子に同じ係数がかかる取り替えを見なくなる．本節はこの二つの量を密度で書き直し，離散のときと同じ性質が成り立つことを見る．

書き直したあとの相対エントロピーは，補題 7.2.3 が示した「 $ℎ (𝑋)$ と $- \int 𝑓 l o g 𝑞$ の差」にほかならない．したがって非負性はすでに手元にある．新しく要るのは定義と，離散のときの読み方がそのまま通ることの確認である．

相対エントロピー

定義 7.5.1（相対エントロピー）. $𝑛 \geq 1$ とし， $𝑓$ と $𝑞$ を $ℝ 𝑛$ 上の密度とする． $𝑆 : = {𝑥 \in ℝ 𝑛 : 𝑓 (𝑥) > 0 かつ 𝑞 (𝑥) > 0}$ とおく． $\int 𝑆 𝑓 (𝑥) 𝑑 𝑥 = 1$ であり $\int 𝑆 𝑓 (𝑥) ∣ l o g 𝑓 (𝑥) 𝑞 (𝑥) ∣ 𝑑 𝑥 < \infty$ であるとき， $𝑓$ の $𝑞$ に対する 相対エントロピー を

𝐷 (𝑓 ‖ 𝑞) : = \int 𝑆 𝑓 (𝑥) l o g 𝑓 (𝑥) 𝑞 (𝑥) 𝑑 𝑥

で定め，このとき $𝐷 (𝑓 ‖ 𝑞)$ が 定まる という．

形式化上の注記（本節共通）

形式化の相対エントロピーは，密度ではなく分布に対して定義されていて，値は非負の拡張実数として返る．本文の $𝐷 (𝑓 ‖ 𝑞)$ にあたるのは，それを実数に直したものである．本節が相対エントロピーとして紐付ける宣言と，注記で触れる相対エントロピーの宣言は，どれもこの形をしている．注記にはほかに微分エントロピーの側で書かれた実数値の宣言も出てくるが，そちらは相対エントロピーではない．

$\int 𝑆 𝑓 = 1$ という条件は， $𝑞$ が $0$ になる点に $𝑓$ が確率を置いていない，ということである．離散のときはその場合に $𝐷 (𝑝 ‖ 𝑞) = + \infty$ と読んだ（1.6 節）が，本書は密度についてその場合の $𝐷$ を定めない． $+ \infty$ を値として認めると，以下の主張がどれも「両辺が有限なら」という但し書きを抱えることになり，得るものより手間のほうが大きいからである． $𝑞$ を「起こらないと決めつけた想定」と読むなら，決めつけが外れたときの罰が無限大になるという事情は離散のときと同じである．定めない場合は実際にある．例 7.2.6 の二つの分布を逆向きにとって， $𝑓$ をガウス分布の密度， $𝑞$ を同じ分散をもつ一様分布の密度にすると，区間の外では $𝑞 = 0$ なのに $𝑓 > 0$ だから $\int 𝑆 𝑓 < 1$ であり， $𝐷 (𝑓 ‖ 𝑞)$ は定まらない．

定理 7.5.2（情報不等式（連続版））. $𝑛 \geq 1$ とし， $𝑋$ を $ℝ 𝑛$ に値をとり密度 $𝑓$ をもつ確率変数， $𝑞$ を $ℝ 𝑛$ 上の密度とし， $𝑆$ を定義 7.5.1 のとおりとする． $\int 𝑆 𝑓 (𝑥) 𝑑 𝑥 = 1$ であり， $ℎ (𝑋)$ が定まり， $\int 𝑆 𝑓 (𝑥) | l o g 𝑞 (𝑥) | 𝑑 𝑥 < \infty$ であるならば， $𝐷 (𝑓 ‖ 𝑞)$ は定まり

𝐷 (𝑓 ‖ 𝑞) = - ℎ (𝑋) - \int 𝑆 𝑓 (𝑥) l o g 𝑞 (𝑥) 𝑑 𝑥 \geq 0

である．

第 1 項を $- ℎ (𝑋)$ に直す．本定理の仮定は補題 7.2.3 の仮定そのものだから，補題 7.2.3 の証明と同じく，7.2 節で借りた零集合の上での積分により $\int 𝑆 𝑓 l o g 𝑓 = \int ℝ 𝑛 𝑓 l o g 𝑓 = - ℎ (𝑋)$ である．よって等式が従う．

非負性も補題 7.2.3 から出る．同じ仮定のもとで $ℎ (𝑋) \leq - \int 𝑆 𝑓 l o g 𝑞$ が成り立ち，移項すれば右辺が $0$ 以上であることがわかる． $◼$

形式化上の注記

定理 7.5.2 は $𝑛 = 1$ の場合だけ，等式と非負性のそれぞれに単独の宣言がある．等式は klDiv_toReal_eq_neg_differentialEntropy_sub_cross (InformationTheory/Shannon/EPI/G2/BridgeDensityHelpers.lean) で，仮定は本文と対応している．二つの分布が Lebesgue 測度について絶対連続であることが「 $𝑋$ が密度 $𝑓$ をもつ」と「 $𝑞$ が密度である」に， $𝑋$ の分布が比べる相手の分布について絶対連続であることが $\int 𝑆 𝑓 = 1$ に，密度とその対数の積が積分できることが「 $ℎ (𝑋)$ が定まる」に，密度と比べる相手の対数密度の積が積分できることが $\int 𝑆 𝑓 | l o g 𝑞 | < \infty$ にあたる．非負性は，補題 7.2.3 に触れた differentialEntropy_le_cross_entropy がそのまま与える．一般の $𝑛$ については，どちらにも対応する単独の宣言がない．

定理 7.5.2 は，離散の情報不等式（定理 1.6.1）を密度で書き直したものである．離散のときは $- \sum 𝑥 𝑝 (𝑥) l o g 𝑞 (𝑥)$ と $𝐻 (𝑝)$ をそれぞれ平均符号長として読めたが，連続では $- \int 𝑆 𝑓 l o g 𝑞$ も $ℎ (𝑋)$ も負になりうる（例 7.1.3）ので，その読み方は個々の項には当てられない．当てられるのは差のほうで， $𝐷 (𝑓 ‖ 𝑞)$ が「密度が $𝑞$ だと思い込んだために余計に払うぶん」にあたる．思い込みで得はしない，という主張になっている．離散のときに述べた等号条件（ $𝑝 = 𝑞$ のとき，かつそのときに限る）にあたるものを，本書は密度について述べない．定理 7.2.4 の等号のときと同じ理由で，密度どうしの一致は確率 $0$ の集合の上での食い違いを許す形でしか言えないからである．

形式化上の注記

本書が述べないだけで，等号条件そのものは分布のレベルで機械検証されている．Mathlib の klDiv_eq_zero_iff がそれで，第1章 1.3 節は相互情報量の等号条件をこれに寄りかからせている．

命題 7.5.3（目盛の取り替えでの不変性）. $𝑛 \geq 1$ とし， $𝑓$ と $𝑞$ を $ℝ 𝑛$ 上の密度， $𝑐 1, \dots, 𝑐 𝑛$ を $0$ でない実数， $𝑏 1, \dots, 𝑏 𝑛$ を実数とし

𝑓 * (𝑥) : = 1 | 𝑐 1 \dots 𝑐 𝑛 | 𝑓 (𝑥 1 - 𝑏 1 𝑐 1, \dots, 𝑥 𝑛 - 𝑏 𝑛 𝑐 𝑛), 𝑞 * (𝑥) : = 1 | 𝑐 1 \dots 𝑐 𝑛 | 𝑞 (𝑥 1 - 𝑏 1 𝑐 1, \dots, 𝑥 𝑛 - 𝑏 𝑛 𝑐 𝑛)

とおく． $𝐷 (𝑓 ‖ 𝑞)$ が定まるならば $𝐷 (𝑓 * ‖ 𝑞 *)$ も定まり， $𝐷 (𝑓 * ‖ 𝑞 *) = 𝐷 (𝑓 ‖ 𝑞)$ である．

証明. 以下， $𝑥 \in ℝ 𝑛$ に対して $𝑦 : = (𝑥 1 - 𝑏 1 𝑐 1, \dots, 𝑥 𝑛 - 𝑏 𝑛 𝑐 𝑛)$ と書き，7.3 節で借りた置換積分をこの置き換えで使う．

$𝑓 *$ と $𝑞 *$ が $ℝ 𝑛$ 上の密度であることを見る．どちらも非負であり，置換積分より $\int ℝ 𝑛 𝑓 * (𝑥) 𝑑 𝑥 = \int ℝ 𝑛 𝑓 (𝑦) 𝑑 𝑦 = 1$ となり， $𝑞 *$ についても同じ計算である． $𝑓 * (𝑥) > 0$ と $𝑓 (𝑦) > 0$ は同値， $𝑞 *$ についても同様だから，定義 7.5.1 の集合は $𝑆 * = {𝑥 \in ℝ 𝑛 : 𝑦 \in 𝑆}$ である．また $𝑆 *$ の上で

l o g 𝑓 * (𝑥) 𝑞 * (𝑥) = l o g 𝑓 (𝑦) 𝑞 (𝑦)

であり， $1 / | 𝑐 1 \dots 𝑐 𝑛 |$ は分母と分子で打ち消し合う．置換積分により積分域 $𝑆 *$ は $𝑆$ に移り， $𝑑 𝑥 = | 𝑐 1 \dots 𝑐 𝑛 | 𝑑 𝑦$ だから

\int 𝑆 * 𝑓 * (𝑥) ∣ l o g 𝑓 * (𝑥) 𝑞 * (𝑥) ∣ 𝑑 𝑥 = \int 𝑆 𝑓 (𝑦) ∣ l o g 𝑓 (𝑦) 𝑞 (𝑦) ∣ 𝑑 𝑦

であり，同じ置き換えで $\int 𝑆 * 𝑓 * = \int 𝑆 𝑓 = 1$ である．よって $𝐷 (𝑓 * ‖ 𝑞 *)$ は定まり，絶対値を外した同じ計算でその値が $𝐷 (𝑓 ‖ 𝑞)$ に等しいことがわかる． $◼$

形式化上の注記

命題 7.5.3 にあたる単独の宣言はない．より一般に，可測な同型で二つの分布を同時に送っても相対エントロピーが変わらないことが klDiv_map_measurableEquiv (InformationTheory/Shannon/MutualInfo.lean) として形式化されていて，本文の主張は，各成分に $𝑡 \mapsto 𝑐 𝑖 𝑡 + 𝑏 𝑖$ を当てる写像をその同型にとった場合にあたる．結論が分布について述べられているので，密度で書いた命題 7.5.3 とそのまま重なりはしない．

命題 7.5.3 が，本節の量が微分エントロピーと違うところである． $𝑛 = 1$ で見ると， $ℎ$ は引き伸ばしで $l o g | 𝑐 |$ だけ動いた（命題 7.3.3）のに対し， $𝐷$ は動かない．比べる二つの密度に同じ変換をかければ，比が変わらないからである．目盛を変えても意味が変わらないので， $𝐷$ の値はそれ自体で読んでよい量になっている．

相互情報量

定義 7.5.4（相互情報量）. $𝑋$ と $𝑌$ を実数値確率変数とし， $(𝑋, 𝑌)$ が結合密度 $𝑓$ をもつとする．定義 7.4.1 を $𝑓$ に当てて得られる $𝑋$ と $𝑌$ の周辺密度を $𝑓 1$ ， $𝑓 2$ ，その積を $𝑞 (𝑥, 𝑦) : = 𝑓 1 (𝑥) 𝑓 2 (𝑦)$ とする（補題 7.4.2 より $𝑞$ は $ℝ 2$ 上の密度である）． $𝐷 (𝑓 ‖ 𝑞)$ が定まるとき， $𝑋$ と $𝑌$ の 相互情報量 を

𝐼 (𝑋; 𝑌) : = 𝐷 (𝑓 ‖ 𝑞)

で定める．

離散のときの定義 1.3.1 は，相互情報量を「同時分布と周辺分布の積との隔たり」として読めるものだった（1.6 節）．定義 7.5.4 はその読み方をそのまま定義に据えている．なお $ℎ$ のときと同じく， $𝐷 (𝑓 ‖ 𝑞)$ と $𝐼 (𝑋; 𝑌)$ の値も密度の選び方によらない．これも測度論を使って示される事実で，本書では証明しない．

形式化: mutualInfo (ソース)

注記

mutualInfo は結合分布と周辺分布の積との相対エントロピーとして定義されていて，定義 7.5.4 と同じ形をしている．第1章 1.3 節が定義 1.3.1 をこれに紐付けているとおり，離散と連続で別の宣言になっているわけではない．ただし，以下で定理 7.5.6 について触れる等式の宣言は mutualInfo を経由せず，相対エントロピーを直に書いたものである．値は一致するが，宣言としては別である．

独立なときの値を先に見ておく．

命題 7.5.5（独立なときの相互情報量）. $𝑋$ と $𝑌$ を独立な実数値確率変数とし，どちらも密度をもつとする．このとき $(𝑋, 𝑌)$ は結合密度をもち， $𝐼 (𝑋; 𝑌)$ は定まって $𝐼 (𝑋; 𝑌) = 0$ である．

証明. $𝑓 1$ ， $𝑓 2$ を $𝑋$ ， $𝑌$ の密度とする．7.4 節で借りた独立と積の密度により $𝑞 (𝑥, 𝑦) : = 𝑓 1 (𝑥) 𝑓 2 (𝑦)$ は $(𝑋, 𝑌)$ の結合密度であり， $𝑓 1$ と $𝑓 2$ はその周辺密度でもある．結合密度としてこの $𝑞$ をとれば，定義 7.5.4 の $𝑓$ も $𝑞$ に等しい．どちらも同じ関数だから $𝑆 = {𝑞 > 0}$ で $\int 𝑆 𝑞 = 1$ であり， $𝑆$ の上で $l o g 𝑞 𝑞 = 0$ だから， $𝐷 (𝑞 ‖ 𝑞)$ は定まって $0$ である． $◼$

形式化上の注記

命題 7.5.5 にあたる単独の宣言はない．分布のレベルでは，独立との同値 mutualInfo_eq_zero_iff_indep (InformationTheory/Shannon/MutualInfo.lean) が可測性だけを仮定して「独立であることと相互情報量が $0$ であることとは同値である」を与えており，第1章 1.3 節はこれに命題 1.3.2 の等号条件を紐付けている．命題 7.5.5 が同時に述べている「 $(𝑋, 𝑌)$ が結合密度をもつ」と「 $𝐼 (𝑋; 𝑌)$ が定まる」にあたる部分は，この宣言には含まれていない．

定理 7.5.6（相互情報量とエントロピーの関係）. $𝑋$ と $𝑌$ を実数値確率変数とし， $(𝑋, 𝑌)$ が結合密度をもつとする． $ℎ (𝑋, 𝑌)$ が定まり， $ℎ (𝑋)$ と $ℎ (𝑌)$ が定まるならば， $𝐼 (𝑋; 𝑌)$ は定まり

𝐼 (𝑋; 𝑌) = ℎ (𝑋) + ℎ (𝑌) - ℎ (𝑋, 𝑌) \geq 0

である．

証明. $𝑓$ を結合密度とし， $𝑓 1$ ， $𝑓 2$ ， $𝑞$ ， $𝑆$ を補題 7.4.2 の $𝑛 = 2$ の場合のとおりにとる．補題 7.4.2 より $𝑞$ は $ℝ 2$ 上の密度で， $\int 𝑆 𝑓 = 1$ と $\int 𝑆 𝑓 | l o g 𝑞 | < \infty$ が成り立つ．よって定理 7.5.2 の仮定が満たされ， $𝐷 (𝑓 ‖ 𝑞)$ すなわち $𝐼 (𝑋; 𝑌)$ は定まって

𝐼 (𝑋; 𝑌) = - ℎ (𝑋, 𝑌) - \int 𝑆 𝑓 l o g 𝑞 \geq 0

である．補題 7.4.2 より $- \int 𝑆 𝑓 l o g 𝑞 = ℎ (𝑋) + ℎ (𝑌)$ だから，主張を得る． $◼$

形式化上の注記

定理 7.5.6 の等式にあたるのは klDiv_prod_marginals_toReal_eq_sum_sub_joint で， $𝑛$ 個の確率変数についての形は klDiv_pi_marginals_toReal_eq_sum_sub_joint (InformationTheory/Shannon/MultivariateDiffEntropy.lean) である．定理 7.4.3 のときと同じく，どちらも結合分布が周辺分布の積について絶対連続であることを仮定にもち，これは本文では補題 7.4.2 の結論なので，宣言は本文の主張をそのまま証明してはいない．残る仮定は $2$ 変数の側と $𝑛$ 変数の側で違う． $2$ 変数の側は，二つの周辺分布が Lebesgue 測度について絶対連続であること（借りた周辺密度の存在にあたる）と，五つの対数密度が積分できること（本文の三つの「定まる」にあたる）を仮定し，結合分布が Lebesgue 測度について絶対連続であることは仮定にもたない． $𝑛$ 変数の側は，各周辺分布についての同じ絶対連続性に加えて結合分布のそれも仮定し，対数密度の積分可能性のほうは，結合分布についてのものと各成分の周辺密度についてのものの二つにまとめられている．非負性の側には単独の宣言があって，mutualInfo_nonneg (InformationTheory/Shannon/MutualInfo.lean) がそれである．第1章 1.3 節が命題 1.3.2 をこれに紐付けており，実数で書いた形は定理 7.4.3 に触れた jointDifferentialEntropy_le_sum が与える．

定理 7.5.6 は，離散のときのエントロピー表現 $𝐼 (𝑋; 𝑌) = 𝐻 (𝑋) + 𝐻 (𝑌) - 𝐻 (𝑋, 𝑌)$ （定理 1.3.4）と同じ形をしている．離散のエントロピーと微分エントロピーは別物だったのに，それを組み合わせた相互情報量は同じ式で書ける．右辺が三つの差でできていて，微分エントロピーの数値そのものが表に出ないからである．7.1 節の終わりに予告した「差だけが現れる」というのは，このことである．

定理 7.4.3 との関係も読める． $𝑛 = 2$ の場合の劣加法性 $ℎ (𝑋, 𝑌) \leq ℎ (𝑋) + ℎ (𝑌)$ は，定理 7.5.6 の $𝐼 (𝑋; 𝑌) \geq 0$ を移項したものにほかならない．離散のときに 1.6 節で情報不等式が既出の不等式を束ねたのと同じことが，ここでも起きている．例 7.4.5 の三角形の上の一様分布では $𝐼 (𝑋; 𝑌) = l o g 𝑒 2$ で，底を $2$ にとれば約 $0.4427$ ビットである． $𝑋$ と $𝑌$ の依存の強さが，それだけあるということである．

7.3 節が残した問いにも，ここで答えが付く．微分エントロピーの数値は目盛の取り替えで動いたが，相互情報量は動かない．

系 7.5.7（目盛の取り替えでの相互情報量の不変性）. $𝑋$ と $𝑌$ を実数値確率変数とし， $(𝑋, 𝑌)$ が結合密度をもち $𝐼 (𝑋; 𝑌)$ が定まるとする． $𝑐$ と $𝑐'$ を $0$ でない実数， $𝑏$ と $𝑏'$ を実数とすると， $𝐼 (𝑐 𝑋 + 𝑏; 𝑐' 𝑌 + 𝑏')$ は定まって $𝐼 (𝑋; 𝑌)$ に等しい．

証明. $𝑓$ を $(𝑋, 𝑌)$ の結合密度， $𝑓 1$ ， $𝑓 2$ を定義 7.4.1 の周辺密度， $𝑞 (𝑥, 𝑦) : = 𝑓 1 (𝑥) 𝑓 2 (𝑦)$ とする．補題 7.4.2 より $𝑞$ は $ℝ 2$ 上の密度であり，定義 7.5.4 より $𝐷 (𝑓 ‖ 𝑞) = 𝐼 (𝑋; 𝑌)$ は定まっている．命題 7.5.3 を $𝑛 = 2$ ， $(𝑐 1, 𝑐 2) : = (𝑐, 𝑐')$ ， $(𝑏 1, 𝑏 2) : = (𝑏, 𝑏')$ ととって読み，そこで作られる密度を $𝑓 *$ ， $𝑞 *$ とする．

$𝑓 *$ が $(𝑐 𝑋 + 𝑏, 𝑐' 𝑌 + 𝑏')$ の結合密度であることを見る．任意の直方体 $𝑅$ について， $(𝑐 𝑋 + 𝑏, 𝑐' 𝑌 + 𝑏')$ が $𝑅$ に入ることと， $(𝑋, 𝑌)$ が $𝑅$ の二つの辺を $𝑡 \mapsto (𝑡 - 𝑏) / 𝑐$ と $𝑡 \mapsto (𝑡 - 𝑏') / 𝑐'$ で送った直方体に入ることとは同値である．定義 7.1.1 をその直方体に当て，7.3 節で借りた置換積分を $𝑦 1 = (𝑥 1 - 𝑏) / 𝑐$ ， $𝑦 2 = (𝑥 2 - 𝑏') / 𝑐'$ で使うと， $P r [(𝑐 𝑋 + 𝑏, 𝑐' 𝑌 + 𝑏') \in 𝑅] = \int 𝑅 𝑓 * (𝑥) 𝑑 𝑥$ を得る． $𝑓 *$ は非負で，同じ置き換えにより $\int ℝ 2 𝑓 * = \int ℝ 2 𝑓 = 1$ だから $ℝ 2$ 上の密度であり，したがって定義 7.1.1 の意味の結合密度である．

$𝑓 *$ の周辺密度を求める．定義 7.4.1 の積分で，第 $1$ 周辺密度については第 $2$ 変数について，第 $2$ 周辺密度については第 $1$ 変数について，借りた置換積分を使うと，前者は $𝑥 \mapsto 1 | 𝑐 | 𝑓 1 (𝑥 - 𝑏 𝑐)$ ，後者は $𝑥 \mapsto 1 | 𝑐' | 𝑓 2 (𝑥 - 𝑏' 𝑐')$ である．この二つの積は $𝑞 *$ にほかならない．

よって定義 7.5.4 より $𝐼 (𝑐 𝑋 + 𝑏; 𝑐' 𝑌 + 𝑏') = 𝐷 (𝑓 * ‖ 𝑞 *)$ であり，命題 7.5.3 よりこれは定まって $𝐷 (𝑓 ‖ 𝑞) = 𝐼 (𝑋; 𝑌)$ に等しい． $◼$

$𝑋$ と $𝑌$ を別々の目盛で測り直しても，二つのあいだの依存の強さは変わらないということである．

例 7.5.8（二つのガウス分布の相対エントロピー）. $𝜇 1$ ， $𝜇 2$ を実数， $𝜎 21, 𝜎 22 > 0$ とし， $𝑓$ を $N (𝜇 1, 𝜎 21)$ の密度， $𝑞$ を $N (𝜇 2, 𝜎 22)$ の密度とする（定義 7.2.1）．このとき $𝐷 (𝑓 ‖ 𝑞)$ は定まり

𝐷 (𝑓 ‖ 𝑞) = 12 l o g 𝜎 22 𝜎 21 + l o g 𝑒 2 (𝜎 21 + (𝜇 1 - 𝜇 2) 2 𝜎 22 - 1)

である．

証明. $𝑋$ が $N (𝜇 1, 𝜎 21)$ に従うとする．どちらの密度も実軸のすべての点で正だから定義 7.5.1 の $𝑆$ は $ℝ$ 全体で， $\int 𝑆 𝑓 = 1$ である．定義 7.2.1 の二つの密度について対数の差をとると

l o g 𝑓 (𝑥) 𝑞 (𝑥) = 12 l o g 𝜎 22 𝜎 21 + l o g 𝑒 ((𝑥 - 𝜇 2) 2 2 𝜎 22 - (𝑥 - 𝜇 1) 2 2 𝜎 21)

である．右辺は $𝑥$ の $2$ 次式で，借りたガウス分布の基本性質より $𝔼 [𝑋] = 𝜇 1$ と $𝔼 [(𝑋 - 𝜇 1) 2] = 𝜎 21$ はどちらも有限だから， $𝑓$ を掛けた積分は絶対収束し $𝐷 (𝑓 ‖ 𝑞)$ は定まる．

平均をとる． $𝔼 [(𝑋 - 𝜇 1) 2] = 𝜎 21$ であり， $(𝑋 - 𝜇 2) 2 = (𝑋 - 𝜇 1) 2 + 2 (𝜇 1 - 𝜇 2) (𝑋 - 𝜇 1) + (𝜇 1 - 𝜇 2) 2$ の平均をとると $𝔼 [𝑋 - 𝜇 1] = 0$ より $𝔼 [(𝑋 - 𝜇 2) 2] = 𝜎 21 + (𝜇 1 - 𝜇 2) 2$ である．よって

𝐷 (𝑓 ‖ 𝑞) = 12 l o g 𝜎 22 𝜎 21 + l o g 𝑒 (𝜎 21 + (𝜇 1 - 𝜇 2) 2 2 𝜎 22 - 𝜎 21 2 𝜎 21)

となり，右辺は主張の式である． $◼$

形式化上の注記

例 7.5.8 の値は klDiv_gaussianReal_gaussianReal_eq (InformationTheory/Shannon/DifferentialEntropy.lean) が与える．ただしこの宣言が述べているのは，非負の拡張実数として定義された相対エントロピーを実数に直した値だけで，例 7.5.8 のもう一方の主張である「 $𝐷 (𝑓 ‖ 𝑞)$ が定まる」にあたる有限性は結論に含まれていない．そのため，例 7.5.8 をそのまま証明する単独の宣言にはなっていない．

両端で確かめる. $𝜎 21 = 𝜎 22 = 𝜎 2$ のとき，例 7.5.8 の式は $l o g 𝑒 2 \cdot (𝜇 1 - 𝜇 2) 2 𝜎 2$ になる．平均が離れているほど大きく，二つの密度が同じもの（ $𝜇 1 = 𝜇 2$ ）になったところで $0$ である．定理 7.5.2 の非負性と整合している．

距離ではない. 離散のときに 1.6 節で見たのと同じく， $𝐷 (𝑓 ‖ 𝑞)$ と $𝐷 (𝑞 ‖ 𝑓)$ は一致しない． $N (0, 1)$ と $N (0, 4)$ で例 7.5.8 の式を両向きに計算すると，底を $2$ にとって前者から後者への隔たりが約 $0.4590$ ビット，後者から前者への隔たりが約 $1.1640$ ビットである．狭い分布を広い分布だと思い込む損と，広い分布を狭い分布だと思い込む損は，別物だということである．

ガウス通信路の章は，本章で組み立てた量を通信路に当てる．雑音がガウス分布に従い，送る信号の電力に制約のかかる通信路では，容量が本節の相互情報量の最大値として書け，その最大を決めるのが定理 7.2.4 の最大エントロピー性である．本章が条件付き微分エントロピーを用意しなかったぶんは，そこで補うことになる．

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