16.7 エントロピーべきと Fisher 情報量

本節からは第7章の微分エントロピーの上に乗る．微分エントロピー $ℎ (𝑋)$ （定義 7.1.2）は目盛の取り替えで動く量で， $𝑋$ を $𝑐$ 倍すると $l o g | 𝑐 |$ だけ増えた（命題 7.3.3）．散らばりを測るもう一つの量である分散は， $𝑐$ 倍すると $𝑐 2$ 倍になる（これを，学部の確率で扱う事実として既知とする）．二つを同じ物差しに載せるには， $ℎ$ を $2$ 倍して指数に持ち上げればよい．そうして作った量なら $𝑐$ 倍で $𝑐 2$ 倍になるはずで，実際そうなる（命題 16.7.2）．本節はその量を定めてガウス分布と一様分布で計算し，分散との大小を決める．続いて，密度の傾きの大きさを測る Fisher 情報量を定め，こちらもガウス分布で計算する．二つの量は，独立なガウス雑音を少しずつ足していく道筋の上で結びつく．

16.4 節で既知とした， $l o g$ が正の実数の全体から実数の全体への狭義単調な全単射であることから，どの実数についても，その値を対数にもつ正の実数はただ一つ定まる．

定義 16.7.1（エントロピーべき）. $𝑋$ を密度をもつ実数値確率変数とし， $ℎ (𝑋)$ （定義 7.1.2）が定まるとする． $l o g 𝑁 (𝑋) = 2 ℎ (𝑋)$ を満たすただ一つの正の実数 $𝑁 (𝑋)$ を， $𝑋$ の エントロピーべき と呼ぶ．

$𝑁$ はエントロピーべきを表す．量そのものを名指すときのほかは引数をとり，第8章が雑音の分散に使う裸の $𝑁$ とは別の記号である．定める式は，底を $𝑏$ にとれば $𝑁 (𝑋) = 𝑏 2 ℎ (𝑋)$ と書き直せる．底を取り替えても $𝑁 (𝑋)$ の値は動かない．取り替えによって $ℎ$ も $l o g$ も同じ倍率で変わり，定める式の両辺が同じ倍率で変わるからである．

形式化: entropyPower (ソース)，定める式 log_entropyPower (ソース)

形式化上の注記. 形式化は $l o g$ を自然対数にとるので，この量を $e x p (2 ℎ (𝑋))$ の形で直に定めている．また形式化は $ℎ$ が定まらない場合にも $ℎ$ に値 $0$ を返す約束なので，そのときこの量は $1$ になる．本文が $𝑁 (𝑋)$ を書くのは $ℎ (𝑋)$ が定まる場合だけである．なお Cover–Thomas の流儀にあたる， $2 𝜋 𝑒$ で割った量の値をガウス分布について与える宣言 entropyPower_div_two_pi_e_gaussianReal (InformationTheory/Shannon/EPI/Plumbing.lean) もある．

命題 16.7.2（定数倍でのふるまい）. $𝑋$ を密度をもつ実数値確率変数， $𝑐 \neq 0$ を実数とする． $ℎ (𝑋)$ が定まるならば $ℎ (𝑐 𝑋)$ も定まり， $𝑁 (𝑐 𝑋) = 𝑐 2 𝑁 (𝑋)$ である．

証明. 命題 7.3.3 より $ℎ (𝑐 𝑋)$ は定まって $ℎ (𝑐 𝑋) = ℎ (𝑋) + l o g | 𝑐 |$ である．よって

l o g 𝑁 (𝑐 𝑋) = 2 ℎ (𝑐 𝑋) = 2 ℎ (𝑋) + 2 l o g | 𝑐 | = l o g 𝑁 (𝑋) + l o g 𝑐 2

であり，右辺は $l o g (𝑐 2 𝑁 (𝑋))$ に等しい（ $| 𝑐 | 2 = 𝑐 2$ である）．定義 16.7.1 は $𝑁 (𝑐 𝑋)$ を，対数が $2 ℎ (𝑐 𝑋)$ に等しいただ一つの正の実数として定めているから， $𝑁 (𝑐 𝑋) = 𝑐 2 𝑁 (𝑋)$ である． $◼$

形式化: entropyPower_map_mul_const (ソース)

形式化上の注記. 宣言は結論の等式だけを述べ，本文の「 $ℎ (𝑐 𝑋)$ も定まる」にあたる部分は含まず，その部分を述べる宣言も無い．命題 7.3.3 に紐付けた宣言も同じ形である．

命題 16.7.2 が， $ℎ$ を $2$ 倍して指数に持ち上げた理由である．分散も $𝑐$ 倍で $𝑐 2$ 倍になるので， $𝑁$ と分散は同じ倍率で動く．二つの大小を比べる意味が出てくるのはそのためで，比べた結果は命題 16.7.5 で出る．

例 16.7.3（一様分布のエントロピーべき）. $𝑤 > 0$ とし， $𝑋$ が長さ $𝑤$ の区間の上の一様分布に従うとすると， $ℎ (𝑋)$ は定まり $𝑁 (𝑋) = 𝑤 2$ である．

証明. 例 7.1.3 より $ℎ (𝑋)$ は定まって $ℎ (𝑋) = l o g 𝑤$ である．よって $2 ℎ (𝑋) = l o g 𝑤 2$ であり，定義 16.7.1 より $𝑁 (𝑋) = 𝑤 2$ である． $◼$

命題 16.7.4（ガウス分布のエントロピーべき）. $𝜇$ を実数， $𝜎 2 > 0$ とし， $𝑋$ が $N (𝜇, 𝜎 2)$ （定義 7.2.1）に従うとすると， $ℎ (𝑋)$ は定まり $𝑁 (𝑋) = 2 𝜋 𝑒 𝜎 2$ である．

証明. 定理 7.2.2 より $ℎ (𝑋)$ は定まって $ℎ (𝑋) = 12 l o g (2 𝜋 𝑒 𝜎 2)$ である．よって $2 ℎ (𝑋) = l o g (2 𝜋 𝑒 𝜎 2)$ であり，定義 16.7.1 より主張を得る． $◼$

形式化: entropyPower_gaussianReal (ソース)，「定まる」にあたる積分可能性 integrable_density_log_density_of_gaussian (ソース)

幅の $2$ 乗として読む. 7.1 節は $2 ℎ (𝑋)$ をその分布の実効的な幅と読んだ．底を $2$ にとれば $𝑁 (𝑋) = 2 2 ℎ (𝑋)$ はその幅の $2$ 乗である．例 16.7.3 の一様分布では幅が $𝑤$ そのもので $𝑁 (𝑋) = 𝑤 2$ になり，7.2 節が幅を $\sqrt 2 𝜋 𝑒 𝜎$ と読んだガウス分布では，命題 16.7.4 のとおり $𝑁 (𝑋) = 2 𝜋 𝑒 𝜎 2$ になる．長さの $2$ 乗の次元をもつという点で， $𝑁$ は分散と同じ物差しの上にある．ただしガウス分布では， $𝑁 (𝑋)$ は分散そのものではなく $2 𝜋 𝑒$ 倍になる．定義 16.7.1 が $ℎ$ を指数に持ち上げるだけで，ガウス分布に値をそろえる定数を入れていないからである．Cover–Thomas は $2 𝜋 𝑒$ で割った量を同じ名前で呼ぶ流儀で，そちらではガウス分布での値が分散そのものになる．どちらをとっても命題 16.7.2 の $𝑐 2$ 倍のふるまいは変わらないので，本書は定義に定数を持ち込まないほうをとる．

分散を固定したときにガウス分布が微分エントロピーを最大にする（定理 7.2.4）ことは，指数に持ち上げてもそのまま残る．

命題 16.7.5（分散による上界）. $𝜎 2 > 0$ とし， $𝑋$ を密度をもつ実数値確率変数とする． $ℎ (𝑋)$ が定まり， $𝑋$ が平均をもち，その分散が定まって $𝜎 2$ 以下であるならば $𝑁 (𝑋) \leq 2 𝜋 𝑒 𝜎 2$ である．

証明. 定理 7.2.4 より $ℎ (𝑋) \leq 12 l o g (2 𝜋 𝑒 𝜎 2)$ である．両辺を $2$ 倍すると，定義 16.7.1 より左辺は $l o g 𝑁 (𝑋)$ であり，右辺は $l o g (2 𝜋 𝑒 𝜎 2)$ である． $l o g$ が狭義単調（16.4 節）だから主張を得る． $◼$

形式化上の注記. この主張をそのまま述べる単独の宣言はない．四つの合成で得られる．微分エントロピーを $12 l o g (2 𝜋 𝑒 𝜎 2)$ で押さえる定理 7.2.4 の紐付け先と，その右辺の実数をガウス分布の微分エントロピーに書き直す定理 7.2.2 の紐付け先と，微分エントロピーの大小をエントロピーべきの大小に移す entropyPower_le_of_differentialEntropy_le (InformationTheory/Shannon/EPI/Plumbing.lean) と，ガウス分布のエントロピーべきの値を与える命題 16.7.4 の紐付け先である．三つめが比べるのは測度どうしなので，一つめの右辺を測度の微分エントロピーに直す二つめを挟まないとつながらない．

この上界が達成されることを見るために，第7章 7.2 節が借りた ガウス分布の基本性質 をそのまま引く．すなわち，定義 7.2.1 の関数は実軸の上での積分が $1$ であり，それを密度とする確率変数の平均は $𝜇$ ，分散は $𝜎 2$ であって， $\int ℝ (𝑥 - 𝜇) 2 𝑔 𝜇, 𝜎 2 (𝑥) 𝑑 𝑥 = 𝜎 2$ である．最後の形は，7.2 節が定理 7.2.2 の証明で使ったものと同じである．当てる対象は定義 7.2.1 のガウス分布に従う実数値確率変数だけで，7.2 節が宣言した射程からは広がらない．依存するのは系 16.7.6 と命題 16.7.8 の証明の二つである．

系 16.7.6. $𝜇$ を実数， $𝜎 2 > 0$ とし， $𝑋$ が $N (𝜇, 𝜎 2)$ （定義 7.2.1）に従うとすると， $𝑋$ は命題 16.7.5 の仮定をこの $𝜎 2$ について満たし，その不等式は等号で成り立つ．

証明. 借りたガウス分布の基本性質より $𝑋$ は平均 $𝜇$ をもち，分散は $𝜎 2$ で，これは $𝜎 2$ 以下である．また定理 7.2.2 より $ℎ (𝑋)$ は定まる．よって命題 16.7.5 の仮定を満たす．その値は命題 16.7.4 より $2 𝜋 𝑒 𝜎 2$ で，命題 16.7.5 の右辺に等しい． $◼$

形式化上の注記. 系 16.7.6 に対応する単独の宣言はない．命題 16.7.4 に紐付けた宣言と，ガウス分布の分散を与える gaussianReal_variance_eq (InformationTheory/Shannon/DifferentialEntropy.lean) を合わせて得られる．

一様分布では等号にならない．例 7.2.6 の証明が求めたとおり，長さ $𝑤$ の区間の上の一様分布の分散は $𝑤 2 / 12$ である．命題 16.7.5 をこの値でとると上界は $2 𝜋 𝑒 𝑤 2 / 12 = (𝜋 𝑒 / 6) 𝑤 2 = 1.4232 \dots 𝑤 2$ で，例 16.7.3 の $𝑁 (𝑋) = 𝑤 2$ を確かに上から抑える．比 $𝜋 𝑒 / 6$ は，例 7.2.6 が出した微分エントロピーの差 $12 l o g 𝜋 𝑒 6$ を指数に持ち上げたものである．

ここまでは，密度がどれだけ広がっているかを測ってきた．次に測るのは，密度がどれだけ急に変わるかである．

定義 16.7.7（Fisher 情報量）. $𝑋$ を密度 $𝑓$ をもつ実数値確率変数とし， $𝑓$ は実軸のすべての点で微分可能かつ正であるとする． $\int ℝ (𝑓' (𝑥) 𝑓 (𝑥)) 2 𝑓 (𝑥) 𝑑 𝑥$ が有限であるとき，その値を $𝑋$ の Fisher 情報量 と呼んで $𝐽 (𝑋)$ と書き，このとき $𝐽 (𝑋)$ が 定まる という．

$𝐽$ は Fisher 情報量を表す．この文字は既出の章がそれぞれ別の意味に使っているが，本節のものはそのどれとも別である．定義 16.7.7 は密度を一つ選んだうえでの量だが，値は選び方によらない．定義 7.1.1 より同じ $𝑋$ の二つの密度はどの有界閉区間の上でも積分が等しく，定義 16.7.7 の条件を満たす密度は微分可能だから連続であって，どの有界閉区間の上でも積分が等しい二つの連続関数は全点で一致する（最後の一歩を，学部の解析で扱う事実として既知とする）．被積分関数に現れる $𝑓' / 𝑓$ は，密度の増え方をその点の密度自身で割ったもので，密度が急に立ち上がっている点ほど絶対値が大きい．その $2$ 乗を，やはり密度自身で平均している．広がりを測る定義 16.7.1 と違って， $𝐽$ が見ているのは密度の形の細かさである．この量を情報量と呼ぶのは，密度を横に少しずらしたときの見分けやすさを測るからである．形は同じで位置だけが分かっていない分布から標本を得て，その位置を当てにいくとしよう．位置を少し動かしたときに密度が大きく変わる分布ほど，どこにいるかは当てやすい．統計でその当てやすさを測るのに現れるのが同じ量で，定義 16.7.7 はそれを，位置がずれるだけの場合について密度の形で書いたものである．

形式化: fisherInfoOfDensity (ソース)

形式化上の注記. 形式化も密度を引数として受け取る．分布から取り出した密度は一般に微分可能な代表元にならないためである．値は $[0, \infty]$ にとる約束なので，本文が「定まる」と呼ばなかった場合にも値を返す．定義の中の $𝑓' / 𝑓$ は，形式化では対数微分として書かれている．

計算のために 微積分の計算規則 を既知とする．積分の線形性，合成関数の微分と指数関数の導関数， $l o g 𝑡$ の導関数が $(l o g 𝑒) / 𝑡$ であること， $1$ 次式による置換積分，部分積分， $𝑡 2 l o g 𝑡$ が $𝑡 ↓ 0$ で $0$ に近づくこと，連続関数の定積分が原始関数の差に等しいこと（微積分の基本定理），および有限な値に収束する広義積分の扱いである．このうち $1$ 次式による置換積分は第7章 7.3 節が，積分の線形性・ $l o g 𝑡$ の導関数・部分積分・ $𝑡 2 l o g 𝑡$ の極限・広義積分の扱いは 7.1 節が，同じ資格ですでに借りている．本節が新たに加えるのは，合成関数の微分と指数関数の導関数と微積分の基本定理である．当てる対象は，命題 16.7.8 と例 16.8.2 の証明に現れる密度と，それに多項式や対数を掛けて作る関数，および例 16.7.9 の証明が雑音の分散を変数として書く， $1$ 次式の対数とその逆数だけである．

命題 16.7.8（ガウス分布の Fisher 情報量）. $𝜇$ を実数， $𝜎 2 > 0$ とし， $𝑋$ が $N (𝜇, 𝜎 2)$ （定義 7.2.1）に従うとすると， $𝐽 (𝑋)$ は定まり $𝐽 (𝑋) = 1 / 𝜎 2$ である．

証明. 定義 7.2.1 の密度 $𝑔 𝜇, 𝜎 2$ は実軸のすべての点で正であり，借りた微積分の計算規則より微分可能で

𝑔' 𝜇, 𝜎 2 (𝑥) = - 𝑥 - 𝜇 𝜎 2 𝑔 𝜇, 𝜎 2 (𝑥)

である．よって定義 16.7.7 の被積分関数は $(𝑥 - 𝜇) 2 𝜎 4 𝑔 𝜇, 𝜎 2 (𝑥)$ であり，借りたガウス分布の基本性質より

\int ℝ (𝑥 - 𝜇) 2 𝜎 4 𝑔 𝜇, 𝜎 2 (𝑥) 𝑑 𝑥 = 𝜎 2 𝜎 4 = 1 𝜎 2

である．これは有限だから $𝐽 (𝑋)$ は定まり，その値は $1 / 𝜎 2$ である． $◼$

形式化: fisherInfoOfDensity_gaussianPDFReal (ソース)

二つの量を掛けてみる. ガウス分布では命題 16.7.4 より $𝑁 (𝑋) = 2 𝜋 𝑒 𝜎 2$ ，命題 16.7.8 より $𝐽 (𝑋) = 1 / 𝜎 2$ だから，積は $𝜎 2$ に依らず $2 𝜋 𝑒$ である．散らばりが大きいほど $𝑁$ は大きく $𝐽$ は小さい，という向きが，ガウス分布では正確に釣り合っている．一般の分布でも，二つが定まるかぎり，この積は $2 𝜋 𝑒$ を下回らないことが知られている（エントロピーの等周不等式と呼ばれる）．ガウス分布での値がちょうど $2 𝜋 𝑒$ だから，ガウス分布は積を最小にする．

等周とあるのは，16.5 節と同じ形の問いだからである．あちらは大きさにあたる要素数を決めて，境界にあたる辺の本数を最小にする問いで，要素数が $2$ のべきなら，最小は部分立方体でとられた（系 16.5.9）．こちらは大きさにあたるエントロピーべきを決めて，境界にあたる Fisher 情報量を最小にする問いで，最小はガウス分布でとられる．本書はこの不等式を示さず，形式化もしていない．本章のどの主張もこれを使わないので，借りる道具には数えず，名前を書くにとどめる．

二つの量が結びつくのは，分布を動かしたときである．動かし方として，独立なガウス雑音を少しずつ足していくもの，すなわち $𝑠$ を $0$ から増やしながら $𝑋 + \sqrt 𝑠 𝑍$ を見ていくものをとり，これを以下，熱流と呼ぶ．名前は， $𝑠$ を時間とみると，この道筋の密度が熱の伝わり方と同じ形の方程式に従うことによる（本書はその方程式を扱わない）．ここから次節でエントロピーべき不等式を借りるところまでは，その不等式がどこから来るかを見せるのが目的である．途中で借りる de Bruijn の恒等式と Stam の不等式は，本書のどの主張の証明も使わない．用意するものが二つある．

熱流を書くには，ガウス雑音を足したものがまたガウス分布に従うことが要る．第9章 9.4 節が確率変数の言葉で借り直した ガウス分布の畳み込み を引く．独立で $N (𝜇 1, 𝜎 21)$ と $N (𝜇 2, 𝜎 22)$ （定義 7.2.1）に従う二つの実数値確率変数の和が $N (𝜇 1 + 𝜇 2, 𝜎 21 + 𝜎 22)$ に従う，という事実である．9.4 節は差についても借りたが，本章が使うのは和だけで，射程はそのぶん狭い．あわせて，独立な二つの実数値確率変数の一方に $0$ でない定数を掛けても独立性が保たれることを既知とする．当てる対象は，本節と次節に現れるガウス分布に従う実数値確率変数だけである．依存するのは例 16.7.9 と命題 16.8.1 の証明の二つである．

de Bruijn の恒等式 を借りる． $𝑋$ を密度をもつ実数値確率変数で $2$ 乗の平均をもつもの， $𝑍$ を $N (0, 1)$ （定義 7.2.1）に従う確率変数とし， $𝑋$ と $𝑍$ は独立であるとする．このとき $𝑠 > 0$ について $𝑋 + \sqrt 𝑠 𝑍$ は密度をもち $𝐽 (𝑋 + \sqrt 𝑠 𝑍)$ （定義 16.7.7）は定まって，次の二つが成り立つ，という主張である．第一に， $𝑡 > 0$ において $𝑠 \mapsto ℎ (𝑋 + \sqrt 𝑠 𝑍)$ は微分可能で，その $𝑡$ での導関数は $l o g 𝑒 2 𝐽 (𝑋 + \sqrt 𝑡 𝑍)$ に等しい．第二に，さらに $ℎ (𝑋)$ が定まるならば， $𝑡 \geq 0$ について

ℎ (𝑋 + \sqrt 𝑡 𝑍) - ℎ (𝑋) = l o g 𝑒 2 \int 𝑡 0 𝐽 (𝑋 + \sqrt 𝑠 𝑍) 𝑑 𝑠

である．微分の形を $0$ から $𝑡$ まで積分すれば積分の形が出そうに見えるが，微分の形が言えているのは $𝑡 > 0$ だけなので， $𝑠 ↓ 0$ の端をつなぐ段が別に要る．そこで二つを別々に借りる．当てる対象は，本節の $𝑋 + \sqrt 𝑠 𝑍$ と，16.8 節がエントロピーべき不等式の出どころを述べる筋書きの中で当てる，密度をもつ独立な二つの実数値確率変数とその和である．本書のどの主張の証明もこれを使わない．例 16.7.9 がガウス分布の場合にこれを確かめ，16.8 節がその筋書きの中で引く．証明を載せないのは，積分と微分の順序を入れ替える段が要り，本書がその道具を用意していないからである．

形式化: 微分の形 debruijn_identity_per_time (ソース)

形式化上の注記. 形式化は $l o g$ を自然対数にとるので，紐付けた宣言に $l o g 𝑒$ の因子が現れない．底を $𝑒$ にとった本文の式と同じものである．宣言は $𝑋 + \sqrt 𝑠 𝑍$ の密度を， $𝑋$ の密度とガウス核との畳み込みとして式で書いている．述べているのは導関数の等式だけで，本文の「 $𝐽 (𝑋 + \sqrt 𝑠 𝑍)$ は定まる」にあたる部分は含まない．宣言に現れる Fisher 情報量は定義 16.7.7 の形式化を実数に読み替えたもので，定まらない場合にも値を返す．積分の形にも宣言 debruijn_identity_integrated (InformationTheory/Shannon/FisherInfo/DeBruijnStandalone.lean) があるが，ポインタは付けない．掲載しているリリースの時点では，その結論が「ある関数の族があって，その Fisher 情報量の積分がエントロピーの差に等しい」という存在の形をしていて，その族が各時刻の密度であることを結論の中で縛っていないからである．

増え方が細かさで決まると読む. 恒等式が言っているのは，雑音を少し足したときに微分エントロピーが増える速さが，そのときの密度の細かさ $𝐽$ で決まるということである．でこぼこの多い密度は，雑音を少し足すだけで大きく平らになるので $ℎ$ が大きく増え，すでに滑らかな密度は増えにくい．

例 16.7.9（熱流に沿った微分エントロピー）. $𝜇$ を実数， $𝜎 2 > 0$ とし， $𝑋$ が $N (𝜇, 𝜎 2)$ （定義 7.2.1）に従い， $𝑍$ が $N (0, 1)$ に従い， $𝑋$ と $𝑍$ は独立であるとする．このとき $𝑠 \geq 0$ について $ℎ (𝑋 + \sqrt 𝑠 𝑍)$ は定まって $12 l o g (2 𝜋 𝑒 (𝜎 2 + 𝑠))$ に等しく，次の二つが成り立つ．

$𝑡 > 0$ において， $𝑠 \mapsto ℎ (𝑋 + \sqrt 𝑠 𝑍)$ は微分可能で，その $𝑡$ での導関数は $l o g 𝑒 2 𝐽 (𝑋 + \sqrt 𝑡 𝑍)$ に等しい．
$𝑡 \geq 0$ について $ℎ (𝑋 + \sqrt 𝑡 𝑍) - ℎ (𝑋) = l o g 𝑒 2 \int 𝑡 0 𝐽 (𝑋 + \sqrt 𝑠 𝑍) 𝑑 𝑠$ である．

証明. $𝑠 > 0$ とする．例 7.3.6 を，掛ける定数 $\sqrt 𝑠$ ，足す定数 $0$ ととって当てると $\sqrt 𝑠 𝑍$ は $N (0, 𝑠)$ に従い，ガウス分布の畳み込みとあわせて既知とした定数倍での独立性の保存より， $𝑋$ と $\sqrt 𝑠 𝑍$ は独立である．借りたガウス分布の畳み込みより $𝑋 + \sqrt 𝑠 𝑍$ は $N (𝜇, 𝜎 2 + 𝑠)$ に従い，定理 7.2.2 より $ℎ (𝑋 + \sqrt 𝑠 𝑍)$ は定まって $12 l o g (2 𝜋 𝑒 (𝜎 2 + 𝑠))$ である． $𝑠 = 0$ のときは $𝑋 + \sqrt 𝑠 𝑍 = 𝑋$ で，同じ式が定理 7.2.2 そのものである．

1 を示す．借りた微積分の計算規則より， $𝑠 \mapsto 12 l o g (2 𝜋 𝑒 (𝜎 2 + 𝑠))$ は微分可能で，その $𝑡$ での導関数は $l o g 𝑒 2 (𝜎 2 + 𝑡)$ である．一方命題 16.7.8 を $N (𝜇, 𝜎 2 + 𝑡)$ に当てると $𝐽 (𝑋 + \sqrt 𝑡 𝑍) = 1 / (𝜎 2 + 𝑡)$ だから，二つは一致する．

2 を示す．借りた微積分の計算規則より $𝑠 \mapsto 1 l o g 𝑒 l o g (𝜎 2 + 𝑠)$ の導関数は $1 𝜎 2 + 𝑠$ であり，これは $[0, 𝑡]$ の上で連続だから，微積分の基本定理より

\int 𝑡 0 𝑑 𝑠 𝜎 2 + 𝑠 = 1 l o g 𝑒 (l o g (𝜎 2 + 𝑡) - l o g 𝜎 2)

である．命題 16.7.8 より被積分関数は $𝐽 (𝑋 + \sqrt 𝑠 𝑍)$ に等しいので，両辺に $l o g 𝑒 2$ を掛けると，右辺は $12 l o g (𝜎 2 + 𝑡) - 12 l o g 𝜎 2$ になる．いっぽう 2 の左辺は，上で求めた値より $12 l o g (2 𝜋 𝑒 (𝜎 2 + 𝑡)) - 12 l o g (2 𝜋 𝑒 𝜎 2)$ であり， $l o g$ の中の共通の因子 $2 𝜋 𝑒$ が引き算で消えて同じ値になる． $◼$

形式化: 値の等式 differentialEntropy_gaussianConvolution_of_gaussian (ソース)

形式化上の注記. 宣言が述べているのは値の等式だけで，本文の「定まる」にあたる部分は含まない．1 にも 2 にもポインタを付けない．1 をガウス分布について述べる単独の宣言はなく，借りた de Bruijn の恒等式の微分の形の紐付け先を， $𝑋$ の密度が定義 7.2.1 のガウス密度である場合に読み，命題 16.7.8 の紐付け先と合わせて得られる．2 にあたる宣言 debruijn_identity_integrated_gaussian (InformationTheory/Shannon/FisherInfo/DeBruijnStandalone.lean) は実在するが，掲載しているリリースの時点では，借りた恒等式の積分の形の宣言と同じく，結論が存在の形をしていて，積分の中の Fisher 情報量が各時刻の密度についてのものであることを縛っていない．

恒等式の両辺を数で突き合わせる. $𝜎 2 = 1$ ， $𝑡 = 3$ とし，底を $2$ にとる．例 16.7.9 の 2 の左辺は $12 l o g 2 (2 𝜋 𝑒 \cdot 4) - 12 l o g 2 (2 𝜋 𝑒) = 12 l o g 2 4 = 1$ ビットである．右辺は， $𝐽 (𝑋 + \sqrt 𝑠 𝑍) = 1 / (1 + 𝑠)$ で $\int 30 𝑑 𝑠 1 + 𝑠 = 1 l o g 2 𝑒 l o g 2 4 = 2 l o g 2 𝑒$ だから， $l o g 2 𝑒 2 \cdot 2 l o g 2 𝑒 = 1$ ビットである．雑音の分散を $0$ から $3$ まで増やすあいだに，微分エントロピーはちょうど $1$ ビット増える．

de Bruijn の恒等式は，微分エントロピーの増え方を Fisher 情報量で書いた．増え方が書けたということは，Fisher 情報量の側で成り立つ不等式を，積分して微分エントロピーの側へ運べるということである．次節はその運び先を見る．

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