List decoding

A list code encodes messages of a type α as words ι → β over an alphabet β, and its list decoder turns every received word w into L candidate messages. The code list decodes up to radius ρ if the candidates for w include every message whose codeword differs from w on at most a ρ fraction of the coordinates Arora and Barak, Chapter 19; binary codes are those with β = Bool. A word that agrees with the codeword of x on a 1 / 2 + δ fraction of the coordinates thus determines x up to L possibilities when the code list decodes up to radius 1 / 2 - δ (Cslib.ListCode.ListDecodes.mem_candidates_of_half_add_le): x is one of the at most L candidates (Cslib.ListCode.card_candidates_le), and it is named by an index of ⌈log₂ L⌉ bits (Cslib.ListCode.ListDecodes.exists_decodeBits_eq_some). This is how the Nisan–Wigderson reconstruction recovers a message from a predictor of its codeword.

Main definitions

• Cslib.ListCode: an encoder of messages as words over an alphabet with a list decoder.
• Cslib.ListCode.ListDecodes: list decoding up to a relative radius.
• Cslib.ListCode.candidates: the candidates for a received word.
• Cslib.ListCode.decodeBits: the candidate named by a binary index.

Main results

• Cslib.ListCode.card_candidates_le: there are at most L candidates.
• Cslib.ListCode.listDecodes_of_surjective: a decoder listing every message list decodes at every radius.
• Cslib.ListCode.ListDecodes.exists_decode_eq, Cslib.ListCode.ListDecodes.exists_decode_eq_of_half_add_le: a message whose codeword agrees with the received word on enough coordinates is a candidate.
• Cslib.ListCode.ListDecodes.exists_decodeBits_eq_some: it is named by an index of Nat.clog 2 L bits.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 19

structure Cslib.ListCode (α : Type u_1) (ι : Type u_2) (β : Type u_3) (L : ℕ) : Type (max (max u_1 u_2) u_3)

A list code: an encoder of messages of type α as words on the coordinates ι over the alphabet β, with a list decoder returning L candidate messages for every received word.

• encode : α → ι → β

  The codeword of a message.

• decode : (ι → β) → Fin L → α

  The k-th candidate message for a received word.

def Cslib.ListCode.ListDecodes {α : Type u_1} {ι : Type u_2} {β : Type u_3} {L : ℕ} (C : ListCode α ι β L) [Fintype ι] [DecidableEq β] (ρ : ℝ) : Prop

The code list decodes up to radius ρ: the candidates for a received word w include every message whose codeword differs from w on at most a ρ fraction of the coordinates.

def Cslib.ListCode.candidates {α : Type u_1} {ι : Type u_2} {β : Type u_3} {L : ℕ} (C : ListCode α ι β L) [DecidableEq α] (w : ι → β) : Finset α

The candidates for the received word w, without repetitions.

@[simp]

theorem Cslib.ListCode.mem_candidates {α : Type u_1} {ι : Type u_2} {β : Type u_3} {L : ℕ} (C : ListCode α ι β L) [DecidableEq α] {w : ι → β} {x : α} : x ∈ C.candidates w ↔ ∃ (k : Fin L), C.decode w k = x

A message is a candidate for w exactly when the decoder returns it at some index.

theorem Cslib.ListCode.card_candidates_le {α : Type u_1} {ι : Type u_2} {β : Type u_3} {L : ℕ} (C : ListCode α ι β L) [DecidableEq α] (w : ι → β) : (C.candidates w).card ≤ L

List size. A received word has at most L candidates.

def Cslib.ListCode.decodeBits {α : Type u_1} {ι : Type u_2} {β : Type u_3} {L : ℕ} (C : ListCode α ι β L) (w : ι → β) (b : BitString (Nat.clog 2 L)) : Option α

The candidate named by the binary index b of Nat.clog 2 L bits, read least significant bit first: the k-th candidate for w if b spells a number k < L, and nothing otherwise.

theorem Cslib.ListCode.exists_decodeBits_eq_some {α : Type u_1} {ι : Type u_2} {β : Type u_3} {L : ℕ} (C : ListCode α ι β L) {w : ι → β} {x : α} (h : ∃ (k : Fin L), C.decode w k = x) : ∃ (b : BitString (Nat.clog 2 L)), C.decodeBits w b = some x

Short index. Every candidate is named by an index of Nat.clog 2 L bits.

theorem Cslib.ListCode.listDecodes_of_surjective {α : Type u_1} {ι : Type u_2} {β : Type u_3} {L : ℕ} {C : ListCode α ι β L} [Fintype ι] [DecidableEq β] (h : ∀ (w : ι → β), Function.Surjective (C.decode w)) (ρ : ℝ) : C.ListDecodes ρ

A decoder whose candidates enumerate all messages, whatever the received word, list decodes at every radius: the list then has L ≥ |α| entries, so this only shows that list decoding is satisfiable.

theorem Cslib.ListCode.ListDecodes.exists_decode_eq {α : Type u_1} {ι : Type u_2} {β : Type u_3} {L : ℕ} {C : ListCode α ι β L} [Fintype ι] [DecidableEq β] {ρ : ℝ} (hC : C.ListDecodes ρ) {x : α} {w : ι → β} (h : 1 - ρ ≤ ↑{i : ι | C.encode x i = w i}.dens) : ∃ (k : Fin L), C.decode w k = x

A list decoder up to radius ρ lists every message whose codeword agrees with the received word on at least a 1 - ρ fraction of the coordinates.

theorem Cslib.ListCode.ListDecodes.exists_decode_eq_of_half_add_le {α : Type u_1} {ι : Type u_2} {β : Type u_3} {L : ℕ} {C : ListCode α ι β L} [Fintype ι] [DecidableEq β] {δ : ℝ} (hC : C.ListDecodes (1 / 2 - δ)) {x : α} {w : ι → β} (h : 1 / 2 + δ ≤ ↑{i : ι | C.encode x i = w i}.dens) : ∃ (k : Fin L), C.decode w k = x

A list decoder up to radius 1 / 2 - δ lists every message whose codeword agrees with the received word on at least a 1 / 2 + δ fraction of the coordinates.

theorem Cslib.ListCode.ListDecodes.mem_candidates_of_half_add_le {α : Type u_1} {ι : Type u_2} {β : Type u_3} {L : ℕ} {C : ListCode α ι β L} [Fintype ι] [DecidableEq β] [DecidableEq α] {δ : ℝ} (hC : C.ListDecodes (1 / 2 - δ)) {x : α} {w : ι → β} (h : 1 / 2 + δ ≤ ↑{i : ι | C.encode x i = w i}.dens) : x ∈ C.candidates w

A message whose codeword agrees with the received word on at least a 1 / 2 + δ fraction of the coordinates is among the candidates of a list decoder up to radius 1 / 2 - δ.

theorem Cslib.ListCode.ListDecodes.exists_decodeBits_eq_some {α : Type u_1} {ι : Type u_2} {β : Type u_3} {L : ℕ} {C : ListCode α ι β L} [Fintype ι] [DecidableEq β] {δ : ℝ} (hC : C.ListDecodes (1 / 2 - δ)) {x : α} {w : ι → β} (h : 1 / 2 + δ ≤ ↑{i : ι | C.encode x i = w i}.dens) : ∃ (b : BitString (Nat.clog 2 L)), C.decodeBits w b = some x

Short index. If a code list decodes up to radius 1 / 2 - δ, a received word that agrees with the codeword of x on at least a 1 / 2 + δ fraction of the coordinates, together with an index of Nat.clog 2 L bits, determines x.