Low-degree extensions

Let h : H ↪ F embed a finite set H of size |H| in a field F. Every function f : (Fin m → H) → F on the grid H ^ m is the restriction of a polynomial of low degree: the low-degree extension lowDegreeExtension h f x = ∑ u, f u * ∏ i, L (u i) (x i), where L a is the Lagrange basis polynomial of the node h a among the nodes h H Babai, Fortnow, Levin, Szegedy, Arora and Barak, Chapter 19. It agrees with f on the grid (Cslib.Code.lowDegreeExtension_apply_embed) and is a codeword of the Reed–Muller code of degree m * (|H| - 1) (Cslib.Code.lowDegreeExtension_mem_reedMuller). Only this total degree bound is formalized; by construction the extension also has degree less than |H| in each variable, and for H = {0, 1} it is the multilinear extension, but neither fact is stated here.

Low-degree extensions encode truth tables into Reed–Muller codewords: the truth table of a function on n = m * b bits, read as a function on (BitString b) ^ m, extends to a polynomial in m variables of total degree at most m * (2 ^ b - 1) over a field with at least 2 ^ b elements. Informally, evaluating the extension at a point costs |H| ^ m terms, linear in the size of the truth table, which is what makes encodings of functions computable in exponential time; no running time is formalized in this module.

Main definitions

• Cslib.Code.lowDegreeExtension: the low-degree extension.

Main results

• Cslib.Code.lowDegreeExtension_apply_embed: it extends f.
• Cslib.Code.lowDegreeExtension_mem_reedMuller: it is a Reed–Muller codeword.

References

• [L. Babai, L. Fortnow, L. Levin, M. Szegedy, Checking computations in polylogarithmic time] [BFLS91]
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 19

noncomputable def Cslib.Code.lowDegreeExtension {F : Type u_1} [Field F] {H : Type u_2} [Fintype H] [DecidableEq H] {m : ℕ} (h : H ↪ F) (f : (Fin m → H) → F) : (Fin m → F) → F

The low-degree extension of f : (Fin m → H) → F along the embedding h : H ↪ F.

theorem Cslib.Code.lowDegreeExtension_apply_embed {F : Type u_1} [Field F] {H : Type u_2} [Fintype H] [DecidableEq H] {m : ℕ} (h : H ↪ F) (f : (Fin m → H) → F) (u : Fin m → H) : (lowDegreeExtension h f fun (i : Fin m) => h (u i)) = f u

The low-degree extension extends f: it agrees with f on the grid.

theorem Cslib.Code.lowDegreeExtension_mem_reedMuller {F : Type u_1} [Field F] {H : Type u_2} [Fintype H] [DecidableEq H] {m : ℕ} (h : H ↪ F) (f : (Fin m → H) → F) : lowDegreeExtension h f ∈ reedMuller F m (m * (Fintype.card H - 1))

The low-degree extension is a Reed–Muller codeword of degree m * (|H| - 1).