Asymptotically good code families

A family of codes C s : Set (ι s → α) over a finite nontrivial alphabet α is asymptotically good (Cslib.Code.IsAsymptoticallyGood) if its block lengths |ι s| grow without bound while its rates and relative minimum distances stay bounded away from zero [Jus72], [GRS19], MacWilliams and Sloane, Chapter 17. In integer form, there are positive natural numbers R and Δ such that every code C s in the family has at least |α| ^ k codewords for some k with |ι s| ≤ R * k (rate k / |ι s| ≥ 1 / R) and minimum distance d with |ι s| ≤ Δ * d (relative distance d / |ι s| ≥ 1 / Δ).

Main definitions

• Cslib.Code.IsAsymptoticallyGood: asymptotically good code families.

References

• J. Justesen, Class of constructive asymptotically good algebraic codes
• V. Guruswami, A. Rudra, M. Sudan, Essential Coding Theory
• [F. J. MacWilliams, N. J. A. Sloane, The Theory of Error-Correcting Codes] [MWS77]

structure Cslib.Code.IsAsymptoticallyGood {σ : Type u_1} {ι : σ → Type u_2} [(s : σ) → Fintype (ι s)] {α : Type u_3} [Fintype α] [DecidableEq α] [Nontrivial α] (C : (s : σ) → Set (ι s → α)) : Prop

A family of codes C s : Set (ι s → α) over a nontrivial alphabet α is asymptotically good if its block lengths |ι s| grow without bound and its rates and relative distances are bounded away from zero: for some positive natural numbers R and Δ, every C s has at least |α| ^ k codewords for a dimension k with |ι s| ≤ R * k (rate at least 1 / R) and minimum distance d with |ι s| ≤ Δ * d (relative distance at least 1 / Δ).

• exists_le_card (N : ℕ) : ∃ (s : σ), N ≤ Fintype.card (ι s)

  The block lengths grow without bound.

• exists_rate : ∃ (R : ℕ), 0 < R ∧ ∀ (s : σ), ∃ (k : ℕ), Fintype.card (ι s) ≤ R * k ∧ Fintype.card α ^ k ≤ Nat.card ↑(C s)

  The rate is bounded away from zero: for some R : ℕ with 0 < R, every code in the family has at least |α| ^ k codewords for a dimension k with |ι s| ≤ R * k.

• exists_minDist : ∃ (Δ : ℕ), 0 < Δ ∧ ∀ (s : σ), ↑(Fintype.card (ι s)) ≤ ↑Δ * minDist (C s)

  The relative distance is bounded away from zero: for some Δ : ℕ with 0 < Δ, every code in the family has minimum distance d with |ι s| ≤ Δ * d.