InformationTheory 教科書（レビュー版）

Lean 4 + Mathlib で機械検証した定理に紐づけて書いている情報理論の教科書原稿です．「形式化」と添えた結果は無条件の検証済み定理に対応しています．宣言名はリンクになっていて，本のアイコンはその定理の解説ページ，GitHub のマークはソースへ飛びます．本文の証明は人間が読みやすい順序で書いているので，Lean がたどる証明ルートとは一致しません．保証されるのは定理の正しさであって，証明手順の一致ではありません．

• 第1章　エントロピー・相互情報量・データ処理不等式
  1. 1.1　エントロピー
  2. 1.2　結合エントロピー・条件付きエントロピーとチェイン則
  3. 1.3　相互情報量
  4. 1.4　条件付き相互情報量
  5. 1.5　エントロピー・相互情報量のチェイン則
  6. 1.6　情報不等式（Jensen と相対エントロピー）
  7. 1.7　対数和不等式
  8. 1.8　データ処理不等式
  9. 1.9　十分統計量
  10. 1.10　ファノの不等式
• 第2章　漸近等分配性とデータ圧縮
  1. 2.1　漸近等分配性
  2. 2.2　典型集合
  3. 2.3　情報源符号化定理
  4. 2.4　強典型性
• 第3章　定常情報源のエントロピーレート
  1. 3.1　定常情報源
  2. 3.2　エントロピーレート
  3. 3.3　マルコフ情報源のエントロピーレート
  4. 3.4　エルゴード性と時間平均
  5. 3.5　Shannon–McMillan–Breiman 定理
• 第4章　符号語長と最適符号
  1. 4.1　符号と一意復号可能性
  2. 4.2　Kraft の不等式
  3. 4.3　平均符号長の下界
  4. 4.4　Shannon 符号
  5. 4.5　McMillan の不等式
  6. 4.6　Huffman 符号の最適性
• 第5章　ギャンブルと情報
  1. 5.1　競馬と倍加率
  2. 5.2　比例賭けの最適性
  3. 5.3　倍加率とエントロピー
  4. 5.4　副情報の値打ち
  5. 5.5　資産の長時間のふるまい
• 第6章　通信路容量
  1. 6.1　通信路と通信路容量
  2. 6.2　ブロック通信路符号と結合典型集合
  3. 6.3　ランダム符号化と達成可能性
  4. 6.4　逆定理
  5. 6.5　フィードバックのある通信路
  6. 6.6　強逆定理
  7. 6.7　一般の通信路の容量
• 第7章　微分エントロピー
  1. 7.1　微分エントロピー
  2. 7.2　ガウス分布の微分エントロピー
  3. 7.3　アフィン変換と微分エントロピー
  4. 7.4　結合微分エントロピーと劣加法性
  5. 7.5　連続な相対エントロピーと相互情報量
• 第8章　ガウス通信路
  1. 8.1　ガウス通信路
  2. 8.2　ガウス通信路の容量
  3. 8.3　逆定理
  4. 8.4　達成可能性
  5. 8.5　帯域制限ガウス通信路
  6. 8.6　並列ガウス通信路と注水
• 第9章　レート歪み理論
  1. 9.1　歪みとレート歪み関数
  2. 9.2　レート歪み関数の性質
  3. 9.3　二値情報源
  4. 9.4　ガウス情報源と逆注水
  5. 9.5　逆定理
  6. 9.6　達成可能性
• 第10章　最大エントロピー
  1. 10.1　最大エントロピー問題
  2. 10.2　モーメント制約と Gibbs 分布
  3. 10.3　分配関数と Legendre 双対性
  4. 10.4　Lagrange 乗数の存在
• 第11章　仮説検定と大偏差
  1. 11.1　型と型類
  2. 11.2　型類の確率
  3. 11.3　Sanov の定理
  4. 11.4　仮説検定と Stein の補題
  5. 11.5　Bayes 誤り確率と Chernoff 情報
  6. 11.6　I 射影と誤りの指数のトレードオフ
• 第12章　万能符号
  1. 12.1　万能符号と冗長度
  2. 12.2　型による万能符号
  3. 12.3　ミニマックス冗長度と通信路容量
  4. 12.4　算術符号
  5. 12.5　Lempel–Ziv 符号
  6. 12.6　Lempel–Ziv 符号の最適性
• 第13章　コルモゴロフ複雑性
  1. 13.1　記述の長さと万能機械
  2. 13.2　圧縮できない対象と計算不可能性
  3. 13.3　複雑性とエントロピー
  4. 13.4　自己限定万能機械と万能確率
  5. 13.5　停止確率
  6. 13.6　二部記述と最小記述長
• 第14章　ネットワーク情報理論
  1. 14.1　多元接続通信路
  2. 14.2　多元接続通信路の容量領域
  3. 14.3　相関のある情報源の符号化
  4. 14.4　副情報つきレート歪み
  5. 14.5　ブロードキャスト通信路と重ね合わせ符号化
  6. 14.6　通信路のクラスと UV 外界
  7. 14.7　Marton の内界
  8. 14.8　中継通信路
• 第15章　ポートフォリオ理論
  1. 15.1　市場とポートフォリオ
  2. 15.2　対数最適ポートフォリオ
  3. 15.3　競争最適性
  4. 15.4　副情報の値打ち
  5. 15.5　i.i.d. 市場での長期のふるまい
  6. 15.6　定常エルゴード市場
  7. 15.7　記憶が伸びる戦略と $W_\infty$
  8. 15.8　万能ポートフォリオ
• 第16章　エントロピー不等式
  1. 16.1　部分集合のエントロピー
  2. 16.2　Han の不等式
  3. 16.3　Shearer の不等式
  4. 16.4　数え上げへの応用
  5. 16.5　超立方体の辺等周
  6. 16.6　行列式の不等式
  7. 16.7　エントロピーべきと Fisher 情報量
  8. 16.8　Stam の不等式とエントロピーべき不等式

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