feat: Coding Theory, Gilbert Varshamov

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

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),
+  <https://cse.buffalo.edu/faculty/atri/courses/coding-theory/book/web-coding-book.pdf>
+-/
+
+@[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

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),
+  <https://cse.buffalo.edu/faculty/atri/courses/coding-theory/book/web-coding-book.pdf>
+-/
+
+@[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