Multilinearity testing

A function f : (ι → F) → F on the points of F ^ ι over a field F is multilinear when its restriction to every axis-parallel line, t ↦ f (update x i t), is affine (Cslib.Code.IsMultilinear) Babai, Fortnow, Lund, Definition 5.1. Equivalently, f evaluates the multilinear extension of its values on the cube {0, 1} ^ ι (Cslib.Code.isMultilinear_iff_eq_eval_multilinearExtension), or evaluates some polynomial of degree at most one in each variable (Cslib.Code.isMultilinear_iff_exists_mem_restrictDegree). The proof of uniqueness pushes zeros off the cube one coordinate at a time: an affine function of one variable vanishing at 0 and 1 vanishes everywhere.

The multilinearity test picks a uniformly random direction i and a uniformly random point x, reads f on the whole axis-parallel line through x in direction i, and accepts when that restriction is affine. Its rejection probability Cslib.Code.multilinearityTestRejection is the average, over the directions, of the proportion of lines in that direction on which f is not affine. In the terms of Babai, Fortnow, Lund, Definition 5.3, it accepts exactly the correct lines, those on which f is linear; wrongPoints f i collects the points of the lines in direction i that are not correct. Their δ-wrong lines are those on which f is not δ-approximately linear, and since their δ-approximation is strict (fewer than δ |X| disagreements, Definition 3.4), for every δ ∈ (0, 1] a δ-wrong line is not correct. So the proportion of lines in direction i that are not correct bounds their proportion of wrong lines for every such δ. Our test differs from theirs (Section 5.1) in reading whole lines, where their subtest samples m₁ + 2 points of a line, and in sampling one random direction, where their test samples lines in every direction.

• Completeness and zero-error soundness: the test rejects with probability zero exactly when f is multilinear (Cslib.Code.multilinearityTestRejection_eq_zero_iff).
• Quantitative soundness (Cslib.Code.exists_isMultilinear_hammingDist_le): over F ^ n, some multilinear g differs from f on at most ∑ i, 2 ^ i * #(wrongPoints f i) points, where wrongPoints f i is the set of points whose line in direction i is not affine. So f is within relative distance n * 2 ^ (n - 1) * ρ of a multilinear function, where ρ is the rejection probability (Cslib.Code.exists_isMultilinear_hammingDist_div_le).

The quantitative bound is original, and it is weaker than the literature's: its constant is exponential in the dimension. Its proof adapts the interpolation step in the proof of Babai, Fortnow, Lund, Lemma 5.11 and inducts on the dimension, without their self-improvement lemma: interpolating multilinear approximations of the two best slices x 0 = t₁ and x 0 = t₂ gives a multilinear function that agrees with f on every direction-0 line that is affine and on which both slices are correct. Babai, Fortnow and Lund prove a bound polynomial in the dimension: if in every direction the proportion of δ-wrong lines is less than ε, then f is 3 n ^ 2 (ε + δ + 1 / N)-approximately multilinear when N ≥ 40 n ^ 2, δ ≤ 1 / (400 n ^ 2) and ε ≤ 1 / (800 n ^ 3) [Babai, Fortnow, Lund, Theorem 5.13] [BFL91]. That bound, for the whole-line test, is Cslib.Code.exists_isMultilinear_hammingDist_lt, in the module Complexity.Foundations.Data.Code.MultilinearitySoundness.

Main definitions

• Cslib.Code.lineRestrict: the restriction of a function to an axis-parallel line.
• Cslib.Code.IsAffineFun: a function of one variable is affine.
• Cslib.Code.IsMultilinear: every axis-parallel restriction is affine.
• Cslib.Code.wrongPoints: the points whose line in a given direction is not affine.
• Cslib.Code.multilinearityTestRejection: the rejection probability of the multilinearity test.

Main results

• Cslib.Code.IsAffineFun.eq_of_eq_of_eq: affine functions agreeing at two points are equal.
• Cslib.Code.IsMultilinear.eq_zero_of_forall_bitPoint: a multilinear function vanishing on the cube vanishes.
• Cslib.Code.isMultilinear_eval_multilinearExtension, Cslib.Code.isMultilinear_iff_eq_eval_multilinearExtension: multilinear functions are the multilinear extensions of functions on the cube.
• Cslib.Code.isAffineFun_iff_exists_affineMap: affine functions of one variable are affine maps.
• Cslib.BitString.indicatorPoly_mem_restrictDegree, Cslib.BitString.multilinearExtension_mem_restrictDegree: multilinear extensions have degree at most one in each variable.
• Cslib.Code.isMultilinear_eval_of_mem_restrictDegree, Cslib.Code.isMultilinear_iff_exists_mem_restrictDegree: multilinear functions are the evaluations of polynomials of degree at most one in each variable.
• Cslib.Code.multilinearityTestRejection_eq_zero_iff: completeness and zero-error soundness.
• Cslib.Code.card_wrongPoints_succ: the wrong points in direction j.succ are those of the slices in direction j.
• Cslib.Code.exists_isMultilinear_hammingDist_le_of_slices: interpolating multilinear approximations of two slices.
• Cslib.Code.exists_isMultilinear_hammingDist_le, Cslib.Code.exists_isMultilinear_hammingDist_div_le: quantitative soundness with a constant exponential in the dimension.

References

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

Affine functions of one variable

def Cslib.Code.IsAffineFun {F : Type u_1} [Field F] (g : F → F) : Prop

A function of one variable over a field is affine when it is t ↦ a * t + b for some a and b, that is, the underlying function of an affine map F →ᵃ[F] F (Cslib.Code.isAffineFun_iff_exists_affineMap). Babai, Fortnow and Lund call such functions linear. This is not Cslib.BitString.IsAffine, which asks that a map preserve sums of three points.

@[instance_reducible]

instance Cslib.Code.instDecidablePredForallIsAffineFunOfFintypeOfDecidableEq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] : DecidablePred IsAffineFun

theorem Cslib.Code.isAffineFun_iff {F : Type u_1} [Field F] {g : F → F} : IsAffineFun g ↔ ∀ (t : F), g t = (g 1 - g 0) * t + g 0

An affine function is determined by its values at 0 and 1.

theorem Cslib.Code.isAffineFun_iff_exists_affineMap {F : Type u_1} [Field F] {g : F → F} : IsAffineFun g ↔ ∃ (φ : F →ᵃ[F] F), ⇑φ = g

Affine functions of one variable are the underlying functions of Mathlib's affine maps.

theorem Cslib.Code.isAffineFun_const {F : Type u_1} [Field F] (c : F) : IsAffineFun fun (x : F) => c

A constant function is affine.

theorem Cslib.Code.isAffineFun_id {F : Type u_1} [Field F] : IsAffineFun fun (t : F) => t

The identity is affine.

theorem Cslib.Code.isAffineFun_one_sub {F : Type u_1} [Field F] : IsAffineFun fun (t : F) => 1 - t

t ↦ 1 - t is affine.

theorem Cslib.Code.IsAffineFun.add {F : Type u_1} [Field F] {g h : F → F} (hg : IsAffineFun g) (hh : IsAffineFun h) : IsAffineFun fun (t : F) => g t + h t

The sum of affine functions is affine.

theorem Cslib.Code.IsAffineFun.sub {F : Type u_1} [Field F] {g h : F → F} (hg : IsAffineFun g) (hh : IsAffineFun h) : IsAffineFun fun (t : F) => g t - h t

The difference of affine functions is affine.

theorem Cslib.Code.IsAffineFun.const_mul {F : Type u_1} [Field F] {g : F → F} (hg : IsAffineFun g) (c : F) : IsAffineFun fun (t : F) => c * g t

A constant multiple of an affine function is affine.

theorem Cslib.Code.IsAffineFun.mul_const {F : Type u_1} [Field F] {g : F → F} (hg : IsAffineFun g) (c : F) : IsAffineFun fun (t : F) => g t * c

An affine function times a constant is affine.

theorem Cslib.Code.isAffineFun_sum {F : Type u_1} [Field F] {κ : Type u_3} (s : Finset κ) {g : κ → F → F} (hg : ∀ k ∈ s, IsAffineFun (g k)) : IsAffineFun fun (t : F) => ∑ k ∈ s, g k t

A finite sum of affine functions is affine.

theorem Cslib.Code.IsAffineFun.eq_of_eq_of_eq {F : Type u_1} [Field F] {g h : F → F} (hg : IsAffineFun g) (hh : IsAffineFun h) {s u : F} (hsu : s ≠ u) (hs : g s = h s) (hu : g u = h u) : g = h

Affine functions agreeing at two points are equal.

Multilinear extensions have degree at most one in each variable

theorem Cslib.BitString.indicatorPoly_mem_restrictDegree {ι : Type u_2} {R : Type u_3} [CommRing R] [Fintype ι] (a : ι → Bool) : indicatorPoly a ∈ MvPolynomial.restrictDegree ι R 1

An indicator polynomial has degree at most one in each variable.

theorem Cslib.BitString.multilinearExtension_mem_restrictDegree {ι : Type u_2} {R : Type u_3} [CommRing R] [Fintype ι] [DecidableEq ι] (g : (ι → Bool) → R) : multilinearExtension g ∈ MvPolynomial.restrictDegree ι R 1

The multilinear extension of a function on the cube has degree at most one in each variable.

Multilinear functions

def Cslib.Code.lineRestrict {F : Type u_1} {ι : Type u_2} [DecidableEq ι] (f : (ι → F) → F) (x : ι → F) (i : ι) (t : F) : F

The restriction of f to the axis-parallel line through x in direction i: t ↦ f (update x i t).

def Cslib.Code.IsMultilinear {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] (f : (ι → F) → F) : Prop

A function on F ^ ι is multilinear when its restriction to every axis-parallel line is affine Babai, Fortnow, Lund, Definition 5.1.

@[simp]

theorem Cslib.Code.lineRestrict_self {F : Type u_1} {ι : Type u_2} [DecidableEq ι] (f : (ι → F) → F) (x : ι → F) (i : ι) : lineRestrict f x i (x i) = f x

The restriction of f to a line, read at the point where the line passes through x, is f x.

theorem Cslib.Code.IsMultilinear.sub {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] {f g : (ι → F) → F} (hf : IsMultilinear f) (hg : IsMultilinear g) : IsMultilinear (f - g)

The difference of multilinear functions is multilinear.

theorem Cslib.Code.IsMultilinear.eq_zero_of_forall_bitPoint {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] [Finite ι] {h : (ι → F) → F} (hh : IsMultilinear h) (h0 : ∀ (b : ι → Bool), h (BitString.bitPoint b) = 0) : h = 0

Uniqueness: a multilinear function vanishing on the cube {0, 1} ^ ι vanishes.

theorem Cslib.Code.isMultilinear_eval_multilinearExtension {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] [Fintype ι] (g : (ι → Bool) → F) : IsMultilinear fun (x : ι → F) => (MvPolynomial.eval x) (BitString.multilinearExtension g)

The multilinear extension of a function on the cube is multilinear.

theorem Cslib.Code.isMultilinear_iff_eq_eval_multilinearExtension {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] [Fintype ι] {f : (ι → F) → F} : IsMultilinear f ↔ f = fun (x : ι → F) => (MvPolynomial.eval x) (BitString.multilinearExtension fun (b : ι → Bool) => f (BitString.bitPoint b))

Multilinear functions are multilinear extensions: a function on F ^ ι is multilinear exactly when it evaluates the multilinear extension of its values on the cube.

theorem Cslib.Code.isMultilinear_eval_of_mem_restrictDegree {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] [Finite ι] {P : MvPolynomial ι F} (hP : P ∈ MvPolynomial.restrictDegree ι F 1) : IsMultilinear fun (x : ι → F) => (MvPolynomial.eval x) P

The evaluation of a polynomial of degree at most one in each variable is multilinear.

theorem Cslib.Code.isMultilinear_iff_exists_mem_restrictDegree {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] [Finite ι] {f : (ι → F) → F} : IsMultilinear f ↔ ∃ P ∈ MvPolynomial.restrictDegree ι F 1, f = fun (x : ι → F) => (MvPolynomial.eval x) P

Multilinear functions are polynomials of degree at most one in each variable.

The multilinearity test

def Cslib.Code.wrongPoints {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] [Fintype ι] [Fintype F] [DecidableEq F] (f : (ι → F) → F) (i : ι) : Finset (ι → F)

The points whose axis-parallel line in direction i carries a restriction of f that is not affine. Each wrong line contributes all of its |F| points.

noncomputable def Cslib.Code.multilinearityTestRejection {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] [Fintype ι] [Fintype F] [DecidableEq F] (f : (ι → F) → F) : ℝ

The rejection probability of the multilinearity test on f: the probability, over a uniformly random direction i and a uniformly random point x, that the restriction of f to the axis-parallel line through x in direction i is not affine. The test reads f on the whole line.

theorem Cslib.Code.multilinearityTestRejection_eq {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] [Fintype ι] [Fintype F] [DecidableEq F] (f : (ι → F) → F) : multilinearityTestRejection f = Finset.univ.expect fun (i : ι) => ↑(wrongPoints f i).card / ↑(Fintype.card (ι → F))

The rejection probability averages, over the directions, the proportion of wrong points.

theorem Cslib.Code.multilinearityTestRejection_nonneg {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] [Fintype ι] [Fintype F] [DecidableEq F] (f : (ι → F) → F) : 0 ≤ multilinearityTestRejection f

The rejection probability is nonnegative.

theorem Cslib.Code.multilinearityTestRejection_eq_zero_iff {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] [Fintype ι] [Fintype F] [DecidableEq F] {f : (ι → F) → F} : multilinearityTestRejection f = 0 ↔ IsMultilinear f

Completeness and zero-error soundness of the multilinearity test: it rejects with probability zero exactly when f is multilinear.

theorem Cslib.Code.IsMultilinear.multilinearityTestRejection_eq_zero {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq ι] [Fintype ι] [Fintype F] [DecidableEq F] {f : (ι → F) → F} (hf : IsMultilinear f) : multilinearityTestRejection f = 0

Completeness of the multilinearity test: a multilinear function is never rejected.

Quantitative soundness

theorem Cslib.Code.card_wrongPoints_succ {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (f : (Fin (n + 1) → F) → F) (j : Fin n) : (wrongPoints f j.succ).card = ∑ t : F, (wrongPoints (fun (y : Fin n → F) => f (Fin.cons t y)) j).card

The wrong points of f in direction j.succ are those of its slices x 0 = t in direction j.

theorem Cslib.Code.exists_isMultilinear_hammingDist_le_of_slices {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (f : (Fin (n + 1) → F) → F) {t₁ t₂ : F} (h12 : t₁ ≠ t₂) {g₁ g₂ : (Fin n → F) → F} (hg₁ : IsMultilinear g₁) (hg₂ : IsMultilinear g₂) : ∃ (g : (Fin (n + 1) → F) → F), IsMultilinear g ∧ hammingDist f g ≤ (wrongPoints f 0).card + Fintype.card F * (hammingDist (fun (y : Fin n → F) => f (Fin.cons t₁ y)) g₁ + hammingDist (fun (y : Fin n → F) => f (Fin.cons t₂ y)) g₂)

Interpolating two slices: if g₁ and g₂ are multilinear functions on F ^ n and t₁ ≠ t₂, then interpolating them in the first coordinate gives a multilinear function on F ^ (n + 1) that differs from f only at points that are wrong in direction 0 or that lie over a point where one of the slices x 0 = t₁, x 0 = t₂ of f differs from g₁, g₂. This is the interpolation step in the proof of Babai, Fortnow, Lund, Lemma 5.11, for lines that are exactly affine.

theorem Cslib.Code.exists_isMultilinear_hammingDist_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (f : (Fin n → F) → F) : ∃ (g : (Fin n → F) → F), IsMultilinear g ∧ hammingDist f g ≤ ∑ i : Fin n, 2 ^ ↑i * (wrongPoints f i).card

Quantitative soundness of the multilinearity test, with a constant exponential in the dimension (an original bound): some multilinear g differs from f on at most ∑ i, 2 ^ i * #(wrongPoints f i) points of F ^ n. The proof interpolates multilinear approximations of the two best slices x 0 = t₁ and x 0 = t₂ and inducts on the dimension. This adapts the interpolation step in the proof of Babai, Fortnow, Lund, Lemma 5.11, without their self-improvement lemma.

theorem Cslib.Code.exists_isMultilinear_hammingDist_div_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} (f : (Fin n → F) → F) : ∃ (g : (Fin n → F) → F), IsMultilinear g ∧ ↑(hammingDist f g) / ↑(Fintype.card (Fin n → F)) ≤ ↑n * 2 ^ (n - 1) * multilinearityTestRejection f

Quantitative soundness of the multilinearity test, as a probability: some multilinear g is within relative distance n * 2 ^ (n - 1) * ρ of f, where ρ is the rejection probability of the test. The constant is exponential in the dimension; the polynomial bound of Babai, Fortnow, Lund, Theorem 5.13 is Cslib.Code.exists_isMultilinear_hammingDist_lt.