16.5 超立方体の辺等周

面積を決めておいて周の長さをいちばん短くする図形は何か,と問うのが等周問題である.同じ問いを超立方体の頂点の上で立てるのが本節である.の二つの点は,ちょうど座標だけ違うときに辺で結ばれているとみる.頂点の集合を選ぶと,端点の一方だけがに入っている辺が決まり,その本数がの周にあたる.要素数を決めておいて,この本数がどこまで小さくなりうるかを問う.本節は下からの評価を二つ与えて二つを比べ,要素数がのべきであるときには最小値を決める.以下に固定し,の元はビットの列として書く.

定義 16.5.1(辺境界). とし,とする.とに対し,の第座標だけを反転して他の座標を変えない点をと書く.かつを満たす対の全体をと書き,の 辺境界 と呼ぶ.

は辺境界を表す記号であって,第10章 10.4 節 の偏微分とは別である(偏微分はつねに分数の形で関数に当たり,こちらはつねに添字を伴って集合に当たる).対と,端点の一方だけがに入る辺とは一対一に対応する.そのような辺について,に入っているほうの端点を,二つの端点が食い違う座標の番号をとすればよい.だからは「から外へ出ていく辺の本数」である.

形式化: edgeBoundaryCount (ソース)

注記

形式化は辺境界を集合としてではなく,その要素数として直に定めている(本文がと書く数がそれである).座標の反転にも flipCoord (InformationTheory/Shannon/HypercubeEdge/Boundary.lean) という名前が与えられている.

命題 16.5.2. とし,とする.との対のうちを満たすものの個数ととの和はに等しい.

証明. との対は,の選び方が通り,の選び方が通りで,全部で個ある.その各々についてはに入るか入らないかのどちらか一方だから,全体はを満たす対とを満たす対とに分かれる.後者の個数は 定義 16.5.1 よりである.◼

形式化: edge_total_count (ソース)

注記

形式化はを満たす対の個数にも internalEdgePairCount (InformationTheory/Shannon/HypercubeEdge/Boundary.lean) という名前を与えていて,宣言はその数と辺境界の要素数との和がに等しい,という形で述べられている.

以下,本節の主張ブロックではの底をにとる.立方体の次元とを同じ物差しで比べるためである.

定理 16.5.3(辺等周不等式). とし,を空でない集合とすると

|𝐴|(𝑛−log2⁡|𝐴|)≤|𝜕e𝐴|

である.

証明. のときはの元がただ一つではその一点だから,とより左辺はであり,対をとるがないので右辺もである.以下とする.

の上の一様分布に従う確率変数をとり,をの第座標とする.は 定義 16.1.1 の設定を満たす族である.はそのもので,とりうる値はの元だから,そのアルファベットをにとって 例 1.1.3 をで当てるとである.

まず上から押さえる.定理 16.1.4 をに当てるとである.はに含まれるから,補題 16.1.2 に注意して 定理 1.2.4 を当てると,各についてである.足し合わせると

𝑛∑𝑖=1𝐻(𝑋𝑖∣𝑋{1,…,𝑛}∖{𝑖})≤log2⁡|𝐴|

である.

次に左辺を数え直す.番号を固定し,のとる値を一つとる.の元で第座標以外がに一致するものは個か個で,個ならその二つは互いに第座標を反転した関係にある.のもとでの条件付きエントロピーを,この二つの場合に分けて見る.

  1. 個のとき.はの上で一様だから,のもとでのの条件付き分布はの上の一様分布である.例 1.1.3 をで当ててであり,このの確率はである.
  2. 個のとき.条件付き分布は一点に集中するから,定義 1.1.1 の和はの一項だけになり,値はである.

定義 1.2.2 は各のもとでの値をその確率で平均したものだから,寄与するのは個の場合のだけで,その寄与はひとつにつきである.そのようなひとつにはの元が個対応し,それらはちょうど,第座標を反転してもに留まるの元だから,そのようなの個数を倍したものが,そのような元の個数に等しい.したがって

𝐻(𝑋𝑖∣𝑋{1,…,𝑛}∖{𝑖})=|{𝑥∈𝐴:𝑥(𝑖)∈𝐴}||𝐴|

である.について足すと,分子の和はを満たす対の個数だから,命題 16.5.2 よりそれはである.前段の不等式と合わせて

𝑛|𝐴|−|𝜕e𝐴||𝐴|≤log2⁡|𝐴|

を得る.を両辺に掛けて整理すれば主張である.◼

形式化: edgeBoundary_entropy_sharp (ソース)

例 16.5.4(部分立方体). 𝑛 ≥0,とする.を要素数の座標の集合,をからへの関数とし,

𝐴:={𝑥∈{0,1}𝑛:𝑥𝑖=𝑐(𝑖)  (𝑖∈𝐹)}

とおく.このときかつであり,定理 16.5.3 は等号で成り立つ(図 16.5.1).

証明. の元はの外の個の座標を自由に選んで得られるからである.と座標をとる.ならばもの上でに一致するのでに属し,ならばの第座標はと違うのでに属さない.したがって外に出る対はのものに限り,その個数はである.一方だから 定理 16.5.3 の左辺はであり,両辺が一致する.◼

図 16.5.1. 𝑛 =3,𝑘 =2,𝐹 ={1},のときの部分立方体(塗った点,第座標がの点).から外へ出る辺は太線の本で,に等しい.

これで,節の冒頭の問いのうち要素数がのべきである場合には答えが出る.節の終わりに 系 16.5.9 としてまとめる.要素数がのべきでないときの最小値を,本書は与えない.

下界をもう一つ作っておく.前節の 定理 16.4.2 は,集合の要素数を射影の要素数で上から押さえる不等式だった.辺境界も射影の要素数で書けるので(命題 16.5.6),同じ不等式をこの節に持ち込める.そうして出る下界を 定理 16.5.3 と比べれば,二つの道の差が数で見える.持ち込むには,個の非負の数の積の乗根が相加平均を超えないという古典的な不等式が要る.本書はこれを 補題 1.1.9 から証明するので,借用ではない.

補題 16.5.5(相加相乗平均の不等式). とし,を非負の実数とすると

(𝑛∏𝑖=1𝑡𝑖)1/𝑛≤1𝑛𝑛∑𝑖=1𝑡𝑖

である.

証明. どれかのがならば左辺はであり,右辺は非負だから成り立つ.以下すべてのが正であるとする.補題 1.1.6 のとおりはの上で狭義凹だから,補題 1.1.9 を,重み,点ととって当てると

1𝑛𝑛∑𝑖=1log⁡𝑡𝑖≤log⁡(1𝑛𝑛∑𝑖=1𝑡𝑖)

である.左辺はに等しい.が狭義単調だから主張を得る.◻

形式化上の注記

この補題だけを述べる宣言はない.積の乗根を相加平均で押さえる形で InformationTheory/ の全体を探しても見つからず,形式化は同じ内容を重みつきの一般形として Mathlib から直に引いている.定理 16.5.7 と 定理 16.6.1 に紐付けた宣言が,それぞれその中でこれを使っている.

命題 16.5.6. とし,とすると

|𝜕e𝐴|+𝑛|𝐴|=2𝑛∑𝑖=1|𝜋−𝑖(𝐴)|

である(は 定義 16.4.1 の射影である).

証明. 番号を固定する.に対し,の元で第座標以外がに一致するものは個か個である.個であるようなの個数を,個であるようなの個数をと書くと,の元はこの二種類に分かれるからであり,の元をこの分け方で数えてである.またの第座標以外を切り詰めたものをと書くと,であることとが個のほうであることとは同じことだから,第座標の向きに外へ出る対の個数はである.よって

𝑎𝑖+|𝐴|=𝑎𝑖+(𝑎𝑖+2𝑏𝑖)=2|𝜋−𝑖(𝐴)|

である.について足すと,左辺の第項の和は,第項の和はだから主張を得る.◼

形式化: edgeBoundary_count_eq (ソース)

命題 16.5.6 は,辺境界を射影の要素数の言葉に書き換える.そこに 定理 16.4.2 を当てれば,もう一つの下界が出る.正の整数に対しがの上で単調非減少であること(の逆写像である)と,正の実数のべき乗の規則,すなわち正の実数,と実数,について,𝑢𝜅+𝜏 =𝑢𝜅𝑢𝜏,が成り立つことを既知とする.単調性を使うのは 定理 16.5.7 の証明と 例 16.6.2 の二箇所で,べき乗の規則を使うのは,本節と次節が乗を積や積のべきに通すところである.

定理 16.5.7. とし,を空でない集合とすると

2𝑛|𝐴|(𝑛−1)/𝑛−𝑛|𝐴|≤|𝜕e𝐴|

である.

証明. 補題 16.5.5 をととって当てると

𝑛∑𝑖=1|𝜋−𝑖(𝐴)|≥𝑛(𝑛∏𝑖=1|𝜋−𝑖(𝐴)|)1/𝑛

である.として 定理 16.4.2 を当てるとであり,乗が単調非減少だから右辺は以上である.命題 16.5.6 と合わせるとであり,移項すれば主張を得る.◼

形式化: edgeBoundary_ge_AMGM (ソース)

注記

宣言は移項する前の形(2𝑛|𝐴|(𝑛−1)/𝑛 ≤|𝜕e𝐴| +𝑛|𝐴|)で述べられている.指数は 定理 16.4.2 の宣言と同じく自然数の引き算で書かれていてでも両辺が定まる.本文がを仮定するのは,を分数として読むためである.

下界が二つ出たので,どちらが強いかを決めておく.

命題 16.5.8. とし,を空でない集合とすると

2𝑛|𝐴|(𝑛−1)/𝑛−𝑛|𝐴|≤|𝐴|(𝑛−log2⁡|𝐴|)

である.すなわち 定理 16.5.3 の下界は 定理 16.5.7 の下界以上である.等号が成り立つのはのときとのときに限る.

証明. は空でなくに含まれるからであり,とおくとである.だからであり,

2𝑛|𝐴|(𝑛−1)/𝑛−𝑛|𝐴|=2𝑛|𝐴||𝐴|−1/𝑛−𝑛|𝐴|=𝑛|𝐴|(2𝑠−1),|𝐴|(𝑛−log2⁡|𝐴|)=𝑛|𝐴|𝑠

である.だから,示すべきはに対するである.補題 1.1.6 のとおりは狭義凹だから,補題 1.1.9 を,点と,重みとととって当てると

log2⁡(1+𝑠)=log2⁡((1−𝑠)⋅1+𝑠⋅2)≥(1−𝑠)log2⁡1+𝑠log2⁡2=𝑠

である.でありは狭義単調だから,を得る.等号については,のときは 補題 1.1.9 の重みが二つとも正で点とが違うから狭義であり,とのときは重みの一方がで等号である.は,はにあたる.◼

形式化上の注記

二つの下界の強弱を述べる宣言はない.辺境界の要素数を結論に含む宣言をすべて開いて確かめた.機械検証が及ぶのは 定理 16.5.3 と 定理 16.5.7 のそれぞれまでで,二つを比べる段は本文の側にある.

二つの下界を数で比べる. とし,を個の座標を固定して得られる点の部分立方体にとる.例 16.5.4 よりである.定理 16.5.3 の下界はで真の値に一致し,定理 16.5.7 の下界はで,ほど届かない.両端では二つは一致する.ではどちらも,ではどちらもである.

二つの下界は道が違う.弱いほうの 定理 16.5.7 は,命題 16.5.6 で辺境界を射影の要素数に書き換えてから 定理 16.4.2 と 補題 16.5.5 に渡すので,本節の側で見ているのは要素数だけである(定理 16.4.2 自身の証明は 定理 16.3.1 を通るので,エントロピーを使わずに済むわけではない).強いほうの 定理 16.5.3 は,射影を経由せずに 定理 16.1.4 の分解を立方体の上でそのまま使い,座標だけを残したときの条件付きエントロピーが,条件の値ごとにかしかとらないことを数え上げに直す.射影を経由しないほうが弱くならない下界を出し,両端のとを除けば真に強い,というのが二つを比べた結果である.

強いほうの下界は,要素数がのべきであるときにはとられる.節の冒頭の問いの答えは,そこから出る.

系 16.5.9(辺境界の最小値). とし,をを満たす整数とする.を満たすを動かすとき,の最小値はである.

証明. は正だからは空でなく,だから,そのようなのどれについても 定理 16.5.3 はを与える.いっぽうだから,要素数の座標の集合と,そこからへの関数を一つずつとって 例 16.5.4 を当てることができ,そこで作った部分立方体は要素数がで,その辺境界の要素数はちょうどである.よっては下界であり,かつとられる.◼

形式化上の注記

要素数を固定したときの辺境界の最小値を述べる宣言はない.結論の形で探しても,最小値を述べるものも,例 16.5.4 の部分立方体を作る宣言も見つからない.機械検証が及ぶのは 定理 16.5.3 の下界までで,その値がとられることを言う段は本文の側にある.

次節は 補題 16.5.5 のほうをもう一度使う.当てる相手は集合の要素数ではなく,行列の行列式である.

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