Entropy and Asymptotic Bounds

This file establishes asymptotic bounds relating Hamming ball sizes to the q-ary entropy function, and provides the key binomial coefficient lower bound used in the Gilbert–Varshamov theorem.

Main Results

• hamming_ball_size_asymptotic_upper_bound : for 0 < p ≤ 1 - 1/q, the Hamming ball of radius ⌊np⌋ has at most q^(H_q(p)·n) elements.
• q_pow_qary_entropy_simp / q_pow_qary_entropy_simp' : simplification lemmas for q^(H_q(p)) in terms of elementary functions.
• binomial_coef_asymptotic_lower_bound' : the dominant binomial term C(n,⌊np⌋)·(q-1)^(pn) grows at least as fast as q^(H_q(p)·n - ε(n)) where ε = o(n).
• qary_entropy_pos : the q-ary entropy is positive for 0 < p ≤ 1 - 1/q.

theorem ErrorCorrectingCodes.Codeword.hamming_ball_size_asymptotic_upper_bound {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] (q n : ℕ) (p : ℝ) (hq : q = Fintype.card α) (hα : Nontrivial α) (hp : 0 < p ∧ p ≤ 1 - 1 / ↑q) (c : Codeword n α) : ↑(hamming_ball ⌊↑n * p⌋₊ c).card ≤ (↑q).rpow (qaryEntropy q p * ↑n)

Asymptotic upper bound on ball size: for 0 < p ≤ 1 - 1/q, the Hamming ball of radius ⌊np⌋ has at most q^(H_q(p)·n) elements.

theorem ErrorCorrectingCodes.Codeword.q_pow_qary_entropy_simp {q : ℕ} {p : ℝ} (hq : 2 ≤ q) (hp : 0 < p ∧ p < 1) : (↑q).rpow (qaryEntropy q p) = (↑q - 1) ^ p * p ^ (-p) * (1 - p) ^ (-(1 - p))

Simplification: q^(H_q(p)) = (q-1)^p · p^(-p) · (1-p)^(-(1-p)). Uses Real.rpow.

theorem ErrorCorrectingCodes.Codeword.q_pow_qary_entropy_simp' {q : ℕ} {p : ℝ} (hq : 2 ≤ q) (hp : 0 < p ∧ p < 1) : ↑q ^ qaryEntropy q p = (↑q - 1) ^ p * p ^ (-p) * (1 - p) ^ (-(1 - p))

Variant of q_pow_qary_entropy_simp using natural-number power (q ^ _).

theorem ErrorCorrectingCodes.Codeword.sqrt_sub_sqrt_floor_le_one {x : ℝ} (hx : 0 ≤ x) : √x - √↑⌊x⌋₊ ≤ 1

Helper: √x - √⌊x⌋ ≤ 1 for x ≥ 0.

theorem ErrorCorrectingCodes.Codeword.binomial_coef_asymptotic_lower_bound' {q : ℕ} {p : ℝ} (hp : 0 < p ∧ p < 1) (hq : 2 ≤ q) : ∃ (ε : ℕ → ℝ), (ε =o[Filter.atTop] fun (n : ℕ) => ↑n) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(n.choose ⌊↑n * p⌋₊) * (↑q - 1) ^ (p * ↑n) ≥ (↑q).rpow (qaryEntropy q p * ↑n - ε n)

Binomial lower bound: there exists ε = o(n) such that for all large n, C(n,⌊np⌋) · (q-1)^(pn) ≥ q^(H_q(p)·n - ε(n)). This is a key ingredient in the Gilbert–Varshamov bound.

theorem ErrorCorrectingCodes.Codeword.qary_entropy_pos {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] (q : ℕ) (p : ℝ) (hq : q = Fintype.card α) (hp : 0 < p ∧ p ≤ 1 - 1 / ↑q) : 0 < p * Real.logb (↑q) (↑q - 1) - p * Real.logb (↑q) p - (1 - p) * Real.logb (↑q) (1 - p)

The q-ary entropy H_q(p) is strictly positive for 0 < p ≤ 1 - 1/q.