16.1 部分集合のエントロピー

エントロピーについて成り立つ不等式は，どこから生まれるのか．本章は出どころを二つ見る．前半，本節から 16.5 節までは，いくつもの変数をいろいろな見方で覆っておいて，どの変数が何回数えられたかを勘定することから不等号を出す．後半の 16.6 節から 16.8 節までは，二つを足したときのふるまいを問うことから出す．後半で相手にするのは，正定値行列の行列式を $1$ 座標あたりに直した量と，第7章の微分エントロピーを指数に持ち上げた量で，どちらについても，二つを足すと値が足し算以上になるという同じ形の不等式が現れる．

前半の材料は第1章 1.2 節にそろっている．そこでは確率変数を二つ並べて，まとめて見たときの不確かさ（定義 1.2.1）と，片方を知ったあとに残る不確かさ（定義 1.2.2）を測った．二つはチェイン則（定理 1.2.3）で結ばれ，条件を増やしても残りの不確かさが増えないこと（定理 1.2.4）がそこに重なった．前半はこの二つを確率変数の族に当てる．族が $𝑛$ 個あるとき，まとめて見る相手は一通りではない．番号の集合を選ぶたびに一つの値が決まるので，見えているのは ${1, \dots, 𝑛}$ の部分集合に実数を返す関数である．

測る量そのものは新しくない．番号の集合 $𝑆$ を選んだら， $𝑆$ に属する番号の変数を一つの組にまとめてしまえばよく，定義 1.1.1 のエントロピーがそのまま値を与える．新しいのは $𝑆$ を動かして値どうしを比べるところである．本節が出す値の並び方についての性質のうち，あとの節の証明が直に引くのは，番号を一つずつ足していったときの分解（定理 16.1.4）である．残りは枠になる．空集合についての値が $0$ であること， $𝑆$ を大きくしても値が減らないこと（命題 16.1.5），二つの集合の和と交わりについての不等式（定理 16.1.6）の三つがそれで，この三つをそろえたところに定義 16.1.7 の枠が現れる．

定義 16.1.1（部分集合のエントロピー）. $𝑛 \geq 1$ とし， $X$ を有限アルファベット， $𝑋 1, \dots, 𝑋 𝑛$ を $X$ に値をとる確率変数とする． $𝑆 \subseteq {1, \dots, 𝑛}$ に対し， $𝑆$ に属する番号を小さい順に並べ，対応する変数を並べた組を $𝑋 𝑆$ と書く．この組は $𝑆$ の各番号に $X$ の元を対応させる関数とみなせるから， $𝑋 𝑆$ は $𝑆$ から $X$ への関数の全体に値をとる一つの確率変数である（ $𝑆 = \emptyset$ のときこの値域は要素が一つの集合である）．この確率変数のエントロピー（定義 1.1.1）を $𝑆$ についての 部分集合のエントロピー と呼んで $𝐻 (𝑋 𝑆)$ と書く．

組を組のままにせず関数として言い直したのは， $𝑆$ が空のときにも値の全体が定まり， $𝑆$ をどう動かしても値の入れ物が同じ作り方で決まるからである．16.4 節では組から座標の一部だけを残す操作を扱うので，そこでもこの言い直しがそのまま効く． $| 𝑆 | = 1$ のときは定義 1.1.1 そのもの， $| 𝑆 | = 2$ のときは定義 1.2.1 の結合エントロピーであり， $𝑆$ が全体のときの $𝐻 (𝑋 {1, \dots, 𝑛})$ が， $𝑛$ 個をまとめて見たときの不確かさにあたる． $𝑋 \emptyset$ のとりうる値は一つしかないから，定義 1.1.1 の和は $- 1 l o g 1$ の一項だけになり， $𝐻 (𝑋 \emptyset) = 0$ である．

形式化: 部分集合のエントロピー jointEntropySubset (ソース)，族の全体についてのエントロピー jointEntropy (ソース)

形式化上の注記. 形式化は，族の変数がどれも同じ有限アルファベットに値をとるものとして扱う（本文も同じである）．空集合についての値が $0$ であることは jointEntropySubset_empty (InformationTheory/Shannon/Polymatroid.lean) が， $𝑆$ が全体のときに族の全体についてのエントロピーと一致することは jointEntropySubset_univ (InformationTheory/Shannon/Han/D.lean) が，それぞれ別の宣言として検証している．

組のまとめ方について一つ断っておく．定義 1.1.1 のエントロピーは値の分布だけで決まるので，組の成分を並べ替えても，成分の一部をまとめて対とみても，値は変わらない．以下の証明はこの読み替えを繰り返し使うので，先に補題として置く．

補題 16.1.2（値の読み替え）. $Y$ ， $Z$ ， $W$ を有限集合とし， $𝑌$ ， $𝑍$ ， $𝑊$ をそれぞれに値をとる確率変数とする． $𝜙$ を $Y$ から $Z$ への単射で $𝑍 = 𝜙 (𝑌)$ を満たすものとすると， $𝐻 (𝑌) = 𝐻 (𝑍)$ （定義 1.1.1）であり， $𝐻 (𝑊 ∣ 𝑌) = 𝐻 (𝑊 ∣ 𝑍)$ （定義 1.2.2）である．

証明. $𝜙$ は単射だから， $𝑧 = 𝜙 (𝑦)$ の形の値について， $𝑍 = 𝑧$ という事象と $𝑌 = 𝑦$ という事象は同じ事象である．よって二つの確率は等しい． $𝜙$ の像に入らない $𝑧$ については $𝑍 = 𝑧$ の確率が $0$ で，定義 1.1.1 の約束によりその項は和に寄与しない．したがって $𝐻 (𝑍)$ の和は $𝐻 (𝑌)$ の和と項ごとに一致する．

条件付きエントロピーも同じである．定義 1.2.2 は，条件の値ごとに残る不確かさを，その値の確率で平均したものである．いま見たとおり $𝑍 = 𝜙 (𝑦)$ と $𝑌 = 𝑦$ は同じ事象だから，その確率も，そのもとでの $𝑊$ の条件付き分布も一致し，各項が対応する．像に入らない値の項は重み $0$ で寄与しないから，二つの平均は等しい． $◻$

形式化上の注記. 読み替えにあたる宣言は二つある． $𝐻 (𝑌) = 𝐻 (𝑍)$ を entropy_measurableEquiv_comp (InformationTheory/Shannon/Pi.lean) が， $𝐻 (𝑊 ∣ 𝑌) = 𝐻 (𝑊 ∣ 𝑍)$ を condEntropy_measurableEquiv_comp (InformationTheory/Shannon/Pi.lean) が述べる．ただし二つが量化するのは可測同型，すなわち値どうしの全単射であって，補題 16.1.2 が量化する単射より狭い．単射一般についてこの補題を述べる単独の宣言は，結論の形で探しても見つからない．本節の証明が読み替えを使うところは，形式化ではこの二つを当てられる全単射の形に組み直されている．

たとえば $𝑆 \subseteq 𝑇$ のとき， $𝑋 𝑇$ の値に対 $(𝑋 𝑆, 𝑋 𝑇 ∖ 𝑆)$ の値を対応させる写像は単射だから，補題 16.1.2 より $𝑋 𝑇$ は対 $(𝑋 𝑆, 𝑋 𝑇 ∖ 𝑆)$ とみてよい．条件の側についても同じである．

例 16.1.3（重複と排他的論理和）. $X = {0, 1}$ ， $𝑛 = 3$ とし，値はビットで書く（1.1 節の約束どおり $l o g$ の底を $2$ にとる）．次の二つの族について値を並べる．

$𝑋 1$ を公平なコイン， $𝑋 2 : = 𝑋 1$ ， $𝑋 3$ を $𝑋 1$ と独立な公平なコインとすると， $𝐻 (𝑋 {1}) = 𝐻 (𝑋 {2}) = 𝐻 (𝑋 {3}) = 1$ ， $𝐻 (𝑋 {1, 2}) = 1$ ， $𝐻 (𝑋 {1, 3}) = 𝐻 (𝑋 {2, 3}) = 2$ ， $𝐻 (𝑋 {1, 2, 3}) = 2$ である．
$𝑋 1$ ， $𝑋 2$ を独立な公平なコイン， $𝑋 3 : = 𝑋 1 \oplus 𝑋 2$ （ $\oplus$ は排他的論理和）とすると， $1$ 点集合についての値はどれも $1$ ， $2$ 点集合についての値はどれも $2$ であり， $𝐻 (𝑋 {1, 2, 3}) = 2$ である．

証明. 確率 $0$ の値の項は定義 1.1.1 の約束により和に寄与しないので，どの場合も実際にとりうる値だけを数え，それらが等確率であることを見て例 1.1.3 を当てればよい．

1 を示す． $𝑋 1$ ， $𝑋 2$ ， $𝑋 3$ はどれも ${0, 1}$ 上の一様分布に従うから， $1$ 点集合についての値は例 1.1.3 を $𝑀 = 2$ で当てて $l o g 2 = 1$ である． $𝑋 {1, 2}$ のとりうる値は $(0, 0)$ と $(1, 1)$ の二つで確率はどちらも $1 / 2$ だから，同じく $𝑀 = 2$ で当てて $1$ である． $𝑋 1$ と $𝑋 3$ は独立でどちらも一様だから対 $(𝑋 1, 𝑋 3)$ は $4$ つの値を確率 $1 / 4$ ずつでとり， $𝑀 = 4$ で当てて $𝐻 (𝑋 {1, 3}) = l o g 4 = 2$ である． $𝑋 2 = 𝑋 1$ だから $𝐻 (𝑋 {2, 3})$ も同じ値である． $𝑋 {1, 2, 3}$ は $(𝑋 1, 𝑋 1, 𝑋 3)$ で，その値に $(𝑋 1, 𝑋 3)$ の値を対応させる写像は単射だから，値は $2$ である（補題 16.1.2）．

2 を示す．写像 $(𝑥 1, 𝑥 2) \mapsto (𝑥 1, 𝑥 1 \oplus 𝑥 2)$ は ${0, 1} 2$ から ${0, 1} 2$ への全単射である． $𝑋 1$ と $𝑋 2$ は独立でどちらも一様だから対 $(𝑋 1, 𝑋 2)$ は $4$ つの値を確率 $1 / 4$ ずつでとり，したがって対 $(𝑋 1, 𝑋 3)$ も $4$ つの値を確率 $1 / 4$ ずつでとる．写像 $(𝑥 1, 𝑥 2) \mapsto (𝑥 2, 𝑥 1 \oplus 𝑥 2)$ も全単射だから，対 $(𝑋 2, 𝑋 3)$ についても同じである．よって $2$ 点集合についての値はどれも例 1.1.3 を $𝑀 = 4$ で当てて $2$ であり，周辺分布をとれば $𝑋 3$ も一様だから， $1$ 点集合についての値はどれも $𝑀 = 2$ で当てて $1$ である． $𝑋 {1, 2, 3}$ のとりうる値は $(𝑥 1, 𝑥 2, 𝑥 1 \oplus 𝑥 2)$ の形の $4$ 通りで確率は $1 / 4$ ずつだから，値は $2$ である． $◼$

増えなくなる場所を見る. 二つの族は， $1$ 点集合についての値がどれも $1$ で，全体についての値が $2$ である点まで一致する．違うのは途中である．1 の族では番号 $1$ に番号 $2$ を足しても値が $1$ のまま増えないのに，2 の族ではどの $1$ 点集合にどの番号を足しても値が $1$ から $2$ へ増え，そのかわり $2$ 点集合に残りの番号を足しても $2$ のままである．どこで増えなくなるかが族の作りを写しており，その「足したときの増分」を正面から書いたのが次の定理である．

定理 16.1.4（部分集合のチェイン則）. 定義 16.1.1 の設定で，どの $𝑆 \subseteq {1, \dots, 𝑛}$ についても

𝐻 (𝑋 𝑆) = \sum 𝑖 \in 𝑆 𝐻 (𝑋 𝑖 ∣ 𝑋 𝑆 \cap {1, \dots, 𝑖 - 1})

である．

証明（ $| 𝑆 |$ についての数学的帰納法）. $𝑆 = \emptyset$ のとき， $𝑋 \emptyset$ のとりうる値は一つだから，定義 1.1.1 より左辺は $𝐻 (𝑋 \emptyset) = 0$ である．右辺は空の和で $0$ である．

$| 𝑆 | = 𝑚$ のすべての集合について主張が成り立つとし， $| 𝑆 | = 𝑚 + 1$ とする． $𝑆$ に属する番号のうち最大のものを $𝑗$ と書き， $𝑅 : = 𝑆 ∖ {𝑗}$ とおく． $𝑋 𝑆$ を対 $(𝑋 𝑅, 𝑋 𝑗)$ とみて（補題 16.1.2），定理 1.2.3 をこの対に当てると

𝐻 (𝑋 𝑆) = 𝐻 (𝑋 𝑅) + 𝐻 (𝑋 𝑗 ∣ 𝑋 𝑅)

である． $𝑗$ は $𝑆$ の最大の番号だから $𝑆 \cap {1, \dots, 𝑗 - 1} = 𝑅$ であり，第 $2$ 項は示すべき和の $𝑖 = 𝑗$ の項そのものである．第 $1$ 項に帰納法の仮定を当てると

𝐻 (𝑋 𝑅) = \sum 𝑖 \in 𝑅 𝐻 (𝑋 𝑖 ∣ 𝑋 𝑅 \cap {1, \dots, 𝑖 - 1})

である． $𝑖 \in 𝑅$ ならば $𝑖 < 𝑗$ だから $𝑗 \notin {1, \dots, 𝑖 - 1}$ であり， $𝑅 \cap {1, \dots, 𝑖 - 1} = 𝑆 \cap {1, \dots, 𝑖 - 1}$ である．よってこの和は示すべき和の $𝑖 \neq 𝑗$ の項の和に等しく， $𝑖 = 𝑗$ の項と合わせて主張を得る． $◼$

形式化: jointEntropySubset_chain_rule (ソース)

形式化上の注記. $𝑆$ が全体の場合を部分集合を経由せずに述べる宣言 jointEntropy_chain_rule (InformationTheory/Shannon/Han/Basic.lean) もあり，形式化ではそちらが上の宣言の土台になっている．

順に足していくと読む. 定理 1.2.3 は二つの変数について「まず一方，次にもう一方」と数えた．定理 16.1.4 はそれを $𝑆$ の番号の小さい順に繰り返しただけである． $𝑖$ の項は， $𝑆$ の中で $𝑖$ より小さい番号をすでに知ったうえで $𝑋 𝑖$ に残る不確かさで，足していくと $𝐻 (𝑋 𝑆)$ になる．番号の小さい順に足したのは書き方の都合で，左辺は $𝑆$ だけで決まる．

命題 16.1.5（包含についての単調性）. 定義 16.1.1 の設定で， $𝑆 \subseteq 𝑇 \subseteq {1, \dots, 𝑛}$ ならば $𝐻 (𝑋 𝑆) \leq 𝐻 (𝑋 𝑇)$ である．

証明. $𝑋 𝑇$ を対 $(𝑋 𝑆, 𝑋 𝑇 ∖ 𝑆)$ とみて（補題 16.1.2），定理 1.2.3 をこの対に当てると

𝐻 (𝑋 𝑇) = 𝐻 (𝑋 𝑆) + 𝐻 (𝑋 𝑇 ∖ 𝑆 ∣ 𝑋 𝑆)

である．定義 1.2.2 の中辺は， $𝑋 𝑆 = 𝑦$ ごとの残りの不確かさを重み $𝑝 (𝑦) \geq 0$ で平均したものであり，その各項は命題 1.1.4 より非負だから，第 $2$ 項は非負である． $◼$

形式化: jointEntropySubset_mono (ソース)

定理 16.1.6（劣モジュラ性）. 定義 16.1.1 の設定で，どの $𝑆, 𝑇 \subseteq {1, \dots, 𝑛}$ についても

𝐻 (𝑋 𝑆 \cup 𝑇) + 𝐻 (𝑋 𝑆 \cap 𝑇) \leq 𝐻 (𝑋 𝑆) + 𝐻 (𝑋 𝑇)

である．

証明. $𝑈 : = 𝑆 \cap 𝑇$ ， $𝑉 : = 𝑆 ∖ 𝑇$ とおく． $𝑆$ は $𝑈$ と $𝑉$ の交わらない和であり， $𝑆 \cup 𝑇$ は $𝑇$ と $𝑉$ の交わらない和である． $𝑋 𝑆$ を対 $(𝑋 𝑈, 𝑋 𝑉)$ ， $𝑋 𝑆 \cup 𝑇$ を対 $(𝑋 𝑇, 𝑋 𝑉)$ とみて（補題 16.1.2），定理 1.2.3 をこの二つの対に当てると

𝐻 (𝑋 𝑆) = 𝐻 (𝑋 𝑈) + 𝐻 (𝑋 𝑉 ∣ 𝑋 𝑈), 𝐻 (𝑋 𝑆 \cup 𝑇) = 𝐻 (𝑋 𝑇) + 𝐻 (𝑋 𝑉 ∣ 𝑋 𝑇)

である． $𝑈 \subseteq 𝑇$ だから， $𝐻 (𝑋 𝑉 ∣ 𝑋 𝑇)$ の条件を対 $(𝑋 𝑈, 𝑋 𝑇 ∖ 𝑈)$ とみて（補題 16.1.2），定理 1.2.4 を当てると

𝐻 (𝑋 𝑉 ∣ 𝑋 𝑇) \leq 𝐻 (𝑋 𝑉 ∣ 𝑋 𝑈)

である．三つを合わせると

𝐻 (𝑋 𝑆 \cup 𝑇) + 𝐻 (𝑋 𝑈) = 𝐻 (𝑋 𝑇) + 𝐻 (𝑋 𝑉 ∣ 𝑋 𝑇) + 𝐻 (𝑋 𝑈) \leq 𝐻 (𝑋 𝑇) + 𝐻 (𝑋 𝑉 ∣ 𝑋 𝑈) + 𝐻 (𝑋 𝑈) = 𝐻 (𝑋 𝑇) + 𝐻 (𝑋 𝑆)

であり， $𝑈 = 𝑆 \cap 𝑇$ だから主張を得る． $◼$

形式化: jointEntropySubset_submodular (ソース)

同じものを足したときの増分で読む. 定理 16.1.6 は移項すると $𝐻 (𝑋 𝑆 \cup 𝑇) - 𝐻 (𝑋 𝑇) \leq 𝐻 (𝑋 𝑆) - 𝐻 (𝑋 𝑆 \cap 𝑇)$ と書ける．左辺は $𝑇$ に $𝑆 ∖ 𝑇$ を足したときの増分，右辺は $𝑆 \cap 𝑇$ に同じ $𝑆 ∖ 𝑇$ を足したときの増分である． $𝑆 \cap 𝑇$ は $𝑇$ に含まれるから，「すでに知っていることが多いほど，同じものを足したときの増分は小さい」と読める．証明で不等号が入ったのは定理 1.2.4 を当てた一箇所だけで，劣モジュラ性は条件付けの単調性の言い換えにほかならない．

空集合についての値が $0$ であることと，命題 16.1.5 と定理 16.1.6 の三つは， $𝑆$ ごとに決まる値がどう並ぶかだけを述べていて，値がエントロピーであることをもう使っていない．同じ三つを満たす集合の関数には名前が付いている．

定義 16.1.7（ポリマトロイドの階数関数）. $𝐸$ を有限集合とし， $𝐸$ の部分集合に実数を返す関数 $r k$ が次の三つを満たすとする．

$r k (\emptyset) = 0$ である．
$𝑆 \subseteq 𝑇 \subseteq 𝐸$ ならば $r k (𝑆) \leq r k (𝑇)$ である．
どの $𝑆, 𝑇 \subseteq 𝐸$ についても $r k (𝑆 \cup 𝑇) + r k (𝑆 \cap 𝑇) \leq r k (𝑆) + r k (𝑇)$ である．

このとき $r k$ を $𝐸$ 上の ポリマトロイドの階数関数 と呼ぶ．

系 16.1.8. 定義 16.1.1 の設定で， $𝑆$ に $𝐻 (𝑋 𝑆)$ を対応させる関数は ${1, \dots, 𝑛}$ 上のポリマトロイドの階数関数（定義 16.1.7）である．

証明. 定義 16.1.7 の第 $1$ の条件は， $𝑋 \emptyset$ のとりうる値が一つだから定義 1.1.1 より $𝐻 (𝑋 \emptyset) = 0$ であること，第 $2$ の条件は命題 16.1.5，第 $3$ の条件は定理 16.1.6 である． $◼$

形式化上の注記. 形式化はポリマトロイドを，階数関数と三つの条件を束ねた構造として持つ（Polymatroid (InformationTheory/Polymatroid/Basic.lean)．台となる集合に有限性を課していない点が定義 16.1.7 と違う）．部分集合のエントロピーからその構造を組み立てる entropyPolymatroid (InformationTheory/Shannon/Polymatroid.lean) もあるが，構造も，構造を組み立てる宣言も結論をもたないので，どちらも形式化ポインタには置かない．機械検証が及ぶのは三つの条件のほうで，第 $1$ の条件を jointEntropySubset_empty (InformationTheory/Shannon/Polymatroid.lean) が，第 $2$ と第 $3$ の条件を命題 16.1.5 と定理 16.1.6 に紐付けた宣言が検証している．

この枠に入るのはエントロピーだけではない．名前にある「マトロイド」は一次独立から来ていて，次の例がそのもとの姿である．

例 16.1.9（張る部分空間の次元）. $𝐸$ を実ベクトル空間の有限個のベクトルからなる集合とする． $𝑆 \subseteq 𝐸$ に $𝑆$ の元が張る部分空間の次元 $r k (𝑆)$ を対応させると， $r k$ は $𝐸$ 上のポリマトロイドの階数関数（定義 16.1.7）である．

証明. 第 $1$ の条件は，空集合が張る部分空間が零ベクトルだけからなり，その次元が $0$ であることによる．第 $2$ の条件は， $𝑆 \subseteq 𝑇$ ならば $𝑆$ の元が張る部分空間が $𝑇$ の元が張る部分空間に含まれ，含まれる側の次元が大きくならないことによる．

第 $3$ の条件を見る．一次独立なベクトルの組が，それを含む部分空間の基底に延ばせることと，部分空間を張るベクトルの本数がその部分空間の次元以上であることは，線形代数で既知とする． $𝑆, 𝑇 \subseteq 𝐸$ をとり， $𝑆 \cap 𝑇$ の元が張る部分空間の基底を一つとって $𝐵$ と書く． $𝐵$ は $𝑆$ の元が張る部分空間の中で一次独立だから， $𝑎$ 本のベクトルを足してその部分空間の基底にできる．同じように， $𝐵$ に $𝑏$ 本を足して $𝑇$ の元が張る部分空間の基底にできる． $r k (𝑆) = | 𝐵 | + 𝑎$ ， $r k (𝑇) = | 𝐵 | + 𝑏$ ， $r k (𝑆 \cap 𝑇) = | 𝐵 |$ である．ここで $𝑆 \cup 𝑇$ の元はどれも $𝑆$ か $𝑇$ に属するから，いま挙げた $| 𝐵 | + 𝑎 + 𝑏$ 本の一次結合で書ける．よって $𝑆 \cup 𝑇$ の元が張る部分空間はこの $| 𝐵 | + 𝑎 + 𝑏$ 本が張る部分空間に含まれ，部分空間が含まれれば次元は大きくならないから

r k (𝑆 \cup 𝑇) \leq | 𝐵 | + 𝑎 + 𝑏 = (| 𝐵 | + 𝑎) + (| 𝐵 | + 𝑏) - | 𝐵 | = r k (𝑆) + r k (𝑇) - r k (𝑆 \cap 𝑇)

である． $◼$

形式化上の注記. 線形代数の次元から定義 16.1.7 の三条件を作る宣言はない．ポリマトロイドの構造を結論に含む宣言を結論の形で探しても，部分集合のエントロピーから組み立てる entropyPolymatroid (InformationTheory/Shannon/Polymatroid.lean) しか見つからない．

そうすると， $𝐻 (𝑋 𝑆)$ について示すことのどこまでが値の出どころに依らないのかを問える．この問いには 16.3 節で答える（系 16.3.4）．次節の Han の不等式は， $(𝑛 - 1)$ 倍した全体のエントロピーを，番号を $1$ 個ずつ抜いた $𝑛$ 通りのエントロピーの和で上から押さえる不等式で，その証明が使うのは定理 16.1.4 のチェイン則と，補題 16.1.2 の読み替えと，定理 1.2.3 と定理 1.2.4 である．

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