From 16f5627f1f7db3371c10912837a6cb143be1b533 Mon Sep 17 00:00:00 2001 From: wurtylex Date: Fri, 28 Aug 2026 09:59:58 -0700 Subject: [PATCH] ported everything over from leanecc (relevanent to gbv) --- Cslib.lean | 3 + .../CodingTheory/Bounds/GilbertVarshamov.lean | 176 ++++++++++++++ Cslib/CodingTheory/Code/Defs.lean | 151 ++++++++++++ Cslib/CodingTheory/HammingBall.lean | 223 ++++++++++++++++++ 4 files changed, 553 insertions(+) create mode 100644 Cslib/CodingTheory/Bounds/GilbertVarshamov.lean create mode 100644 Cslib/CodingTheory/Code/Defs.lean create mode 100644 Cslib/CodingTheory/HammingBall.lean diff --git a/Cslib.lean b/Cslib.lean index 1d0469a56b..d3a7f93d70 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -3,6 +3,9 @@ module -- shake: keep-all --deprecated_module: ignore public import Cslib.Algorithms.CCS.VendingMachine public import Cslib.Algorithms.Lean.MergeSort.MergeSort public import Cslib.Algorithms.Lean.TimeM +public import Cslib.CodingTheory.Bounds.GilbertVarshamov +public import Cslib.CodingTheory.Code.Defs +public import Cslib.CodingTheory.HammingBall public import Cslib.Computability.Automata.Acceptors.Acceptor public import Cslib.Computability.Automata.Acceptors.OmegaAcceptor public import Cslib.Computability.Automata.DA.Basic diff --git a/Cslib/CodingTheory/Bounds/GilbertVarshamov.lean b/Cslib/CodingTheory/Bounds/GilbertVarshamov.lean new file mode 100644 index 0000000000..43d5641204 --- /dev/null +++ b/Cslib/CodingTheory/Bounds/GilbertVarshamov.lean @@ -0,0 +1,176 @@ +/- +Copyright (c) 2026 Anthony Chang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anthony Chang, Alex Chai, Erin Jaen +-/ + +module + +public import Cslib.CodingTheory.Code.Defs +public import Cslib.CodingTheory.HammingBall +public import Mathlib.Data.Set.Card.Arithmetic + +/-! +# The Gilbert–Varshamov bound + +This file proves the Gilbert–Varshamov bound for general (not necessarily linear) codes. + +## References + +* V. Guruswami, A. Rudra, M. Sudan, *Essential Coding Theory* (draft, 2023), + +-/ + +@[expose] public section + +namespace Cslib.CodingTheory.Code + +open scoped ENNReal + +variable {α : Type*} {n : ℕ} [DecidableEq α] + +/-- If `C` is maximal with respect to inclusion among the codes of minimum distance at least `d`, +then the Hamming balls of radius `d - 1` around its codewords cover the whole space: a word `z` +outside all of them would be at distance at least `d` from every codeword, so that `insert z C` +would still have minimum distance at least `d`, contradicting maximality. -/ +lemma iUnion_hammingBall_eq_univ_of_maximal {d : ℕ} {C : Code α n} + (hC : Maximal (fun D : Code α n => (d : ℕ∞) ≤ D.minDist) C) : + ⋃ c ∈ C, hammingBall c (d - 1) = Set.univ := by + refine Set.eq_univ_of_forall fun z => ?_ + by_contra hz + simp only [Set.mem_iUnion, mem_hammingBall, not_exists, not_le] at hz + -- every codeword is at distance at least `d` from `z` + have hdist : ∀ c ∈ C, (d : ℕ∞) ≤ (hammingDist c z : ℕ∞) := fun c hc => by + have := hz c hc + exact_mod_cast (by omega : d ≤ hammingDist c z) + -- so `z` can be added to `C` without decreasing the minimum distance below `d`, hence `z ∈ C` + have hsub : insert z C ⊆ C := + hC.le_of_ge (le_minDist_insert hC.prop hdist) (Set.subset_insert z C) + simpa using hz z (hsub (Set.mem_insert z C)) + +/-- Over a finite alphabet, there is a code that is maximal with respect to inclusion among the +codes of minimum distance at least `d`: the family of such codes is finite and nonempty (it +contains the empty code). -/ +lemma exists_maximal_le_minDist [Finite α] (d : ℕ∞) : + ∃ C : Code α n, Maximal (fun D : Code α n => d ≤ D.minDist) C := + (Set.toFinite {D : Code α n | d ≤ D.minDist}).exists_maximal ⟨∅, by simp [minDist]⟩ + +variable [Fintype α] + +/-- Packing bound: if `C` is maximal with respect to inclusion among the codes of minimum +distance at least `d`, then `q ^ n ≤ |C| · Vol_q(n, d - 1)` (where `q = |α|`), since the `|C|` +Hamming balls of radius `d - 1` around the codewords cover the `q ^ n` words. -/ +lemma card_pow_le_ncard_mul_hammingVolume_of_maximal {d : ℕ} {C : Code α n} + (hC : Maximal (fun D : Code α n => (d : ℕ∞) ≤ D.minDist) C) : + Fintype.card α ^ n ≤ C.ncard * hammingVolume (Fintype.card α) n (d - 1) := by + have hfin : C.Finite := Set.toFinite C + calc Fintype.card α ^ n + = (Set.univ : Set (Fin n → α)).ncard := by simp + _ = (⋃ c ∈ hfin.toFinset, hammingBall c (d - 1)).ncard := by + rw [← iUnion_hammingBall_eq_univ_of_maximal hC] + simp only [Set.Finite.mem_toFinset] + _ ≤ ∑ c ∈ hfin.toFinset, (hammingBall c (d - 1)).ncard := + hfin.toFinset.set_ncard_biUnion_le _ + _ = ∑ _c ∈ hfin.toFinset, hammingVolume (Fintype.card α) n (d - 1) := + Finset.sum_congr rfl fun c _ => ncard_hammingBall c (d - 1) + _ = C.ncard * hammingVolume (Fintype.card α) n (d - 1) := by + rw [Finset.sum_const, smul_eq_mul, Set.ncard_eq_toFinset_card C hfin] + +/-- Gilbert–Varshamov bound, combinatorial form: for every `d` there is a code of minimum +distance at least `d` with `q ^ n ≤ |C| · Vol_q(n, d - 1)`, where `q = |α|`. -/ +theorem gilbert_varshamov_ncard (d : ℕ) : + ∃ C : Code α n, (d : ℕ∞) ≤ C.minDist ∧ + Fintype.card α ^ n ≤ C.ncard * hammingVolume (Fintype.card α) n (d - 1) := by + obtain ⟨C, hC⟩ := exists_maximal_le_minDist (α := α) (n := n) d + exact ⟨C, hC.prop, card_pow_le_ncard_mul_hammingVolume_of_maximal hC⟩ + +/-- Gilbert–Varshamov bound: over an alphabet of size `q ≥ 2`, for every `0 ≤ δ < 1 - 1 / q` +and every block length `n ≥ 1` there is a code of rate at least `1 - H_q(δ)` and relative minimum +distance at least `δ`. Here `H_q` is the `q`-ary entropy function `Real.qaryEntropy`, which is +measured in nats, hence the division by `log q`. -/ +theorem gilbert_varshamov (hq : 2 ≤ Fintype.card α) (hn : 1 ≤ n) {δ : ℝ} (hδ0 : 0 ≤ δ) + (hδ1 : δ < 1 - 1 / (Fintype.card α : ℝ)) : + ∃ C : Code α n, + 1 - Real.qaryEntropy (Fintype.card α) δ / Real.log (Fintype.card α) ≤ C.rate ∧ + ENNReal.ofReal δ ≤ C.relMinDist := by + set q : ℕ := Fintype.card α + have hq1 : (1 : ℝ) < q := by exact_mod_cast Nat.lt_of_lt_of_le one_lt_two hq + have hq0 : (0 : ℝ) < q := one_pos.trans hq1 + have hn0 : (0 : ℝ) < n := by exact_mod_cast hn + -- the designed distance `d = max ⌈δ n⌉ 1` + set d : ℕ := max ⌈δ * n⌉₊ 1 with hd_def + have hδnd : δ * n ≤ (d : ℝ) := + calc δ * n ≤ (⌈δ * n⌉₊ : ℝ) := Nat.le_ceil _ + _ ≤ (d : ℝ) := by exact_mod_cast le_max_left _ _ + obtain ⟨C, hCd, hCcard⟩ := gilbert_varshamov_ncard (α := α) (n := n) d + -- the packing radius `r = d - 1` satisfies `r ≤ δ n`, hence `r / n ≤ δ < 1 - 1 / q` + set r : ℕ := d - 1 with hr_def + have hrδn : (r : ℝ) ≤ δ * n := by + rcases Nat.eq_zero_or_pos ⌈δ * n⌉₊ with h | h + -- if `⌈δ n⌉ = 0` then `r = 0` and the claim is `0 ≤ δ n` + · have hr0 : r = 0 := by omega + rw [hr0, Nat.cast_zero] + exact mul_nonneg hδ0 hn0.le + -- otherwise `r = ⌈δ n⌉ - 1 < ⌈δ n⌉`, which means `r < δ n` + · have hrlt : r < ⌈δ * n⌉₊ := by omega + exact (Nat.lt_ceil.mp hrlt).le + have hrn_le_δ : (r : ℝ) / n ≤ δ := by + rw [div_le_iff₀ hn0] + exact hrδn + have hrange : (r : ℝ) / n ≤ 1 - 1 / (q : ℝ) := hrn_le_δ.trans hδ1.le + set H : ℝ := Real.qaryEntropy q ((r : ℝ) / n) + have hVol : (hammingVolume q n r : ℝ) ≤ (q : ℝ) ^ ((n : ℝ) * H / Real.log q) := + hammingVolume_le_pow_mul_entropy hq hn hrange + -- the packing bound forces `C` to be nonempty, so its cardinality is positive + have hncard : (0 : ℝ) < (C.ncard : ℝ) := by + have : 0 < C.ncard := by + rcases Nat.eq_zero_or_pos C.ncard with h0 | h0 + · rw [h0, zero_mul] at hCcard + exact absurd hCcard (not_le.mpr (pow_pos (by omega) n)) + · exact h0 + exact_mod_cast this + -- the packing bound in `ℝ`: `q ^ n ≤ |C| · Vol_q(n, r)` + have hcardR : (q : ℝ) ^ (n : ℝ) ≤ (C.ncard : ℝ) * (hammingVolume q n r : ℝ) := by + rw [Real.rpow_natCast] + exact_mod_cast hCcard + -- hence `|C| ≥ q ^ (n - n H / log q)` + have key : (q : ℝ) ^ ((n : ℝ) - (n : ℝ) * H / Real.log q) ≤ (C.ncard : ℝ) := by + rw [Real.rpow_sub hq0, div_le_iff₀ (Real.rpow_pos_of_pos hq0 _)] + calc (q : ℝ) ^ (n : ℝ) + ≤ (C.ncard : ℝ) * (hammingVolume q n r : ℝ) := hcardR + _ ≤ (C.ncard : ℝ) * (q : ℝ) ^ ((n : ℝ) * H / Real.log q) := + mul_le_mul_of_nonneg_left hVol hncard.le + -- taking `logb q`, the dimension is at least `n - n H / log q` + have hdim : (n : ℝ) - (n : ℝ) * H / Real.log q ≤ C.dim := by + have hlog := Real.logb_le_logb_of_le hq1 (Real.rpow_pos_of_pos hq0 _) key + rwa [Real.logb_rpow hq0 hq1.ne'] at hlog + -- so the rate is at least `1 - H / log q` + have hrate1 : 1 - H / Real.log q ≤ C.rate := by + change 1 - H / Real.log q ≤ C.dim / n + rw [le_div_iff₀ hn0] + calc (1 - H / Real.log q) * n = n - n * H / Real.log q := by ring + _ ≤ C.dim := hdim + -- monotonicity of the entropy on `[0, 1 - 1 / q]` turns `H_q(r / n)` into `H_q(δ)` + have hmono : H ≤ Real.qaryEntropy q δ := + (Real.qaryEntropy_strictMonoOn hq).monotoneOn + (Set.mem_Icc.mpr ⟨by positivity, hrange⟩) + (Set.mem_Icc.mpr ⟨hδ0, hδ1.le⟩) hrn_le_δ + have hrate : 1 - Real.qaryEntropy q δ / Real.log q ≤ C.rate := by + refine le_trans ?_ hrate1 + gcongr + -- the relative minimum distance is at least `d / n ≥ δ` + have hdist : ENNReal.ofReal δ ≤ C.relMinDist := by + change ENNReal.ofReal δ ≤ (C.minDist : ℝ≥0∞) / (n : ℝ≥0∞) + refine le_trans ?_ (ENNReal.div_le_div_right (ENat.toENNReal_le.mpr hCd) _) + rw [ENNReal.le_div_iff_mul_le (Or.inl (by exact_mod_cast (by omega : n ≠ 0))) + (Or.inl (ENNReal.natCast_ne_top n))] + calc ENNReal.ofReal δ * (n : ℝ≥0∞) + = ENNReal.ofReal (δ * n) := by + rw [← ENNReal.ofReal_natCast n, ← ENNReal.ofReal_mul hδ0] + _ ≤ ENNReal.ofReal (d : ℝ) := ENNReal.ofReal_le_ofReal hδnd + _ = ((d : ℕ∞) : ℝ≥0∞) := by + rw [ENNReal.ofReal_natCast d] + exact_mod_cast rfl + exact ⟨C, hrate, hdist⟩ + +end Cslib.CodingTheory.Code diff --git a/Cslib/CodingTheory/Code/Defs.lean b/Cslib/CodingTheory/Code/Defs.lean new file mode 100644 index 0000000000..0c996fe36a --- /dev/null +++ b/Cslib/CodingTheory/Code/Defs.lean @@ -0,0 +1,151 @@ +/- +Copyright (c) 2026 Anthony Chang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anthony Chang, Alex Chai, Erin Jaen +-/ + +module + +public import Cslib.Init +public import Mathlib.Analysis.SpecialFunctions.Log.Base +public import Mathlib.Data.ENat.Lattice +public import Mathlib.Data.Real.ENatENNReal +public import Mathlib.Data.Set.Card +public import Mathlib.InformationTheory.Hamming + +/-! +# Codes + +This file defines (block) codes and some basic properties. + +A code of block length `n` over an alphabet `α` is a set of words `Fin n → α`, called its +codewords. Its main parameters are its dimension `log_q |C|` (where `q = |α|` is the size of +the alphabet, assumed finite), its rate `dim C / n`, its minimum distance (the least Hamming +distance between two distinct codewords) and its relative minimum distance `minDist C / n`. + +## References + +* V. Guruswami, A. Rudra, M. Sudan, *Essential Coding Theory* (draft, 2023), + +-/ + +@[expose] public section + +namespace Cslib.CodingTheory + +open scoped ENNReal + +/-- A *code* of block length `n` over the alphabet `α` is a set of words of length `n` over `α`; +its elements are the *codewords*. -/ +abbrev Code (α : Type*) (n : ℕ) := Set (Fin n → α) + +namespace Code + +variable {α : Type*} {n : ℕ} + +section MinDist + +variable [DecidableEq α] + +/-- The minimum distance of a code: the least Hamming distance between two distinct codewords. +It is `⊤` if the code has fewer than two codewords. -/ +noncomputable def minDist (C : Code α n) : ℕ∞ := + ⨅ c₁ ∈ C, ⨅ c₂ ∈ C, ⨅ _ : c₁ ≠ c₂, (hammingDist c₁ c₂ : ℕ∞) + +/-- The minimum distance is a lower bound for the distance between any two distinct codewords. -/ +lemma minDist_le_hammingDist {C : Code α n} {c₁ c₂ : Fin n → α} + (h₁ : c₁ ∈ C) (h₂ : c₂ ∈ C) (hne : c₁ ≠ c₂) : + C.minDist ≤ (hammingDist c₁ c₂ : ℕ∞) := by + unfold minDist + exact (iInf₂_le c₁ h₁).trans <| (iInf₂_le c₂ h₂).trans (iInf_le _ hne) + +/-- The minimum distance is the greatest lower bound for the distances between distinct +codewords. -/ +lemma le_minDist {C : Code α n} {m : ℕ∞} + (h : ∀ c₁ ∈ C, ∀ c₂ ∈ C, c₁ ≠ c₂ → m ≤ (hammingDist c₁ c₂ : ℕ∞)) : + m ≤ C.minDist := by + simp only [minDist, le_iInf_iff] + exact h + +/-- The minimum distance of any code is at least `1`: distinct codewords are at positive +distance, and the empty infimum is `⊤`. -/ +lemma one_le_minDist (C : Code α n) : 1 ≤ C.minDist := + le_minDist fun c₁ _ c₂ _ hne => by + have : hammingDist c₁ c₂ ≠ 0 := fun h => hne (by simpa using h) + exact_mod_cast Nat.one_le_iff_ne_zero.mpr this + +/-- The minimum distance is antitone: enlarging a code cannot increase its minimum distance. -/ +lemma minDist_anti {C D : Code α n} (h : C ⊆ D) : D.minDist ≤ C.minDist := + le_minDist fun _ hc₁ _ hc₂ hne => minDist_le_hammingDist (h hc₁) (h hc₂) hne + +/-- If `C` has minimum distance at least `d` and every codeword of `C` is at distance at least `d` +from the word `c`, then `insert c C` still has minimum distance at least `d`. -/ +lemma le_minDist_insert {C : Code α n} {c : Fin n → α} {d : ℕ∞} (hC : d ≤ C.minDist) + (hc : ∀ x ∈ C, d ≤ (hammingDist x c : ℕ∞)) : d ≤ minDist (insert c C) := by + refine le_minDist fun c₁ hc₁ c₂ hc₂ hne => ?_ + rcases Set.mem_insert_iff.mp hc₁ with rfl | h₁ + · rcases Set.mem_insert_iff.mp hc₂ with rfl | h₂ + · exact absurd rfl hne + · rw [hammingDist_comm] + exact hc c₂ h₂ + · rcases Set.mem_insert_iff.mp hc₂ with rfl | h₂ + · exact hc c₁ h₁ + · exact hC.trans (minDist_le_hammingDist h₁ h₂ hne) + +/-- The minimum distance of a code `{x, y}` with two distinct codewords is `hammingDist x y`. -/ +lemma minDist_pair {x y : Fin n → α} (hxy : x ≠ y) : + minDist ({x, y} : Code α n) = hammingDist x y := + le_antisymm + (minDist_le_hammingDist (Set.mem_insert x {y}) (Set.mem_insert_of_mem x rfl) hxy) + (le_minDist <| by + -- each codeword is `x` or `y`, and they are distinct + rintro c₁ (rfl | rfl) c₂ (rfl | rfl) hne + · exact absurd rfl hne + · exact le_rfl + · exact_mod_cast (hammingDist_comm _ _).le + · exact absurd rfl hne) + +/-- The relative minimum distance `minDist C / n` of a code, as an element of `ℝ≥0∞`. -/ +noncomputable def relMinDist (C : Code α n) : ℝ≥0∞ := (C.minDist : ℝ≥0∞) / n + +end MinDist + +section Dim + +variable [Fintype α] + +/-- The dimension `log_q |C|` of a code (a real number), where `q = |α|` is the size of the +alphabet. -/ +noncomputable def dim (C : Code α n) : ℝ := Real.logb (Fintype.card α) C.ncard + +/-- The rate `dim C / n` of a code (with the convention that it is `0` if `n = 0`). -/ +noncomputable def rate (C : Code α n) : ℝ := C.dim / n + +/-- The dimension of a code is at most its block length. -/ +lemma dim_le_n (C : Code α n) : C.dim ≤ n := by + obtain h0 | hpos := Nat.eq_zero_or_pos C.ncard + · -- the empty code: `dim C = logb q 0 = 0` + simp [dim, h0] + obtain hq | hq := Nat.lt_or_ge (Fintype.card α) 2 + · -- degenerate alphabet: the base of the logarithm is `0` or `1`, so `dim C = 0` + rcases (by omega : Fintype.card α = 0 ∨ Fintype.card α = 1) with h | h <;> simp [dim, h] + · -- `2 ≤ q`: apply `logb q` to `|C| ≤ q ^ n` + have hq1 : (1 : ℝ) < Fintype.card α := by exact_mod_cast hq + have hcard : (C.ncard : ℝ) ≤ (Fintype.card α : ℝ) ^ n := by + have h := Set.ncard_le_ncard (Set.subset_univ C) + simp only [Set.ncard_univ, Nat.card_eq_fintype_card, Fintype.card_fun, + Fintype.card_fin] at h + exact_mod_cast h + calc C.dim ≤ Real.logb (Fintype.card α) ((Fintype.card α : ℝ) ^ n) := + Real.logb_le_logb_of_le hq1 (by exact_mod_cast hpos) hcard + _ = n := by rw [Real.logb_pow, Real.logb_self_eq_one hq1, mul_one] + +/-- The rate of a code is at most `1`. -/ +lemma rate_le_one (C : Code α n) : C.rate ≤ 1 := + div_le_one_of_le₀ C.dim_le_n (by positivity) + +end Dim + +end Code + +end Cslib.CodingTheory diff --git a/Cslib/CodingTheory/HammingBall.lean b/Cslib/CodingTheory/HammingBall.lean new file mode 100644 index 0000000000..8be8fad18c --- /dev/null +++ b/Cslib/CodingTheory/HammingBall.lean @@ -0,0 +1,223 @@ +/- +Copyright (c) 2026 Anthony Chang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Anthony Chang, Alex Chai, Erin Jaen +-/ + +module + +public import Cslib.Init +public import Mathlib.Analysis.SpecialFunctions.BinaryEntropy +public import Mathlib.Data.Fintype.BigOperators +public import Mathlib.Data.Set.Card +public import Mathlib.InformationTheory.Hamming +import all Mathlib.Analysis.SpecialFunctions.BinaryEntropy + +/-! +# Hamming balls and their volume + +We define Hamming balls and their volumes in this file. +Hamming balls are essential for combinatorial bounds in coding theory. + +## References + +* V. Guruswami, A. Rudra, M. Sudan, *Essential Coding Theory* (draft, 2023), + +-/ + +@[expose] public section + +namespace Cslib.CodingTheory + +open Finset + +/-- The volume `Vol_q(n, r) = ∑_{i = 0}^{r} C(n, i) (q - 1) ^ i` of a Hamming ball of radius +`r` in the space of words of length `n` over an alphabet of size `q`. -/ +def hammingVolume (q n r : ℕ) : ℕ := ∑ i ∈ range (r + 1), n.choose i * (q - 1) ^ i + +@[simp] +lemma hammingVolume_zero (q n : ℕ) : hammingVolume q n 0 = 1 := by simp [hammingVolume] + +lemma hammingVolume_pos (q n r : ℕ) : 0 < hammingVolume q n r := + sum_pos' (fun _ _ => Nat.zero_le _) ⟨0, mem_range.mpr r.succ_pos, by simp⟩ + +/-- For `2 ≤ q` and `1 ≤ n`, the volume of a Hamming ball of radius `r ≤ (1 - 1 / q) n` is at +most `q ^ (n H_q(r / n))`, where `H_q` is the `q`-ary entropy function `Real.qaryEntropy` (which +is measured in nats, hence the division by `log q`). -/ +lemma hammingVolume_le_pow_mul_entropy {q n r : ℕ} (hq : 2 ≤ q) (hn : 1 ≤ n) + (hr : (r : ℝ) / n ≤ 1 - 1 / q) : + (hammingVolume q n r : ℝ) ≤ + (q : ℝ) ^ ((n : ℝ) * Real.qaryEntropy q ((r : ℝ) / n) / Real.log q) := by + -- if `r = 0` then the volume is `1` and the exponent vanishes + obtain rfl | hr0 := Nat.eq_zero_or_pos r + · simp + -- write `l = r / n`; then `0 < l ≤ 1 - 1 / q < 1` + set l : ℝ := (r : ℝ) / n with hl + have hn0 : (0 : ℝ) < n := by exact_mod_cast hn + have hq0 : (0 : ℝ) < q := by positivity + have hl0 : 0 < l := div_pos (by exact_mod_cast hr0) hn0 + have hl1 : l < 1 := hr.trans_lt (sub_lt_self 1 (by positivity)) + have h1l : 0 < 1 - l := sub_pos.mpr hl1 + have hql : (0 : ℝ) < (q : ℝ) - 1 := sub_pos.mpr (by exact_mod_cast hq) + have hrn : r < n := by exact_mod_cast (div_lt_one hn0).mp hl1 + -- as `n l = r`, the definition of `H_q` gives + -- `n H_q(l) = r log (q - 1) + r log l⁻¹ + (n - r) log (1 - l)⁻¹` + have hnl : (n : ℝ) * l = r := by rw [hl, mul_comm, div_mul_cancel₀ _ hn0.ne'] + have hent : (n : ℝ) * Real.qaryEntropy q l + = (r : ℝ) * Real.log ((q : ℝ) - 1) + + ((r : ℝ) * Real.log l⁻¹ + ((n - r : ℕ) : ℝ) * Real.log (1 - l)⁻¹) := by + simp only [Real.qaryEntropy, Real.binEntropy] + push_cast [Nat.cast_sub hrn.le] + rw [← hnl] + ring + -- as `1 < q`, `q ^ (x / log q) = exp x` + have hexp : (q : ℝ) ^ ((n : ℝ) * Real.qaryEntropy q l / Real.log q) + = Real.exp ((n : ℝ) * Real.qaryEntropy q l) := by + rw [Real.rpow_def_of_pos hq0, mul_comm (Real.log _), + div_mul_cancel₀ _ (Real.log_pos (by exact_mod_cast hq)).ne'] + -- so `q ^ (n H_q(l) / log q) = (q - 1) ^ r / (l ^ r (1 - l) ^ (n - r))` + have hRHS : Real.exp ((n : ℝ) * Real.qaryEntropy q l) + = ((q : ℝ) - 1) ^ r / (l ^ r * (1 - l) ^ (n - r)) := by + rw [hent, Real.exp_add, Real.exp_add, Real.exp_nat_mul, Real.exp_nat_mul, + Real.exp_nat_mul, Real.exp_log hql, Real.exp_log (inv_pos.mpr hl0), + Real.exp_log (inv_pos.mpr h1l), inv_pow, inv_pow, ← mul_inv, ← div_eq_mul_inv] + -- hence it suffices to show `Vol_q(n, r) l ^ r (1 - l) ^ (n - r) ≤ (q - 1) ^ r` + rw [hexp, hRHS, le_div_iff₀ (by positivity)] + -- with `θ = l / ((q - 1) (1 - l))`, the hypothesis `l ≤ 1 - 1 / q` says exactly `θ ≤ 1` + have htheta : l ≤ ((q : ℝ) - 1) * (1 - l) := by + have h : l * q ≤ (q : ℝ) - 1 := + calc l * q ≤ (1 - 1 / (q : ℝ)) * q := mul_le_mul_of_nonneg_right hr hq0.le + _ = q - 1 := by field_simp + calc l = l * q - l * ((q : ℝ) - 1) := by ring + _ ≤ ((q : ℝ) - 1) - l * ((q : ℝ) - 1) := sub_le_sub_right h _ + _ = ((q : ℝ) - 1) * (1 - l) := by ring + -- the binomial theorem: `∑_{i ≤ n} C(n, i) l ^ i (1 - l) ^ (n - i) = (l + (1 - l)) ^ n = 1` + have hbinom : + ∑ i ∈ range (n + 1), l ^ i * (1 - l) ^ (n - i) * (n.choose i : ℝ) = 1 := by + rw [← add_pow, add_sub_cancel, one_pow] + calc (hammingVolume q n r : ℝ) * (l ^ r * (1 - l) ^ (n - r)) + = ∑ i ∈ range (r + 1), + (n.choose i : ℝ) * ((q : ℝ) - 1) ^ i * (l ^ r * (1 - l) ^ (n - r)) := by + rw [hammingVolume, Nat.cast_sum, sum_mul] + refine sum_congr rfl fun i _ => ?_ + push_cast [Nat.cast_sub (show 1 ≤ q by omega)] + ring + -- for `i ≤ r`, the `i`-th term is `(q - 1) ^ r C(n, i) l ^ i (1 - l) ^ (n - i) θ ^ (r - i)`, + -- and `θ ^ (r - i) ≤ 1` + _ ≤ ∑ i ∈ range (r + 1), + ((q : ℝ) - 1) ^ r * (l ^ i * (1 - l) ^ (n - i) * (n.choose i : ℝ)) := by + refine sum_le_sum fun i hi => ?_ + have hir : i ≤ r := mem_range_succ_iff.mp hi + have h1 : l ^ r = l ^ i * l ^ (r - i) := by rw [← pow_add]; congr 1; omega + have h2 : (1 - l) ^ (n - i) = (1 - l) ^ (n - r) * (1 - l) ^ (r - i) := by + rw [← pow_add]; congr 1; omega + have h3 : ((q : ℝ) - 1) ^ r = ((q : ℝ) - 1) ^ i * ((q : ℝ) - 1) ^ (r - i) := by + rw [← pow_add]; congr 1; omega + calc (n.choose i : ℝ) * ((q : ℝ) - 1) ^ i * (l ^ r * (1 - l) ^ (n - r)) + = (n.choose i : ℝ) * ((q : ℝ) - 1) ^ i * (l ^ i * (1 - l) ^ (n - r)) + * l ^ (r - i) := by rw [h1]; ring + _ ≤ (n.choose i : ℝ) * ((q : ℝ) - 1) ^ i * (l ^ i * (1 - l) ^ (n - r)) + * (((q : ℝ) - 1) * (1 - l)) ^ (r - i) := by gcongr + _ = ((q : ℝ) - 1) ^ r * (l ^ i * (1 - l) ^ (n - i) * (n.choose i : ℝ)) := by + rw [h2, h3, mul_pow]; ring + -- extend the sum from `i ≤ r` to `i ≤ n` + _ ≤ ∑ i ∈ range (n + 1), + ((q : ℝ) - 1) ^ r * (l ^ i * (1 - l) ^ (n - i) * (n.choose i : ℝ)) := + sum_le_sum_of_subset_of_nonneg + (range_subset_range.mpr (Nat.succ_le_succ hrn.le)) fun i _ _ => by positivity + _ = ((q : ℝ) - 1) ^ r := by rw [← mul_sum, hbinom, mul_one] + +variable {α : Type*} {n : ℕ} [DecidableEq α] + +/-- The Hamming ball of radius `r` around the word `x`: all words at Hamming distance at most +`r` from `x`. -/ +def hammingBall (x : Fin n → α) (r : ℕ) : Set (Fin n → α) := {y | hammingDist x y ≤ r} + +@[simp] +lemma mem_hammingBall {x y : Fin n → α} {r : ℕ} : y ∈ hammingBall x r ↔ hammingDist x y ≤ r := + Iff.rfl + +lemma mem_hammingBall_self (x : Fin n → α) (r : ℕ) : x ∈ hammingBall x r := by simp + +/-- The set of coordinates on which the words `x` and `y` disagree; its cardinality is the Hamming +distance `hammingDist x y` (see `card_disagree`). -/ +def disagree (x y : Fin n → α) : Finset (Fin n) := {j | x j ≠ y j} + +@[simp] +lemma card_disagree (x y : Fin n → α) : (disagree x y).card = hammingDist x y := rfl + +@[simp] +lemma mem_disagree {x y : Fin n → α} {j : Fin n} : j ∈ disagree x y ↔ x j ≠ y j := by + simp [disagree] + +variable [Fintype α] + +/-- For a fixed set `S` of coordinates, there are exactly `(q - 1) ^ |S|` words that disagree with +`x` precisely on `S`, where `q = |α|`: they can take any of the `q - 1` values different from `x j` +at each `j ∈ S`, and must agree with `x` elsewhere. -/ +lemma ncard_setOf_disagree_eq (x : Fin n → α) (S : Finset (Fin n)) : + {y : Fin n → α | disagree x y = S}.ncard = (Fintype.card α - 1) ^ S.card := by + rw [Set.ncard_eq_toFinset_card', Set.toFinset_ofPred] + -- the words disagreeing with `x` exactly on `S` are the elements of the product of the sets + -- `{x j}ᶜ` for `j ∈ S` and `{x j}` for `j ∉ S` + have hset : (univ.filter fun y : Fin n → α => disagree x y = S) + = Fintype.piFinset fun j => if j ∈ S then {x j}ᶜ else {x j} := by + ext y + simp only [mem_filter, mem_univ, true_and, Fintype.mem_piFinset] + have key : ∀ j : Fin n, + (y j ∈ if j ∈ S then ({x j}ᶜ : Finset α) else {x j}) ↔ (x j ≠ y j ↔ j ∈ S) := by + intro j + by_cases hj : j ∈ S <;> simp [hj, eq_comm] + rw [Finset.ext_iff] + simp only [mem_disagree, key] + rw [hset, Fintype.card_piFinset] + simp only [apply_ite Finset.card, card_compl, card_singleton] + rw [Fintype.prod_ite_mem, prod_const] + +/-- There are exactly `C(n, i) (q - 1) ^ i` words at Hamming distance exactly `i` from `x`, where +`q = |α|`: partition them according to the set of coordinates on which they disagree with `x`. -/ +lemma ncard_hammingSphere (x : Fin n → α) (i : ℕ) : + {y : Fin n → α | hammingDist x y = i}.ncard = n.choose i * (Fintype.card α - 1) ^ i := by + rw [Set.ncard_eq_toFinset_card', Set.toFinset_ofPred] + -- the disagreement set of a word at distance `i` from `x` is a subset of `Fin n` of size `i` + have hmaps : ((univ.filter fun y : Fin n → α => hammingDist x y = i : Finset _) : + Set (Fin n → α)).MapsTo (fun y => disagree x y) ((univ : Finset (Fin n)).powersetCard i) := by + intro y hy + rw [mem_coe, mem_filter] at hy + rw [mem_coe, mem_powersetCard] + exact ⟨filter_subset _ _, hy.2⟩ + rw [card_eq_sum_card_fiberwise hmaps] + -- each fibre has `(q - 1) ^ i` elements and there are `C(n, i)` of them + trans ∑ _S ∈ (univ : Finset (Fin n)).powersetCard i, (Fintype.card α - 1) ^ i + · refine sum_congr rfl fun S hS => ?_ + obtain ⟨-, rfl⟩ := mem_powersetCard.mp hS + -- on the fibre over `S` the condition `hammingDist x y = |S|` is automatic + rw [filter_filter, filter_congr fun y _ => + and_iff_right_of_imp fun h => by rw [← card_disagree, h], + ← Set.toFinset_ofPred, ← Set.ncard_eq_toFinset_card', ncard_setOf_disagree_eq] + · rw [sum_const, card_powersetCard, card_fin, smul_eq_mul] + +/-- A Hamming ball of radius `r` contains exactly `Vol_q(n, r)` words, where `q = |α|`: partition +it into the spheres of radius `0, …, r` and count them with `ncard_hammingSphere`. -/ +lemma ncard_hammingBall (x : Fin n → α) (r : ℕ) : + (hammingBall x r).ncard = hammingVolume (Fintype.card α) n r := by + rw [hammingBall, hammingVolume, Set.ncard_eq_toFinset_card', Set.toFinset_ofPred] + -- the distance to `x` of a word in the ball lies in `{0, …, r}` + have hmaps : ((univ.filter fun y : Fin n → α => hammingDist x y ≤ r : Finset _) : + Set (Fin n → α)).MapsTo (fun y => hammingDist x y) (range (r + 1)) := by + intro y hy + rw [mem_coe, mem_filter] at hy + rw [mem_coe, mem_range] + exact Nat.lt_succ_of_le hy.2 + rw [card_eq_sum_card_fiberwise hmaps] + -- the fibre at distance `i ≤ r` is the sphere of radius `i` + refine sum_congr rfl fun i hi => ?_ + have hir : i ≤ r := mem_range_succ_iff.mp hi + have hfib : (univ.filter fun y : Fin n → α => hammingDist x y ≤ r).filter + (fun y => hammingDist x y = i) = univ.filter fun y => hammingDist x y = i := by + ext y + simp only [mem_filter, mem_univ, true_and] + exact and_iff_right_of_imp fun h => h.trans_le hir + rw [hfib, ← Set.toFinset_ofPred, ← Set.ncard_eq_toFinset_card', ncard_hammingSphere] + +end Cslib.CodingTheory