Documentation

Complexity.Foundations.Data.Code.LocalDecoding

Local decoding of Reed–Muller codes along lines #

Let F be a finite field with q elements and let f be a codeword of the Reed–Muller code of degree d in m variables over F, the evaluation table of a polynomial of total degree at most d. Along every affine line c ↦ x + c • v the codeword is a polynomial in c of degree at most d, and the values of a polynomial of degree below q - 1 sum to zero over F. So for d + 1 < q the sum of f over every line vanishes (Cslib.Code.sum_add_smul_eq_zero_of_mem_reedMuller), and the value of f at x is minus the sum of its values on the punctured line Cslib.LineCode.puncturedLine x v of the q - 1 points x + c • v with c ≠ 0.

The line decoder Cslib.Code.lineDecode w x v reads a received word w at the q - 1 points of that punctured line only (Cslib.Code.lineDecode_congr) and returns minus their sum. This is the basic local decoder of Reed–Muller codes, which interpolates the restriction of the received word to a random line through x Arora and Barak, Chapter 19, [GRS19]; interpolating a polynomial of degree below q - 1 from all q - 1 points other than x gives minus their sum at x. On a codeword it returns the value at x for every direction (Cslib.Code.lineDecode_eq_of_mem_reedMuller), and on a corrupted codeword it still does whenever the punctured line avoids the corrupted points (Cslib.Code.lineDecode_eq_of_disjoint). By the blocking bound Cslib.LineCode.card_filter_not_disjoint_puncturedLine_le, every corrupted point other than x lies on the punctured lines of only q - 1 of the q ^ m - 1 nonzero directions, so at most (q - 1) * Δ(w, f) nonzero directions make the decoder err (Cslib.Code.card_filter_lineDecode_ne_le): for a uniformly random nonzero direction the decoder reads f x from w with q - 1 queries except with probability at most (q - 1) * Δ(w, f) / (q ^ m - 1). In particular, if 2 * (q - 1) * Δ(w, f) < q ^ m - 1, more than half of the nonzero directions recover f x at every point x (Cslib.Code.lt_two_mul_card_filter_lineDecode_eq).

Main definitions #

Main results #

References #

source
theorem Cslib.Code.exists_natDegree_le_eval_eq_of_mem_reedMuller {F : Type u_1} [Field F] {m d : ℕ} {f : (Fin m → F) → F} (hf : f ∈ reedMuller F m d) (x v : Fin m → F) :
∃ (g : Polynomial F), g.natDegree ≤ d ∧ ∀ (t : F), Polynomial.eval t g = f (x + t • v)

Restriction to a line. The restriction t ↦ f (x + t • v) of a codeword f of the Reed–Muller code of degree d is a polynomial of degree at most d.

source
theorem Cslib.Code.sum_add_smul_eq_zero_of_mem_reedMuller {F : Type u_1} [Field F] [Fintype F] {m d : ℕ} (hd : d + 1 < Fintype.card F) {f : (Fin m → F) → F} (hf : f ∈ reedMuller F m d) (x v : Fin m → F) :
∑ c : F, f (x + c • v) = 0

Line sums of Reed–Muller codewords. For d + 1 < q, the values of a codeword of the Reed–Muller code of degree d over a field with q elements sum to zero on every affine line c ↦ x + c • v, including the degenerate line v = 0.

source
def Cslib.Code.lineDecode {F : Type u_1} [Field F] [Fintype F] {m : ℕ} [DecidableEq F] (w : (Fin m → F) → F) (x v : Fin m → F) :
F

The line decoder: the value at x read off a received word w along the direction v, minus the sum of the values of w at the q - 1 points x + c • v with c ≠ 0.

Instances For
    source
    theorem Cslib.Code.lineDecode_congr {F : Type u_1} [Field F] [Fintype F] {m : ℕ} [DecidableEq F] {w w' : (Fin m → F) → F} {x v : Fin m → F} (h : ∀ y ∈ LineCode.puncturedLine x v, w y = w' y) :
    lineDecode w x v = lineDecode w' x v

    Locality. The line decoder queries the received word only at the points of the punctured line puncturedLine x v, of which there are at most q - 1.

    source
    theorem Cslib.Code.lineDecode_eq_of_mem_reedMuller {F : Type u_1} [Field F] [Fintype F] {m d : ℕ} [DecidableEq F] (hd : d + 1 < Fintype.card F) {f : (Fin m → F) → F} (hf : f ∈ reedMuller F m d) (x v : Fin m → F) :
    lineDecode f x v = f x

    The line decoder is exact on codewords. For d + 1 < q, on a codeword f of the Reed–Muller code of degree d the line decoder returns f x for every direction v.

    source
    theorem Cslib.Code.lineDecode_eq_of_disjoint {F : Type u_1} [Field F] [Fintype F] {m d : ℕ} [DecidableEq F] (hd : d + 1 < Fintype.card F) {f w : (Fin m → F) → F} (hf : f ∈ reedMuller F m d) {x v : Fin m → F} (h : Disjoint (LineCode.puncturedLine x v) {y : Fin m → F | w y ≠ f y}) :
    lineDecode w x v = f x

    For d + 1 < q, if the punctured line through x in the direction v avoids the points where the received word w differs from a codeword f of the Reed–Muller code of degree d, the line decoder reads f x from w. An error at x itself is corrected.

    source
    theorem Cslib.Code.card_filter_lineDecode_ne_le {F : Type u_1} [Field F] [Fintype F] {m d : ℕ} [DecidableEq F] (hd : d + 1 < Fintype.card F) {f : (Fin m → F) → F} (hf : f ∈ reedMuller F m d) (w : (Fin m → F) → F) (x : Fin m → F) :
    {v ∈ Finset.univ.erase 0 | lineDecode w x v ≠ f x}.card ≤ hammingDist w f * (Fintype.card F - 1)

    Local decoding of Reed–Muller codes. For d + 1 < q, let w be a received word and f a codeword of the Reed–Muller code of degree d over a field with q elements. At every point x, at most (q - 1) * Δ(w, f) of the q ^ m - 1 nonzero directions v make the line decoder err.

    source
    theorem Cslib.Code.lt_two_mul_card_filter_lineDecode_eq {F : Type u_1} [Field F] [Fintype F] {m d : ℕ} [DecidableEq F] (hd : d + 1 < Fintype.card F) {f w : (Fin m → F) → F} (hf : f ∈ reedMuller F m d) (h : 2 * (hammingDist w f * (Fintype.card F - 1)) < Fintype.card F ^ m - 1) (x : Fin m → F) :
    Fintype.card F ^ m - 1 < 2 * {v ∈ Finset.univ.erase 0 | lineDecode w x v = f x}.card

    Self-correction of Reed–Muller codes. For d + 1 < q, if a received word w and a codeword f of the Reed–Muller code of degree d over a field with q elements satisfy 2 * (q - 1) * Δ(w, f) < q ^ m - 1, then at every point x more than half of the q ^ m - 1 nonzero directions make the line decoder return f x.