List Decoding

This file defines list-decodable codes and proves the list-decoding capacity theorem: for any ρ with 0 < ρ ≤ 1 − 1/q and list size L ≥ 1, there exist codes of rate

r = 1 − H_q(ρ) − 1/L

that are list-decodable with radius ρ and list size L.

Main Definitions

• list_decodable ρ hρ₁ hρ₂ n L hL C : C is (ρ, L)-list-decodable if every Hamming ball of radius ⌊ρn⌋ contains at most L codewords of C.

Main Results

• exists_listDecodable_code : a counting/probabilistic argument showing existence of list-decodable codes meeting a given size bound.
• binom_ratio_bound : the ratio C(N−k, M−k) / C(N,M) ≤ (M/N)ᵏ.
• listDecoding_counting_ineq : the counting inequality used in the capacity proof.
• list_decoding_capacity : codes of rate 1 − H_q(ρ) − 1/L are (ρ, L)-list-decodable.

References

• V. Guruswami, A. Rudra, M. Sudan, "Essential Coding Theory", Chapter on List Decoding.

def CodingTheory.Codeword.list_decodable {α : Type u_1} [Fintype α] [DecidableEq α] (ρ : ℝ) (hρ₁ : 0 ≤ ρ) (hρ₂ : ρ ≤ 1) (n L : ℕ) (hL : L ≥ 1) (C : Code n α) : Prop

A code C is (ρ, L)-list-decodable if every Hamming ball of radius ⌊ρn⌋ contains at most L codewords of C.

Equations

• CodingTheory.Codeword.list_decodable ρ hρ₁ hρ₂ n L hL C = ∀ (y : CodingTheory.Codeword n α), (CodingTheory.Codeword.hamming_ball ⌊ρ * ↑n⌋₊ y ∩ C).card ≤ L

theorem CodingTheory.Codeword.exists_listDecodable_code {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] (n L M : ℕ) (p : ℝ) (hp1 : 0 ≤ p) (hp2 : p ≤ 1) (hL : 1 ≤ L) (V : ℕ) (hV : ∀ (y : Codeword n α), (hamming_ball ⌊p * ↑n⌋₊ y).card ≤ V) (h_ineq : Fintype.card α ^ n * V.choose (L + 1) * (Fintype.card α ^ n - (L + 1)).choose (M - (L + 1)) < (Fintype.card α ^ n).choose M) (hM_le_N : M ≤ Fintype.card α ^ n) (hL_lt_M : L < M) : ∃ (C : Code n α), Finset.card C = M ∧ list_decodable p hp1 hp2 n L hL C

Existence of list-decodable codes: if the ball volume V and code size M satisfy the given counting inequality, then there exists a code C of size M that is (p, L)-list-decodable.

theorem CodingTheory.Codeword.binom_ratio_bound (N M k : ℕ) (hM : M ≤ N) (hk : k ≤ M) : ↑((N - k).choose (M - k)) / ↑(N.choose M) ≤ (↑M / ↑N) ^ k

Binomial ratio bound: C(N−k, M−k) / C(N, M) ≤ (M/N)ᵏ.

theorem CodingTheory.Codeword.listDecoding_counting_ineq (q : ℕ) (p : ℝ) (n L : ℕ) (hq : 2 ≤ q) (hL : 1 ≤ L) (r : ℝ) (hr : r = 1 - qaryEntropy q p - 1 / ↑L) (M : ℕ) (hM : M = ⌊↑q ^ (r * ↑n)⌋₊) (V : ℕ) (hV : V = ⌊(↑q).rpow (qaryEntropy q p * ↑n)⌋₊) (hM_pos : 0 < M) (hM_le : M ≤ q ^ n) (hL_lt_M : L < M) : ↑q ^ n * ↑(V.choose (L + 1)) * ↑((q ^ n - (L + 1)).choose (M - (L + 1))) < ↑((q ^ n).choose M)

Counting inequality for list decoding: for the given choice of rate r and ball-size bound V, the number of "bad" M-subsets exceeds the number of good ones only if M is small (i.e., rate > capacity).

theorem CodingTheory.Codeword.list_decoding_capacity {α : Type u_1} [Fintype α] [Nonempty α] [DecidableEq α] [Field α] {n : ℕ} (q : ℕ) (p : ℝ) (hq : q = Fintype.card α) (hp : 0 < p ∧ p ≤ 1 - 1 / ↑q) (L : ℕ) (hL : 1 ≤ L) : have r := 1 - qaryEntropy q p - 1 / ↑L; have M := ⌊↑q ^ (r * ↑n)⌋₊; ∃ (C : Code n α), M ≤ Finset.card C ∧ list_decodable p ⋯ ⋯ n L hL C

List-decoding capacity theorem: for any 0 < ρ ≤ 1 − 1/q and L ≥ 1, there exist codes of rate r = 1 − H_q(ρ) − 1/L that are (ρ, L)-list-decodable.

In other words, one can list-decode at any rate below the list-decoding capacity 1 − H_q(ρ) using list size L.