Polynomial soundness of the multilinearity test

This module proves the soundness theorem of Babai, Fortnow and Lund for the multilinearity test: if in every direction fewer than an ε fraction of the axis-parallel lines carry a restriction of f that is not affine, then f agrees with a multilinear function outside a 3 n ^ 2 (ε + 1 / |F|) fraction of the points, when |F| ≥ 40 n ^ 2 and ε ≤ 1 / (800 n ^ 3) (Cslib.Code.exists_isMultilinear_hammingDist_lt) Babai, Fortnow, Lund, Theorem 5.13.

The test here reads whole lines, so its wrong lines are the lines that are not correct in the sense of Babai, Fortnow, Lund, Definition 5.3. For every δ ∈ (0, 1] a δ-wrong line is not correct, so our hypothesis implies theirs for every such δ; our conclusion is theirs with the δ term removed, which is what their bound gives as δ tends to 0. Their condition δ ≤ 1 / (400 n ^ 2) has no counterpart.

The proof follows theirs.

• Self-improvement (Cslib.Code.IsMultilinear.hammingDist_le_of_two_mul_le, Babai, Fortnow, Lund, Lemma 5.10): a multilinear function that agrees with f on at least half of the points agrees with it outside at most (2 n + 1) ∑ᵢ |Wᵢ| + 2 n ^ 2 |F| ^ (n - 1) points, where Wᵢ is the set of points whose line in direction i is wrong. Let B be the set where they differ and S the points of B on no wrong line. A point on a line through a point of S that is outside S is on a wrong line, or is the unique point of a correct line where the two distinct affine restrictions agree. The Expansion Lemma (Cslib.card_le_two_mul_card_lineClosure_sdiff) bounds S by 2 n times those points.
• Induction on the dimension, replacing their tree coloring Babai, Fortnow, Lund, Lemma 5.12: the wrong points of the slices x 0 = t average to at most those of f, so when f has few wrong points, at least two slices have few (Markov's inequality with thresholds decreasing by a factor 1 - 1 / |F| per dimension). By induction they are close to multilinear functions; interpolating those (Cslib.Code.exists_isMultilinear_hammingDist_le_of_slices, the interpolation step of Babai, Fortnow, Lund, Lemma 5.11) gives a multilinear function within half of the points, and self-improvement brings it within a fifth.

The induction on slices in one direction, which needs only two good slices, is our simplification of their tree argument over hyperplanes in all directions.

Main results

• Cslib.Code.IsMultilinear.hammingDist_le_of_two_mul_le: the self-improvement lemma.
• Cslib.Code.exists_isMultilinear_hammingDist_lt: polynomial soundness of the multilinearity test.

References

• L. Babai, L. Fortnow, C. Lund, Non-deterministic exponential time has two-prover interactive protocols, Section 5

theorem Cslib.Code.IsMultilinear.hammingDist_le_of_two_mul_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} {f g : (Fin n → F) → F} (hg : IsMultilinear g) (h : 2 * hammingDist f g ≤ Fintype.card F ^ n) : hammingDist f g ≤ (2 * n + 1) * ∑ i : Fin n, (wrongPoints f i).card + 2 * n ^ 2 * Fintype.card F ^ (n - 1)

The self-improvement lemma: a multilinear function g that agrees with f on at least half of the points agrees with it outside at most (2 n + 1) ∑ᵢ |Wᵢ| + 2 n ^ 2 |F| ^ (n - 1) points, where Wᵢ = wrongPoints f i Babai, Fortnow, Lund, Lemma 5.10.

theorem Cslib.Code.exists_isMultilinear_hammingDist_lt {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (f : (Fin n → F) → F) {ε : ℝ} (hn : 0 < n) (hq : 40 * n ^ 2 ≤ Fintype.card F) (hε : ε ≤ 1 / (800 * ↑n ^ 3)) (hW : ∀ (i : Fin n), ↑(wrongPoints f i).card < ε * ↑(Fintype.card F) ^ n) : ∃ (g : (Fin n → F) → F), IsMultilinear g ∧ ↑(hammingDist f g) < 3 * ↑n ^ 2 * (ε + 1 / ↑(Fintype.card F)) * ↑(Fintype.card F) ^ n

Polynomial soundness of the multilinearity test: if in every direction fewer than an ε fraction of the lines carry a restriction of f that is not affine, |F| ≥ 40 n ^ 2 and ε ≤ 1 / (800 n ^ 3), then some multilinear function agrees with f outside fewer than a 3 n ^ 2 (ε + 1 / |F|) fraction of the points Babai, Fortnow, Lund, Theorem 5.13, for the whole-line test, where their δ term vanishes.