Self-correction of Reed–Muller codes by interpolation along lines

A received word w that differs from a Reed–Muller codeword p of degree d on few points can be corrected by reading w at d + 1 points x + ν i • v of a line through x, for fixed distinct nonzero nodes ν i, and interpolating: p x = ∑ i, λ i * p (x + ν i • v) for the Lagrange weights λ i of the nodes at 0 (Cslib.Code.lagrangeDecode_eq_of_mem_reedMuller). Each queried point is uniformly distributed over the directions v, so at every point x at most (d + 1) * Δ(w, p) directions make the step err (Cslib.Code.card_lagrangeDecode_ne_le) Arora and Barak, Chapter 19. Combined with ternary majority trees (Cslib.majTree, Cslib.exists_forall_majTree_eq), this corrects w everywhere on a bounded set with fixed directions.

Main definitions

• Cslib.Code.lagrangeWeight, Cslib.Code.lagrangeDecode: interpolation along a line.

Main results

• Cslib.Code.lagrangeDecode_eq_of_mem_reedMuller: interpolation is exact on codewords.
• Cslib.Code.card_lagrangeDecode_ne_le: few directions err.

References

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

noncomputable def Cslib.Code.lagrangeWeight {F : Type u_1} [Field F] {d : ℕ} (ν : Fin (d + 1) ↪ F) (i : Fin (d + 1)) : F

The Lagrange weight of the node ν i at 0.

theorem Cslib.Code.eval_zero_eq_sum_lagrangeWeight {F : Type u_1} [Field F] {d : ℕ} (ν : Fin (d + 1) ↪ F) {P : Polynomial F} (hP : P.natDegree ≤ d) : Polynomial.eval 0 P = ∑ i : Fin (d + 1), lagrangeWeight ν i * Polynomial.eval (ν i) P

A polynomial of degree at most d is determined at 0 by its values at d + 1 nodes.

noncomputable def Cslib.Code.lagrangeDecode {F : Type u_1} [Field F] {m d : ℕ} (ν : Fin (d + 1) ↪ F) (w : (Fin m → F) → F) (x v : Fin m → F) : F

Interpolation along a line: the combination of the values of w at the points x + ν i • v with the Lagrange weights at 0.

theorem Cslib.Code.lagrangeDecode_eq_of_mem_reedMuller {F : Type u_1} [Field F] {m d : ℕ} (ν : Fin (d + 1) ↪ F) {p : (Fin m → F) → F} (hp : p ∈ reedMuller F m d) (x v : Fin m → F) : lagrangeDecode ν p x v = p x

Interpolation is exact on codewords of the Reed–Muller code of degree d, for every direction.

theorem Cslib.Code.card_lagrangeDecode_ne_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} (ν : Fin (d + 1) ↪ F) (hν : ∀ (i : Fin (d + 1)), ν i ≠ 0) {p : (Fin m → F) → F} (hp : p ∈ reedMuller F m d) (w : (Fin m → F) → F) (x : Fin m → F) : {v : Fin m → F | lagrangeDecode ν w x v ≠ p x}.card ≤ (d + 1) * {y : Fin m → F | w y ≠ p y}.card

Few directions err. At every point x, at most (d + 1) * Δ(w, p) directions v make interpolation along the line through x in the direction v err, when the nodes are nonzero.