16.2 Han の不等式

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

定理 16.2.1（Han の不等式）. 定義 16.1.1 の設定で

(𝑛 - 1) 𝐻 (𝑋 {1, \dots, 𝑛}) \leq 𝑛 \sum 𝑖 = 1 𝐻 (𝑋 {1, \dots, 𝑛} ∖ {𝑖})

である．

証明. 番号 $𝑖$ を一つ固定する． $𝑋 {1, \dots, 𝑛}$ を対 $(𝑋 {1, \dots, 𝑛} ∖ {𝑖}, 𝑋 𝑖)$ とみて（補題 16.1.2），定理 1.2.3 をこの対に当てると

𝐻 (𝑋 {1, \dots, 𝑛}) - 𝐻 (𝑋 {1, \dots, 𝑛} ∖ {𝑖}) = 𝐻 (𝑋 𝑖 ∣ 𝑋 {1, \dots, 𝑛} ∖ {𝑖})

である． ${1, \dots, 𝑖 - 1}$ と ${𝑖 + 1, \dots, 𝑛}$ は交わらず，和が ${1, \dots, 𝑛} ∖ {𝑖}$ である．右辺の条件を対 $(𝑋 {1, \dots, 𝑖 - 1}, 𝑋 {𝑖 + 1, \dots, 𝑛})$ とみて（補題 16.1.2），定理 1.2.4 を当てると

𝐻 (𝑋 𝑖 ∣ 𝑋 {1, \dots, 𝑛} ∖ {𝑖}) \leq 𝐻 (𝑋 𝑖 ∣ 𝑋 {1, \dots, 𝑖 - 1})

である． $𝑖$ について足し合わせる．左辺の和は $𝑛 𝐻 (𝑋 {1, \dots, 𝑛}) - \sum 𝑛 𝑖 = 1 𝐻 (𝑋 {1, \dots, 𝑛} ∖ {𝑖})$ であり，右辺の和は定理 16.1.4 を $𝑆 = {1, \dots, 𝑛}$ に当てて $𝐻 (𝑋 {1, \dots, 𝑛})$ に等しい．移項すれば主張を得る． $◼$

形式化: han_inequality (ソース)

注記

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

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

系 16.2.2（部分集合版の Han の不等式）. 定義 16.1.1 の設定で，空でない $𝑆 \subseteq {1, \dots, 𝑛}$ について

(| 𝑆 | - 1) 𝐻 (𝑋 𝑆) \leq \sum 𝑖 \in 𝑆 𝐻 (𝑋 𝑆 ∖ {𝑖})

である．

証明. $𝑆$ に属する番号を小さい順に $𝑖 1 < \dots < 𝑖 | 𝑆 |$ と並べ， $𝑌 𝑗 : = 𝑋 𝑖 𝑗$ とおく． $𝑌 1, \dots, 𝑌 | 𝑆 |$ は定義 16.1.1 の設定を満たす族である． $𝑅 \subseteq 𝑆$ に対し， $𝑅$ に属する番号を $𝑌$ の側の番号に読み替えた集合を $𝑅'$ と書くと $𝐻 (𝑋 𝑅) = 𝐻 (𝑌 𝑅')$ である（補題 16.1.2）．定理 16.2.1 を $𝑌$ の族に当てると，左辺は $(| 𝑆 | - 1) 𝐻 (𝑌 {1, \dots, | 𝑆 |}) = (| 𝑆 | - 1) 𝐻 (𝑋 𝑆)$ であり，右辺は $𝑌$ の番号を $1$ 個ずつ抜いた項の和である． $𝑌$ の番号 $𝑗$ を抜いた集合に対応する $𝑆$ の部分集合は $𝑆 ∖ {𝑖 𝑗}$ だから，右辺は $\sum 𝑖 \in 𝑆 𝐻 (𝑋 𝑆 ∖ {𝑖})$ に等しい． $◼$

形式化: han_inequality_subset (ソース)

例 16.2.3. 例 16.1.3 の二つの族について定理 16.2.1 の両辺を計算すると，1 の族では $4$ と $5$ ，2 の族では $4$ と $6$ である．

証明. どちらの族でも $𝐻 (𝑋 {1, 2, 3}) = 2$ だから， $𝑛 = 3$ より左辺は $2 \cdot 2 = 4$ である．右辺は $2$ 点集合についての値の和で，1 の族では $𝐻 (𝑋 {2, 3}) + 𝐻 (𝑋 {1, 3}) + 𝐻 (𝑋 {1, 2}) = 2 + 2 + 1 = 5$ ，2 の族では $2 + 2 + 2 = 6$ である． $◼$

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

定義 16.2.4（ $𝑘$ 点部分集合の平均エントロピー）. 定義 16.1.1 の設定で $1 \leq 𝑘 \leq 𝑛$ とする． ${1, \dots, 𝑛}$ の $𝑘$ 点部分集合すべてにわたる和をとって

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

と定め，これを $𝑘$ 点部分集合の平均エントロピー と呼ぶ．

本書には裸の $𝐻$ に添字を付けた形がすでに二つある．第3章 3.2 節は $𝐻 𝑛$ を長さ $𝑛$ のブロックのエントロピーそのものに使い，3.5 節までそのまま持ち越す．第4章は $𝐻 𝐷 (𝑋)$ を底を $𝐷$ にとったエントロピーに使う． $¯ 𝐻 𝑘$ はそのどちらとも別の量なので，横棒を付けて区別する． $(𝑛 𝑘)$ は $𝑘$ 点部分集合の個数だから， $¯ 𝐻 𝑘$ は「 $𝑘$ 点集合を一つ選んだときの，番号 $1$ 個あたりのエントロピー」を集合について平均したものである． $𝑘 = 𝑛$ のときは $¯ 𝐻 𝑛 = 𝐻 (𝑋 {1, \dots, 𝑛}) / 𝑛$ で， $𝑘 = 1$ のときは $¯ 𝐻 1 = 1 𝑛 \sum 𝑛 𝑖 = 1 𝐻 (𝑋 {𝑖})$ である．

形式化上の注記（定義 16.2.4 と定理 16.2.5 に共通）

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

定理 16.2.5. 定義 16.1.1 の設定で $1 \leq 𝑘 < 𝑛$ とすると，定義 16.2.4 の量について $¯ 𝐻 𝑘 + 1 \leq ¯ 𝐻 𝑘$ である．

証明. $| 𝑆 | = 𝑘 + 1$ を満たす $𝑆$ に系 16.2.2 を当てると $𝑘 𝐻 (𝑋 𝑆) \leq \sum 𝑖 \in 𝑆 𝐻 (𝑋 𝑆 ∖ {𝑖})$ である．これを $| 𝑆 | = 𝑘 + 1$ の $𝑆$ すべてにわたって足すと

𝑘 \sum | 𝑆 | = 𝑘 + 1 𝐻 (𝑋 𝑆) \leq \sum | 𝑆 | = 𝑘 + 1 \sum 𝑖 \in 𝑆 𝐻 (𝑋 𝑆 ∖ {𝑖})

である．右辺は， $| 𝑆 | = 𝑘 + 1$ かつ $𝑖 \in 𝑆$ を満たす対 $(𝑆, 𝑖)$ にわたる和である．対 $(𝑆, 𝑖)$ に対 $(𝑆 ∖ {𝑖}, 𝑖)$ を対応させると，これは $| 𝑇 | = 𝑘$ かつ $𝑖 \notin 𝑇$ を満たす対 $(𝑇, 𝑖)$ の全体との一対一の対応になる（逆向きの対応は $(𝑇, 𝑖)$ に $(𝑇 \cup {𝑖}, 𝑖)$ を対応させるものである）． $𝑇$ を固定するごとに $𝑖$ の選び方は $𝑛 - 𝑘$ 通りだから，右辺は $(𝑛 - 𝑘) \sum | 𝑇 | = 𝑘 𝐻 (𝑋 𝑇)$ に等しい．よって

𝑘 \sum | 𝑆 | = 𝑘 + 1 𝐻 (𝑋 𝑆) \leq (𝑛 - 𝑘) \sum | 𝑇 | = 𝑘 𝐻 (𝑋 𝑇)

である．割る前に，いま使った対応の両側を数え直しておく．対 $(𝑆, 𝑖)$ の個数は， $𝑆$ を先に選ぶ数え方で $(𝑘 + 1) (𝑛 𝑘 + 1)$ ， $𝑇$ を先に選ぶ数え方で $(𝑛 - 𝑘) (𝑛 𝑘)$ だから， $(𝑘 + 1) (𝑛 𝑘 + 1) = (𝑛 - 𝑘) (𝑛 𝑘)$ である．

$1 \leq 𝑘 < 𝑛$ だから $𝑘 (𝑛 - 𝑘) (𝑛 𝑘)$ は正で，両辺をこれで割ると

1 (𝑛 - 𝑘) (𝑛 𝑘) \sum | 𝑆 | = 𝑘 + 1 𝐻 (𝑋 𝑆) \leq 1 𝑘 (𝑛 𝑘) \sum | 𝑇 | = 𝑘 𝐻 (𝑋 𝑇)

である．右辺は定義 16.2.4 の $¯ 𝐻 𝑘$ である．左辺の係数の分母は，いま数え直した等式により $(𝑘 + 1) (𝑛 𝑘 + 1)$ に等しいから，左辺は $¯ 𝐻 𝑘 + 1$ である． $◼$

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

証明. $𝑛 = 3$ だから $(31) = (32) = 3$ ， $(33) = 1$ である．1 の族では $1$ 点集合についての値の和が $1 + 1 + 1 = 3$ ， $2$ 点集合についての値の和が $1 + 2 + 2 = 5$ ， $3$ 点集合についての値が $2$ だから， $¯ 𝐻 1 = 3 / (1 \cdot 3) = 1$ ， $¯ 𝐻 2 = 5 / (2 \cdot 3) = 5 / 6$ ， $¯ 𝐻 3 = 2 / (3 \cdot 1) = 2 / 3$ である．2 の族では三つの和がそれぞれ $3$ ， $6$ ， $2$ だから， $¯ 𝐻 1 = 3 / 3 = 1$ ， $¯ 𝐻 2 = 6 / 6 = 1$ ， $¯ 𝐻 3 = 2 / 3$ である． $◼$

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

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

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