16.2 Han の不等式

16.1 節 は部分集合のエントロピーを集合の関数として眺め,値の並び方についての性質を出した.本節はそこから最初の不等式を引く.個の変数を,番号を個ずつ抜いた通りの見方で観察する人たちがいるとしよう.どの人も個しか見ていないので,一人ぶんでは全体に届かない.ところが人ぶんを足すと,どの番号も回ずつ数えられて全体を何重にも覆うことになる.そこで重なりのぶんを戻す.人ぶんの合計をで割っても,なお全体のエントロピー以上である,というのが Han の不等式である.

定理 16.2.1(Han の不等式). 定義 16.1.1 の設定で

(𝑛1)𝐻(𝑋{1,,𝑛})𝑛𝑖=1𝐻(𝑋{1,,𝑛}{𝑖})

である.

証明. 番号を一つ固定する.を対とみて(補題 16.1.2),定理 1.2.3 をこの対に当てると

𝐻(𝑋{1,,𝑛})𝐻(𝑋{1,,𝑛}{𝑖})=𝐻(𝑋𝑖𝑋{1,,𝑛}{𝑖})

である.は交わらず,和がである.右辺の条件を対とみて(補題 16.1.2),定理 1.2.4 を当てると

𝐻(𝑋𝑖𝑋{1,,𝑛}{𝑖})𝐻(𝑋𝑖𝑋{1,,𝑖1})

である.について足し合わせる.左辺の和はであり,右辺の和は 定理 16.1.4に当ててに等しい.移項すれば主張を得る.

形式化: han_inequality (ソース)

形式化上の注記. 宣言は,番号を抜いた項を部分集合のエントロピー(定義 16.1.1)としてではなく,番目を除いた族のエントロピーとして直に定めている(jointEntropyExcept (InformationTheory/Shannon/Han/Basic.lean)).二つが同じ値であることは,系 16.2.2 に紐付けた宣言の証明の中で使われているが,公開された宣言としては立っていない.

覆いの回数で読む. 証明を通してみると,やっていることは二段である.まず 定理 1.2.3 で,番号を抜いた見方と全体との差が「以外をすべて知ったうえでに残る不確かさ」であることを出す.次に 定理 1.2.4 で,その条件をより小さい番号だけに減らす.減らしたあとの項はによらず 定理 16.1.4 の項そのものなので,個ぶんを足すとに化ける.左辺で回数えた全体から,この回ぶんを差し引いたものが倍である.

系 16.2.2(部分集合版の Han の不等式). 定義 16.1.1 の設定で,空でないについて

(|𝑆|1)𝐻(𝑋𝑆)𝑖𝑆𝐻(𝑋𝑆{𝑖})

である.

証明. に属する番号を小さい順にと並べ,とおく.定義 16.1.1 の設定を満たす族である.に対し,に属する番号をの側の番号に読み替えた集合をと書くとである(補題 16.1.2).定理 16.2.1の族に当てると,左辺はであり,右辺はの番号を個ずつ抜いた項の和である.の番号を抜いた集合に対応するの部分集合はだから,右辺はに等しい.

形式化: han_inequality_subset (ソース)

例 16.2.3. 例 16.1.3 の二つの族について 定理 16.2.1 の両辺を計算すると,1 の族では,2 の族ではである.

証明. どちらの族でもだから,より左辺はである.右辺は点集合についての値の和で,1 の族では,2 の族ではである.

定理 16.2.1 が比べたのは,点の集合と全体という隣り合う二つの大きさである.同じ比べ方は点と点のあいだでもできるはずで,そうするとからまで動かした鎖ができる.大きさの違う集合どうしを比べるには,集合の個数と番号の個数で割って番号あたりに直しておく必要がある.

定義 16.2.4(点部分集合の平均エントロピー). 定義 16.1.1 の設定でとする.点部分集合すべてにわたる和をとって

¯𝐻𝑘:=1𝑘(𝑛𝑘)|𝑆|=𝑘𝐻(𝑋𝑆)

と定め,これを点部分集合の平均エントロピー と呼ぶ.

本書には裸のに添字を付けた形がすでに二つある.第3章 3.2 節を長さのブロックのエントロピーそのものに使い,3.5 節 までそのまま持ち越す.第4章を底をにとったエントロピーに使う.はそのどちらとも別の量なので,横棒を付けて区別する.点部分集合の個数だから,は「点集合を一つ選んだときの,番号個あたりのエントロピー」を集合について平均したものである.のときはで,のときはである.

形式化上の注記(定義 16.2.4定理 16.2.5 に共通). 定義 16.2.4にあたる宣言も,定理 16.2.5 にあたる宣言もない.点部分集合にわたる部分集合のエントロピーの和を結論に含む宣言を,名前ではなく結論の形で探して見つからなかった.機械検証が及ぶのは 系 16.2.2 までで,そこから先の数え上げは本文の側にある.

定理 16.2.5. 定義 16.1.1 の設定でとすると,定義 16.2.4 の量についてである.

証明. を満たす系 16.2.2 を当てるとである.これをすべてにわたって足すと

𝑘|𝑆|=𝑘+1𝐻(𝑋𝑆)|𝑆|=𝑘+1 𝑖𝑆𝐻(𝑋𝑆{𝑖})

である.右辺は,かつを満たす対にわたる和である.対に対を対応させると,これはかつを満たす対の全体との一対一の対応になる(逆向きの対応はを対応させるものである).を固定するごとにの選び方は通りだから,右辺はに等しい.よって

𝑘|𝑆|=𝑘+1𝐻(𝑋𝑆)(𝑛𝑘)|𝑇|=𝑘𝐻(𝑋𝑇)

である.割る前に,いま使った対応の両側を数え直しておく.対の個数は,を先に選ぶ数え方でを先に選ぶ数え方でだから,である.

だからは正で,両辺をこれで割ると

1(𝑛𝑘)(𝑛𝑘)|𝑆|=𝑘+1𝐻(𝑋𝑆)1𝑘(𝑛𝑘)|𝑇|=𝑘𝐻(𝑋𝑇)

である.右辺は 定義 16.2.4である.左辺の係数の分母は,いま数え直した等式によりに等しいから,左辺はである.

例 16.2.6. 例 16.1.3 の二つの族について 定義 16.2.4 の値を計算すると,1 の族では¯𝐻2 =5/6であり,2 の族ではである.

証明. だからである.1 の族では点集合についての値の和が点集合についての値の和が点集合についての値がだから,¯𝐻1 =3/(1 3) =1¯𝐻2 =5/(2 3) =5/6である.2 の族では三つの和がそれぞれ6だから,¯𝐻1 =3/3 =1¯𝐻2 =6/6 =1である.

1 の族ではの不等号が二つとも狭義になり,2 の族では最初の不等号が等号になる.2 の族で等号が起きるのは,点集合についての値がちょうど点集合についての値倍で,番号個あたりに直すと点集合のときと変わらないからである.その中身は,どの二つの変数も独立だということである.例 16.1.3 の証明で見たとおり,2 の族ではどの点集合についても対が点上の一様分布に従い,これは二つの一様分布の積である.三つまとめると値がにとどまるので,そこから先の不等号は狭義になる.つまり 2 の族は,対ごとには独立でも三つ全体では独立でなく,そのずれをのあいだの狭義の不等号がとらえている.

について下がっていくという読み方は,番号個あたりの不確かさが「まわりを何個いっしょに見るか」で決まり,いっしょに見る個数が増えるほど小さくなる,ということである.鎖の両端はで,前者は変数ずつのエントロピーの平均,後者は全体のエントロピーをで割ったものである.この両端どうしを直に比べる不等式は,次節で別の道から出る(系 16.3.2).

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