diff --git a/Complexity.lean b/Complexity.lean index a2f36969fc..7a26b70d90 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1803,6 +1803,7 @@ public import Complexity.Foundations.Data.Code.LocalDecoding public import Complexity.Foundations.Data.Code.LocalListDecoding public import Complexity.Foundations.Data.Code.LowDegreeExtension public import Complexity.Foundations.Data.Code.Multilinearity +public import Complexity.Foundations.Data.Code.MultilinearitySoundness public import Complexity.Foundations.Data.Code.ReedMuller public import Complexity.Foundations.Data.Code.ReedSolomon public import Complexity.Foundations.Data.Code.SelfCorrection @@ -1818,6 +1819,7 @@ public import Complexity.Foundations.Data.Finset.Quantile public import Complexity.Foundations.Data.Finset.Sampling public import Complexity.Foundations.Data.Finset.SymmDiff public import Complexity.Foundations.Data.Hamming +public import Complexity.Foundations.Data.Hamming.Expansion public import Complexity.Foundations.Data.Int.Order public import Complexity.Foundations.Data.List.Append public import Complexity.Foundations.Data.List.BalancedFold diff --git a/Complexity/Foundations/Data/Code/Multilinearity.lean b/Complexity/Foundations/Data/Code/Multilinearity.lean index f0099acec1..b9e041012a 100644 --- a/Complexity/Foundations/Data/Code/Multilinearity.lean +++ b/Complexity/Foundations/Data/Code/Multilinearity.lean @@ -61,8 +61,9 @@ direction-`0` line that is affine and on which both slices are correct. Babai, F 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] -[BabaiFortnowLund1991]. That bound, which needs their expansion, self-improvement and tree coloring -lemmas, is not formalized here. +[BabaiFortnowLund1991]. That bound, for the whole-line test, is +`Cslib.Code.exists_isMultilinear_hammingDist_lt`, in the module +`Complexity.Foundations.Data.Code.MultilinearitySoundness`. ## Main definitions @@ -88,6 +89,10 @@ lemmas, is not formalized here. `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. @@ -454,8 +459,9 @@ private theorem lineRestrict_succ (f : (Fin (n + 1) → F) → F) (x : Fin (n + funext t simp only [lineRestrict, Fin.cons_update, Fin.cons_self_tail] -/-- The wrong points of `f` in direction `j.succ` are those of its slices in direction `j`. -/ -private theorem card_wrongPoints_succ (f : (Fin (n + 1) → F) → F) (j : Fin n) : +/-- The wrong points of `f` in direction `j.succ` are those of its slices `x 0 = t` in direction +`j`. -/ +theorem card_wrongPoints_succ (f : (Fin (n + 1) → F) → F) (j : Fin n) : #(wrongPoints f j.succ) = ∑ t, #(wrongPoints (fun y => f (Fin.cons t y)) j) := by have : wrongPoints f j.succ = ({x | ¬IsAffineFun (lineRestrict (fun y => f (Fin.cons (x 0) y)) (Fin.tail x) j)} : Finset (Fin (n + 1) → F)) := by @@ -489,6 +495,70 @@ private theorem exists_two_mul_le_sum (D : F → ℕ) : rw [show m + 2 - 1 = m + 1 by omega] at hsum nlinarith +/-- **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][BabaiFortnowLund1991], +for lines that are exactly affine. -/ +theorem exists_isMultilinear_hammingDist_le_of_slices (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, IsMultilinear g ∧ hammingDist f g ≤ #(wrongPoints f 0) + + Fintype.card F * (hammingDist (fun y => f (Fin.cons t₁ y)) g₁ + + hammingDist (fun y => f (Fin.cons t₂ y)) g₂) := by + have hd : t₂ - t₁ ≠ 0 := sub_ne_zero.mpr h12.symm + -- The interpolation of `g₁` and `g₂` in the first coordinate. + let g : (Fin (n + 1) → F) → F := fun x => + g₁ (Fin.tail x) + (x 0 - t₁) / (t₂ - t₁) * (g₂ (Fin.tail x) - g₁ (Fin.tail x)) + have hg0 (x : Fin (n + 1) → F) : lineRestrict g x 0 = fun t => + g₁ (Fin.tail x) + (t - t₁) / (t₂ - t₁) * (g₂ (Fin.tail x) - g₁ (Fin.tail x)) := by + funext t + simp only [g, lineRestrict, Fin.tail_update_zero, update_self] + have hg : IsMultilinear g := by + intro x i + induction i using Fin.cases with + | zero => + rw [hg0] + exact ⟨(g₂ (Fin.tail x) - g₁ (Fin.tail x)) / (t₂ - t₁), + g₁ (Fin.tail x) - t₁ * ((g₂ (Fin.tail x) - g₁ (Fin.tail x)) / (t₂ - t₁)), + fun t => by ring⟩ + | succ j => + have : lineRestrict g x j.succ = fun t => lineRestrict g₁ (Fin.tail x) j t + + (x 0 - t₁) / (t₂ - t₁) * + (lineRestrict g₂ (Fin.tail x) j t - lineRestrict g₁ (Fin.tail x) j t) := by + funext t + simp only [g, lineRestrict, Fin.tail_update_succ, + update_of_ne (Fin.succ_ne_zero j).symm] + rw [this] + exact (hg₁ _ j).add (((hg₂ _ j).sub (hg₁ _ j)).const_mul _) + refine ⟨g, hg, ?_⟩ + -- Every point where `f` and `g` differ is wrong in direction `0`, or lies over a point where + -- one of the two slices differs from its approximation. + let bad (t : F) (h : (Fin n → F) → F) : Finset (Fin (n + 1) → F) := + {x | f (Fin.cons t (Fin.tail x)) ≠ h (Fin.tail x)} + have hsub : ({x | f x ≠ g x} : Finset (Fin (n + 1) → F)) ⊆ + wrongPoints f 0 ∪ (bad t₁ g₁ ∪ bad t₂ g₂) := by + intro x hx + simp only [wrongPoints, bad, mem_filter, mem_univ, true_and, mem_union] at hx ⊢ + by_contra! hc + obtain ⟨haff, h1, h2⟩ := hc + have hcons (t : F) : update x 0 t = Fin.cons t (Fin.tail x) := by + rw [← Fin.update_cons_zero (x 0) (Fin.tail x) t, Fin.cons_self_tail] + have hline := haff.eq_of_eq_of_eq (hg x 0) h12 + (by rw [hg0]; simp only [lineRestrict, hcons, h1, sub_self, zero_div, zero_mul, add_zero]) + (by rw [hg0]; simp only [lineRestrict, hcons, h2, div_self hd, one_mul, + add_sub_cancel]) + exact hx (by simpa using congrFun hline (x 0)) + have hcard (t : F) (h : (Fin n → F) → F) : + #(bad t h) = Fintype.card F * hammingDist (fun y => f (Fin.cons t y)) h := by + rw [card_filter_zero_tail (fun _ y => f (Fin.cons t y) ≠ h y), sum_const, card_univ, + smul_eq_mul, hammingDist] + calc hammingDist f g = #({x | f x ≠ g x} : Finset (Fin (n + 1) → F)) := rfl + _ ≤ #(wrongPoints f 0) + (#(bad t₁ g₁) + #(bad t₂ g₂)) := + (card_le_card hsub).trans ((card_union_le _ _).trans + (Nat.add_le_add_left (card_union_le _ _) _)) + _ = _ := by rw [hcard, hcard, mul_add] + /-- **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 @@ -503,64 +573,11 @@ theorem exists_isMultilinear_hammingDist_le (f : (Fin n → F) → F) : choose gs hgs hdist using fun t : F => ih fun y => f (Fin.cons t y) obtain ⟨t₁, t₂, h12, hD⟩ := exists_two_mul_le_sum fun t => hammingDist (fun y => f (Fin.cons t y)) (gs t) - have hd : t₂ - t₁ ≠ 0 := sub_ne_zero.mpr h12.symm - -- The interpolation of `gs t₁` and `gs t₂` in the first coordinate. - let g : (Fin (n + 1) → F) → F := fun x => - gs t₁ (Fin.tail x) + (x 0 - t₁) / (t₂ - t₁) * (gs t₂ (Fin.tail x) - gs t₁ (Fin.tail x)) - have hg0 (x : Fin (n + 1) → F) : lineRestrict g x 0 = fun t => - gs t₁ (Fin.tail x) + (t - t₁) / (t₂ - t₁) * (gs t₂ (Fin.tail x) - gs t₁ (Fin.tail x)) := by - funext t - simp only [g, lineRestrict, Fin.tail_update_zero, update_self] - have hg : IsMultilinear g := by - intro x i - induction i using Fin.cases with - | zero => - rw [hg0] - exact ⟨(gs t₂ (Fin.tail x) - gs t₁ (Fin.tail x)) / (t₂ - t₁), - gs t₁ (Fin.tail x) - t₁ * ((gs t₂ (Fin.tail x) - gs t₁ (Fin.tail x)) / (t₂ - t₁)), - fun t => by ring⟩ - | succ j => - have : lineRestrict g x j.succ = fun t => lineRestrict (gs t₁) (Fin.tail x) j t + - (x 0 - t₁) / (t₂ - t₁) * - (lineRestrict (gs t₂) (Fin.tail x) j t - lineRestrict (gs t₁) (Fin.tail x) j t) := by - funext t - simp only [g, lineRestrict, Fin.tail_update_succ, - update_of_ne (Fin.succ_ne_zero j).symm] - rw [this] - exact (hgs t₁ _ j).add (((hgs t₂ _ j).sub (hgs t₁ _ j)).const_mul _) + obtain ⟨g, hg, hfg⟩ := exists_isMultilinear_hammingDist_le_of_slices f h12 (hgs t₁) (hgs t₂) refine ⟨g, hg, ?_⟩ - -- Every point where `f` and `g` differ is wrong in direction `0`, or lies over a point where - -- one of the two slices differs from its approximation. - let bad (t : F) : Finset (Fin (n + 1) → F) := - {x | f (Fin.cons t (Fin.tail x)) ≠ gs t (Fin.tail x)} - have hsub : ({x | f x ≠ g x} : Finset (Fin (n + 1) → F)) ⊆ - wrongPoints f 0 ∪ (bad t₁ ∪ bad t₂) := by - intro x hx - simp only [wrongPoints, bad, mem_filter, mem_univ, true_and, mem_union] at hx ⊢ - by_contra! hc - obtain ⟨haff, h1, h2⟩ := hc - have hcons (t : F) : update x 0 t = Fin.cons t (Fin.tail x) := by - rw [← Fin.update_cons_zero (x 0) (Fin.tail x) t, Fin.cons_self_tail] - have hline := haff.eq_of_eq_of_eq (hg x 0) h12 - (by rw [hg0]; simp only [lineRestrict, hcons, h1, sub_self, zero_div, zero_mul, add_zero]) - (by rw [hg0]; simp only [lineRestrict, hcons, h2, div_self hd, one_mul, - add_sub_cancel]) - exact hx (by simpa using congrFun hline (x 0)) - have hcard (t : F) : - #(bad t) = Fintype.card F * hammingDist (fun y => f (Fin.cons t y)) (gs t) := by - rw [card_filter_zero_tail (fun _ y => f (Fin.cons t y) ≠ gs t y), sum_const, card_univ, - smul_eq_mul, hammingDist] - calc hammingDist f g = #({x | f x ≠ g x} : Finset (Fin (n + 1) → F)) := rfl - _ ≤ #(wrongPoints f 0) + (Fintype.card F * - hammingDist (fun y => f (Fin.cons t₁ y)) (gs t₁) + - Fintype.card F * hammingDist (fun y => f (Fin.cons t₂ y)) (gs t₂)) := by - rw [← hcard, ← hcard] - exact (card_le_card hsub).trans ((card_union_le _ _).trans - (Nat.add_le_add_left (card_union_le _ _) _)) - _ ≤ #(wrongPoints f 0) + - 2 * ∑ t, hammingDist (fun y => f (Fin.cons t y)) (gs t) := by - rw [← mul_add] - exact Nat.add_le_add_left hD _ + calc hammingDist f g ≤ #(wrongPoints f 0) + + 2 * ∑ t, hammingDist (fun y => f (Fin.cons t y)) (gs t) := + hfg.trans (Nat.add_le_add_left hD _) _ ≤ #(wrongPoints f 0) + 2 * ∑ t, ∑ j : Fin n, 2 ^ (j : ℕ) * #(wrongPoints (fun y => f (Fin.cons t y)) j) := Nat.add_le_add_left (Nat.mul_le_mul_left _ (sum_le_sum fun t _ => hdist t)) _ @@ -574,7 +591,8 @@ theorem exists_isMultilinear_hammingDist_le (f : (Fin n → F) → 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][BabaiFortnowLund1991] is not formalized here. -/ +[Babai, Fortnow, Lund, Theorem 5.13][BabaiFortnowLund1991] is +`Cslib.Code.exists_isMultilinear_hammingDist_lt`. -/ theorem exists_isMultilinear_hammingDist_div_le (f : (Fin n → F) → F) : ∃ g, IsMultilinear g ∧ (hammingDist f g : ℝ) / Fintype.card (Fin n → F) ≤ n * 2 ^ (n - 1) * multilinearityTestRejection f := by diff --git a/Complexity/Foundations/Data/Code/MultilinearitySoundness.lean b/Complexity/Foundations/Data/Code/MultilinearitySoundness.lean new file mode 100644 index 0000000000..69db47a410 --- /dev/null +++ b/Complexity/Foundations/Data/Code/MultilinearitySoundness.lean @@ -0,0 +1,365 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Data.Code.Multilinearity +public import Complexity.Foundations.Data.Hamming.Expansion +import Mathlib.Algebra.Order.Field.Basic +import Mathlib.Algebra.Order.Ring.Pow +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity + +/-! +# 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][BabaiFortnowLund1991]. + +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][BabaiFortnowLund1991]. 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][BabaiFortnowLund1991]): 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][BabaiFortnowLund1991]: 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][BabaiFortnowLund1991]) 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*][BabaiFortnowLund1991], Section 5 +-/ + +@[expose] public section + +namespace Cslib.Code + +open Finset Function + +variable {F : Type*} [Field F] [Fintype F] [DecidableEq F] {n : ℕ} + +/-- The points where the restrictions of `f` and `g` to the line in direction `i` are both affine +and distinct, but `f` and `g` agree: at most one on each line. -/ +private def agreePoints (f g : (Fin n → F) → F) (i : Fin n) : Finset (Fin n → F) := + {x | IsAffineFun (lineRestrict f x i) ∧ lineRestrict f x i ≠ lineRestrict g x i ∧ f x = g x} + +omit [Field F] [Fintype F] [DecidableEq F] in +private theorem lineRestrict_update (f : (Fin n → F) → F) (x : Fin n → F) (i : Fin n) (t : F) : + lineRestrict f (update x i t) i = lineRestrict f x i := by + funext s + simp [lineRestrict] + +/-- Each line in direction `i` has at most one point where two distinct affine restrictions +agree, so there are at most `|F| ^ (n - 1)` such points. -/ +private theorem card_agreePoints_le {f g : (Fin n → F) → F} (hg : IsMultilinear g) (i : Fin n) : + #(agreePoints f g i) ≤ Fintype.card F ^ (n - 1) := by + have hfib : #{y : Fin n → F | y i = 0} = Fintype.card F ^ (n - 1) := by + have := Fintype.card_filter_piFinset_const_eq_of_mem (univ : Finset F) i (mem_univ 0) + simpa [Fintype.piFinset_univ] using this + rw [← hfib] + refine card_le_card_of_injOn (fun x => update x i 0) (fun x _ => by simp) ?_ + intro x hx x' hx' hxx' + simp only [agreePoints, coe_filter, mem_univ, true_and, Set.mem_ofPred_eq] at hx hx' + have hf : lineRestrict f x i = lineRestrict f x' i := by + rw [← lineRestrict_update f x i 0, ← lineRestrict_update f x' i 0] + exact congrArg (lineRestrict f · i) hxx' + have hg' : lineRestrict g x i = lineRestrict g x' i := by + rw [← lineRestrict_update g x i 0, ← lineRestrict_update g x' i 0] + exact congrArg (lineRestrict g · i) hxx' + have hxi : x i = x' i := by + by_contra hne + refine hx.2.1 (hx.1.eq_of_eq_of_eq (hg x i) hne ?_ ?_) + · simpa [lineRestrict] using hx.2.2 + · rw [hf, hg'] + simpa [lineRestrict] using hx'.2.2 + calc x = update (update x i 0) i (x i) := by simp + _ = update (update x' i 0) i (x' i) := by + rw [show update x i 0 = update x' i 0 from hxx', hxi] + _ = x' := by simp + +/-- **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][BabaiFortnowLund1991]. -/ +theorem IsMultilinear.hammingDist_le_of_two_mul_le {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, #(wrongPoints f i) + 2 * n ^ 2 * Fintype.card F ^ (n - 1) := by + let B : Finset (Fin n → F) := {x | f x ≠ g x} + let W : Finset (Fin n → F) := univ.biUnion (wrongPoints f) + let I : Finset (Fin n → F) := univ.biUnion (agreePoints f g) + let S : Finset (Fin n → F) := B \ W + have hB : #B = hammingDist f g := rfl + -- A point outside `S` on a line through a point of `S` is wrong or an agreement point. + have hcl : lineClosure S \ S ⊆ W ∪ I := by + intro y hy + simp only [mem_sdiff, mem_lineClosure] at hy + obtain ⟨⟨i, t, hs⟩, hyS⟩ := hy + simp only [S, B, W, mem_sdiff, mem_filter, mem_univ, true_and, mem_biUnion, + not_exists] at hs hyS + simp only [W, I, mem_union, mem_biUnion, mem_univ, true_and] + by_cases hyW : ∃ j, y ∈ wrongPoints f j + · exact Or.inl hyW + right + push Not at hyW + have hfy : f y = g y := by + by_contra hne + exact hyS ⟨hne, hyW⟩ + have hcorr : IsAffineFun (lineRestrict f y i) := by + have := hs.2 i + simp only [wrongPoints, mem_filter, mem_univ, true_and, not_not] at this + rwa [lineRestrict_update] at this + refine ⟨i, ?_⟩ + simp only [agreePoints, mem_filter, mem_univ, true_and] + refine ⟨hcorr, fun heq => hs.1 ?_, hfy⟩ + have := congrFun heq t + simpa [lineRestrict] using this + have hexp : #S ≤ 2 * n * #(lineClosure S \ S) := by + refine card_le_two_mul_card_lineClosure_sdiff ?_ + exact (Nat.mul_le_mul_left 2 (card_le_card sdiff_subset)).trans (hB ▸ h) + have hW : #W ≤ ∑ i, #(wrongPoints f i) := card_biUnion_le + have hI : #I ≤ n * Fintype.card F ^ (n - 1) := by + refine card_biUnion_le.trans ?_ + calc ∑ i, #(agreePoints f g i) ≤ ∑ _i : Fin n, Fintype.card F ^ (n - 1) := + sum_le_sum fun i _ => card_agreePoints_le hg i + _ = n * Fintype.card F ^ (n - 1) := by simp + have hBS : #B ≤ #S + #W := by + refine (card_le_card ?_).trans (card_union_le S W) + intro x hx + by_cases hxW : x ∈ W + · exact mem_union_right _ hxW + · exact mem_union_left _ (mem_sdiff.mpr ⟨hx, hxW⟩) + have hcl' := (card_le_card hcl).trans (card_union_le W I) + rw [← hB] + calc #B ≤ 2 * n * (#W + #I) + #W := by nlinarith + _ ≤ 2 * n * (∑ i, #(wrongPoints f i) + n * Fintype.card F ^ (n - 1)) + + ∑ i, #(wrongPoints f i) := by gcongr + _ = _ := by ring + +/-- The wrong points of the slices `x 0 = t` add up to at most those of `f`. -/ +private theorem sum_sum_card_wrongPoints_le (f : (Fin (n + 1) → F) → F) : + ∑ t, ∑ j : Fin n, #(wrongPoints (fun y => f (Fin.cons t y)) j) ≤ + ∑ i, #(wrongPoints f i) := by + rw [Fin.sum_univ_succ, sum_comm] + simp only [← card_wrongPoints_succ] + exact Nat.le_add_left _ _ + +/-- The induction on the dimension: with thresholds decreasing by a factor `1 - 1 / |F|` per +dimension, a function with few wrong points is within `γ` of a multilinear function. -/ +private theorem exists_isMultilinear_hammingDist_le_mul {ε₀ γ : ℝ} (hε₀ : 0 ≤ ε₀) + (hγ : ε₀ + 2 * γ ≤ 1 / 2) : + ∀ k : ℕ, (2 * k + 1) * ε₀ + 2 * k ^ 2 / (Fintype.card F : ℝ) ≤ γ → + ∀ h : (Fin k → F) → F, (∑ i, (#(wrongPoints h i) : ℝ)) < + (1 - 1 / (Fintype.card F : ℝ)) ^ k * ε₀ * (Fintype.card F : ℝ) ^ k → + ∃ g, IsMultilinear g ∧ (hammingDist h g : ℝ) ≤ γ * (Fintype.card F : ℝ) ^ k := by + have hq : (0 : ℝ) < Fintype.card F := by exact_mod_cast Fintype.card_pos + have hq2 : 2 ≤ Fintype.card F := Fintype.one_lt_card + have hq1 : (1 : ℝ) ≤ Fintype.card F := by exact_mod_cast (by omega : 1 ≤ Fintype.card F) + have key : (1 - 1 / (Fintype.card F : ℝ)) * Fintype.card F = Fintype.card F - 1 := by + field_simp + intro k + induction k with + | zero => + intro hk h _ + refine ⟨h, fun _ i => i.elim0, ?_⟩ + simp only [hammingDist_self, Nat.cast_zero, pow_zero, mul_one] + simp only [CharP.cast_eq_zero, mul_zero, add_zero, zero_add, ne_eq, OfNat.ofNat_ne_zero, + not_false_eq_true, zero_pow, zero_div] at hk + linarith + | succ k ih => + intro hk f hf + have hk' : (2 * k + 1) * ε₀ + 2 * k ^ 2 / (Fintype.card F : ℝ) ≤ γ := by + refine le_trans ?_ hk + push_cast + gcongr <;> nlinarith + -- The threshold of the slices. + obtain ⟨θ, hθ⟩ : ∃ θ : ℝ, + θ = (1 - 1 / (Fintype.card F : ℝ)) ^ k * ε₀ * (Fintype.card F : ℝ) ^ k := ⟨_, rfl⟩ + rw [← hθ] at ih + have hT : (∑ i, (#(wrongPoints f i) : ℝ)) < ((Fintype.card F : ℝ) - 1) * θ := by + calc _ < _ := hf + _ = ((1 - 1 / (Fintype.card F : ℝ)) * Fintype.card F) * + ((1 - 1 / (Fintype.card F : ℝ)) ^ k * ε₀ * (Fintype.card F : ℝ) ^ k) := by ring + _ = _ := by rw [key, hθ] + have hθpos : 0 < θ := by + have h0 : (0 : ℝ) ≤ ∑ i, (#(wrongPoints f i) : ℝ) := by positivity + have : 0 < ((Fintype.card F : ℝ) - 1) * θ := h0.trans_lt hT + exact pos_of_mul_pos_right this (by linarith) + -- At least two slices have fewer than `θ` wrong points. + let good : Finset F := {t | (∑ j, (#(wrongPoints (fun y => f (Fin.cons t y)) j) : ℝ)) < θ} + have hbad : (#goodᶜ : ℝ) * θ < ((Fintype.card F : ℝ) - 1) * θ := by + calc (#goodᶜ : ℝ) * θ = ∑ _t ∈ goodᶜ, θ := by rw [sum_const, nsmul_eq_mul] + _ ≤ ∑ t ∈ goodᶜ, (∑ j, (#(wrongPoints (fun y => f (Fin.cons t y)) j) : ℝ)) := by + refine sum_le_sum fun t ht => ?_ + simp only [good, mem_compl, mem_filter, mem_univ, true_and, not_lt] at ht + exact ht + _ ≤ ∑ t, (∑ j, (#(wrongPoints (fun y => f (Fin.cons t y)) j) : ℝ)) := + sum_le_sum_of_subset_of_nonneg (subset_univ _) fun _ _ _ => by positivity + _ ≤ ∑ i, (#(wrongPoints f i) : ℝ) := by exact_mod_cast sum_sum_card_wrongPoints_le f + _ < _ := hT + have hlt : (#goodᶜ : ℝ) < Fintype.card F - 1 := lt_of_mul_lt_mul_right hbad hθpos.le + have hlt' : #goodᶜ + 1 < Fintype.card F := by + have : ((#goodᶜ + 1 : ℕ) : ℝ) < Fintype.card F := by push_cast; linarith + exact_mod_cast this + have hcard : #good + #goodᶜ = Fintype.card F := card_add_card_compl good + obtain ⟨t₁, ht₁, t₂, ht₂, h12⟩ := one_lt_card.mp (by omega : 1 < #good) + simp only [good, mem_filter, mem_univ, true_and] at ht₁ ht₂ + obtain ⟨g₁, hg₁, hd₁⟩ := ih hk' _ ht₁ + obtain ⟨g₂, hg₂, hd₂⟩ := ih hk' _ ht₂ + obtain ⟨g, hg, hfg⟩ := exists_isMultilinear_hammingDist_le_of_slices f h12 hg₁ hg₂ + refine ⟨g, hg, ?_⟩ + -- The wrong points of `f` are few. + have hpow : (1 - 1 / (Fintype.card F : ℝ)) ^ (k + 1) ≤ 1 := by + refine pow_le_one₀ ?_ ?_ + · rw [sub_nonneg, div_le_one hq] + exact hq1 + · have : 0 ≤ 1 / (Fintype.card F : ℝ) := by positivity + linarith + have hTle : (∑ i, (#(wrongPoints f i) : ℝ)) ≤ ε₀ * (Fintype.card F : ℝ) ^ (k + 1) := by + calc _ ≤ _ := hf.le + _ ≤ 1 * ε₀ * (Fintype.card F : ℝ) ^ (k + 1) := by gcongr + _ = ε₀ * (Fintype.card F : ℝ) ^ (k + 1) := by ring + have hW0 : (#(wrongPoints f 0) : ℝ) ≤ ∑ i, (#(wrongPoints f i) : ℝ) := + single_le_sum (f := fun i => (#(wrongPoints f i) : ℝ)) (fun i _ => by positivity) + (mem_univ (0 : Fin (k + 1))) + -- The interpolation is within half of the points. + have hhalf : (hammingDist f g : ℝ) ≤ (ε₀ + 2 * γ) * (Fintype.card F : ℝ) ^ (k + 1) := by + calc (hammingDist f g : ℝ) ≤ #(wrongPoints f 0) + + (Fintype.card F : ℝ) * ((hammingDist (fun y => f (Fin.cons t₁ y)) g₁ : ℝ) + + hammingDist (fun y => f (Fin.cons t₂ y)) g₂) := by exact_mod_cast hfg + _ ≤ ε₀ * (Fintype.card F : ℝ) ^ (k + 1) + (Fintype.card F : ℝ) * + (γ * (Fintype.card F : ℝ) ^ k + γ * (Fintype.card F : ℝ) ^ k) := by + gcongr + linarith + _ = (ε₀ + 2 * γ) * (Fintype.card F : ℝ) ^ (k + 1) := by ring + have h2 : 2 * hammingDist f g ≤ Fintype.card F ^ (k + 1) := by + have hqpow : 0 ≤ (Fintype.card F : ℝ) ^ (k + 1) := by positivity + have : ((2 * hammingDist f g : ℕ) : ℝ) ≤ ((Fintype.card F ^ (k + 1) : ℕ) : ℝ) := by + push_cast + nlinarith + exact_mod_cast this + -- Self-improvement brings it within `γ`. + have hself := hg.hammingDist_le_of_two_mul_le h2 + rw [Nat.add_sub_cancel] at hself + have hself' : (hammingDist f g : ℝ) ≤ (2 * ((k + 1 : ℕ) : ℝ) + 1) * + (∑ i, (#(wrongPoints f i) : ℝ)) + 2 * ((k + 1 : ℕ) : ℝ) ^ 2 * (Fintype.card F : ℝ) ^ k := by + exact_mod_cast hself + calc (hammingDist f g : ℝ) ≤ _ := hself' + _ ≤ (2 * ((k + 1 : ℕ) : ℝ) + 1) * (ε₀ * (Fintype.card F : ℝ) ^ (k + 1)) + + 2 * ((k + 1 : ℕ) : ℝ) ^ 2 * (Fintype.card F : ℝ) ^ k := by gcongr + _ = ((2 * ((k + 1 : ℕ) : ℝ) + 1) * ε₀ + 2 * ((k + 1 : ℕ) : ℝ) ^ 2 / Fintype.card F) * + (Fintype.card F : ℝ) ^ (k + 1) := by + field_simp + ring + _ ≤ γ * (Fintype.card F : ℝ) ^ (k + 1) := by gcongr + +/-- **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][BabaiFortnowLund1991], for the whole-line test, where their +`δ` term vanishes. -/ +theorem exists_isMultilinear_hammingDist_lt (f : (Fin n → F) → F) {ε : ℝ} (hn : 0 < n) + (hq : 40 * n ^ 2 ≤ Fintype.card F) (hε : ε ≤ 1 / (800 * n ^ 3)) + (hW : ∀ i, (#(wrongPoints f i) : ℝ) < ε * Fintype.card F ^ n) : + ∃ g, IsMultilinear g ∧ + (hammingDist f g : ℝ) < 3 * n ^ 2 * (ε + 1 / Fintype.card F) * Fintype.card F ^ n := by + have hq0 : (0 : ℝ) < Fintype.card F := by exact_mod_cast Fintype.card_pos + have hnr : (1 : ℝ) ≤ n := by exact_mod_cast hn + have hqr : 40 * (n : ℝ) ^ 2 ≤ Fintype.card F := by exact_mod_cast hq + have hεpos : 0 < ε := by + have h0 : (0 : ℝ) ≤ #(wrongPoints f ⟨0, hn⟩) := by positivity + have : 0 < ε * (Fintype.card F : ℝ) ^ n := h0.trans_lt (hW ⟨0, hn⟩) + exact pos_of_mul_pos_left this (by positivity) + have hsum : (∑ i, (#(wrongPoints f i) : ℝ)) < n * ε * (Fintype.card F : ℝ) ^ n := by + calc (∑ i, (#(wrongPoints f i) : ℝ)) < ∑ _i : Fin n, ε * (Fintype.card F : ℝ) ^ n := + sum_lt_sum_of_nonempty ⟨⟨0, hn⟩, mem_univ _⟩ fun i _ => hW i + _ = n * ε * (Fintype.card F : ℝ) ^ n := by simp [mul_assoc] + -- Run the induction with `ε₀ = 2 n ε` and `γ = 1 / 5`. + have hn3 : (1 : ℝ) ≤ n ^ 3 := one_le_pow₀ hnr + have hεn : 800 * n ^ 3 * ε ≤ 1 := by + rw [le_div_iff₀ (by positivity)] at hε + linarith + have hqn : 2 * (n : ℝ) ^ 2 / Fintype.card F ≤ 1 / 20 := by + rw [div_le_iff₀ hq0] + nlinarith + have hpow : (1 : ℝ) / 2 ≤ (1 - 1 / (Fintype.card F : ℝ)) ^ n := by + have h1q : 1 / (Fintype.card F : ℝ) ≤ 1 := by + rw [div_le_one hq0] + nlinarith + have hb := one_add_mul_le_pow (a := -(1 / (Fintype.card F : ℝ))) (by linarith) n + have : (n : ℝ) * (1 / (Fintype.card F : ℝ)) ≤ 1 / 2 := by + rw [mul_one_div, div_le_iff₀ hq0] + nlinarith + rw [← sub_eq_add_neg] at hb + nlinarith + have hn2 : (n : ℝ) ≤ n ^ 2 := by nlinarith + have hn3' : (n : ℝ) ^ 2 ≤ n ^ 3 := by nlinarith + obtain ⟨g, hg, hfg⟩ := exists_isMultilinear_hammingDist_le_mul (F := F) (ε₀ := 2 * n * ε) + (γ := 1 / 5) (by positivity) (by nlinarith) n (by nlinarith) f (by + calc (∑ i, (#(wrongPoints f i) : ℝ)) < n * ε * (Fintype.card F : ℝ) ^ n := hsum + _ = 1 / 2 * (2 * n * ε) * (Fintype.card F : ℝ) ^ n := by ring + _ ≤ (1 - 1 / (Fintype.card F : ℝ)) ^ n * (2 * n * ε) * (Fintype.card F : ℝ) ^ n := by + gcongr) + refine ⟨g, hg, ?_⟩ + have h2 : 2 * hammingDist f g ≤ Fintype.card F ^ n := by + have hqpow : 0 ≤ (Fintype.card F : ℝ) ^ n := by positivity + have : ((2 * hammingDist f g : ℕ) : ℝ) ≤ ((Fintype.card F ^ n : ℕ) : ℝ) := by + push_cast + nlinarith + exact_mod_cast this + have hself := hg.hammingDist_le_of_two_mul_le h2 + have hself' : (hammingDist f g : ℝ) ≤ (2 * (n : ℝ) + 1) * (∑ i, (#(wrongPoints f i) : ℝ)) + + 2 * (n : ℝ) ^ 2 * (Fintype.card F : ℝ) ^ (n - 1) := by + exact_mod_cast hself + have hqn1 : (Fintype.card F : ℝ) ^ (n - 1) * Fintype.card F = (Fintype.card F : ℝ) ^ n := by + rw [← pow_succ, Nat.sub_add_cancel hn] + have hqpow : 0 ≤ (Fintype.card F : ℝ) ^ (n - 1) := by positivity + calc (hammingDist f g : ℝ) ≤ _ := hself' + _ < (2 * n + 1) * (n * ε * (Fintype.card F : ℝ) ^ n) + + 2 * (n : ℝ) ^ 2 * (Fintype.card F : ℝ) ^ (n - 1) := by gcongr + _ ≤ 3 * n ^ 2 * ε * (Fintype.card F : ℝ) ^ n + + 2 * (n : ℝ) ^ 2 * (Fintype.card F : ℝ) ^ (n - 1) := by + have : 0 ≤ ε * (Fintype.card F : ℝ) ^ n := by positivity + nlinarith + _ ≤ 3 * n ^ 2 * (ε + 1 / Fintype.card F) * (Fintype.card F : ℝ) ^ n := by + rw [← hqn1] + field_simp + nlinarith + +end Cslib.Code diff --git a/Complexity/Foundations/Data/Hamming/Expansion.lean b/Complexity/Foundations/Data/Hamming/Expansion.lean new file mode 100644 index 0000000000..e854d5476f --- /dev/null +++ b/Complexity/Foundations/Data/Hamming/Expansion.lean @@ -0,0 +1,240 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Cslib.Init +public import Mathlib.Data.Fintype.BigOperators +import Mathlib.Algebra.Order.BigOperators.Group.Finset +import Mathlib.Algebra.BigOperators.Ring.Finset +import Mathlib.Algebra.Group.Action.Defs +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Ring + +/-! +# Expansion of the axis-parallel line closure + +The *line closure* of a set `S` of points of `X ^ n` is the union of the axis-parallel lines +through the points of `S`: the points `y` such that changing one coordinate of `y` lands in `S` +(`Cslib.lineClosure`). This is the closure `S̄ = ⋃ᵢ πᵢ⁻¹(πᵢ(S))` of +[Babai, Fortnow, Lund, Definition 5.7][BabaiFortnowLund1991], where `πᵢ` forgets the `i`-th +coordinate. The closure of a set of at most half of the points is larger than the set by a factor +`1 + 1 / (2 n)` (`Cslib.card_le_two_mul_card_lineClosure_sdiff`, `Cslib.card_lineClosure_ge`), +the Expansion Lemma [Babai, Fortnow, Lund, Lemma 5.8][BabaiFortnowLund1991], which they attribute +to Aldous. + +Our proof is a canonical-path argument, not Aldous's. For `x ∈ S` and `z ∉ S`, the path from `x` to +`z` that replaces the coordinates of `x` by those of `z` in increasing order leaves `S` along some +edge `(u, update u c (z c))` with `u ∈ S`. Swapping the first `c` coordinates of `x` and `z` is a +bijection of pairs that sends this event to the event that changing the `c`-th coordinate of a point +`u ∈ S` to that of an arbitrary point leaves `S`. Counting, `|S| |Sᶜ| ≤ n |X| ^ n |S̄ \ S|`, and +`|Sᶜ| ≥ |X| ^ n / 2` gives `|S| ≤ 2 n |S̄ \ S|`. + +## Main definitions + +* `Cslib.lineClosure`: the union of the axis-parallel lines through the points of a set. + +## Main results + +* `Cslib.card_mul_card_compl_le`: `|S| |Sᶜ| ≤ n |X| ^ n |S̄ \ S|`. +* `Cslib.card_le_two_mul_card_lineClosure_sdiff`, `Cslib.card_lineClosure_ge`: the Expansion + Lemma. + +## References + +* [L. Babai, L. Fortnow, C. Lund, *Non-deterministic exponential time has two-prover interactive + protocols*][BabaiFortnowLund1991], Section 5.2 +-/ + +@[expose] public section + +namespace Cslib + +open Finset Function + +variable {X : Type*} [Fintype X] [DecidableEq X] {n : ℕ} + +/-- The *line closure* of a set `S` of points of `X ^ n`: the points `y` that agree with some point +of `S` in all coordinates but one, that is, the union of the axis-parallel lines through the points +of `S` [Babai, Fortnow, Lund, Definition 5.7][BabaiFortnowLund1991]. -/ +def lineClosure (S : Finset (Fin n → X)) : Finset (Fin n → X) := + {y | ∃ i t, update y i t ∈ S} + +/-- Membership in the line closure. -/ +theorem mem_lineClosure {S : Finset (Fin n → X)} {y : Fin n → X} : + y ∈ lineClosure S ↔ ∃ i t, update y i t ∈ S := by + simp [lineClosure] + +/-- In positive dimension, a set lies in its line closure. -/ +theorem subset_lineClosure {S : Finset (Fin n → X)} (hn : 0 < n) : S ⊆ lineClosure S := + fun y hy => mem_lineClosure.mpr ⟨⟨0, hn⟩, y ⟨0, hn⟩, by simpa using hy⟩ + +/-- The point that takes its first `k` coordinates from `z` and the others from `x`: the `k`-th +point of the canonical path from `x` to `z`. -/ +private def mix (k : ℕ) (x z : Fin n → X) : Fin n → X := + fun j => if (j : ℕ) < k then z j else x j + +omit [Fintype X] [DecidableEq X] in +private theorem mix_zero (x z : Fin n → X) : mix 0 x z = x := by + funext j + simp [mix] + +omit [Fintype X] [DecidableEq X] in +private theorem mix_self (x z : Fin n → X) : mix n x z = z := by + funext j + simp [mix, j.isLt] + +omit [Fintype X] [DecidableEq X] in +private theorem mix_succ (x z : Fin n → X) (c : Fin n) : + mix ((c : ℕ) + 1) x z = update (mix c x z) c (z c) := by + funext j + by_cases hj : j = c + · subst hj + simp [mix] + · have hne : (j : ℕ) ≠ c := fun h => hj (Fin.ext h) + have hiff : (j : ℕ) < c + 1 ↔ (j : ℕ) < c := by omega + rw [update_of_ne hj] + simp only [mix, hiff] + +omit [Fintype X] [DecidableEq X] in +/-- **The canonical path leaves `S`**: from `x ∈ S` to `z ∉ S`, some step of the canonical path +goes from a point of `S` to a point outside `S`. -/ +private theorem exists_mix_mem_update_not_mem {S : Finset (Fin n → X)} {x z : Fin n → X} + (hx : x ∈ S) (hz : z ∉ S) : + ∃ c : Fin n, mix c x z ∈ S ∧ update (mix c x z) c (z c) ∉ S := by + by_contra! h + have hall (k : ℕ) (hk : k ≤ n) : mix k x z ∈ S := by + induction k with + | zero => rwa [mix_zero] + | succ k ih => + have hc := h ⟨k, hk⟩ (ih (by omega)) + rwa [← mix_succ] at hc + exact hz (mix_self x z ▸ hall n le_rfl) + +/-- Swapping the first `c` coordinates of two points. -/ +private def swapPrefix (c : ℕ) (p : (Fin n → X) × (Fin n → X)) : (Fin n → X) × (Fin n → X) := + (mix c p.1 p.2, mix c p.2 p.1) + +omit [Fintype X] [DecidableEq X] in +private theorem swapPrefix_involutive (c : ℕ) : + Involutive (swapPrefix (n := n) (X := X) c) := by + intro p + ext j <;> simp only [swapPrefix, mix] <;> split_ifs <;> rfl + +/-- The number of directed edges in direction `c` from a point of `S` to a point outside `S`. -/ +private theorem card_filter_swap (S : Finset (Fin n → X)) (c : Fin n) : + #{p : (Fin n → X) × (Fin n → X) | mix c p.1 p.2 ∈ S ∧ update (mix c p.1 p.2) c (p.2 c) ∉ S} = + #{p : (Fin n → X) × (Fin n → X) | p.1 ∈ S ∧ update p.1 c (p.2 c) ∉ S} := by + have hc (p : (Fin n → X) × (Fin n → X)) : (swapPrefix c p).2 c = p.2 c := by + simp [swapPrefix, mix] + simp only [card_filter] + refine Fintype.sum_equiv ((swapPrefix_involutive (n := n) (X := X) c).toPerm _) _ _ + fun p => ?_ + simp only [Involutive.coe_toPerm, hc] + rfl + +/-- Changing the `c`-th coordinate of a point of `S` to that of an arbitrary point: the count +is `|X| ^ (n - 1)` times the count of directed edges from `S` to its complement in direction +`c`. -/ +private theorem card_filter_update_apply (S : Finset (Fin n → X)) (c : Fin n) : + #{p : (Fin n → X) × (Fin n → X) | p.1 ∈ S ∧ update p.1 c (p.2 c) ∉ S} = + Fintype.card X ^ (n - 1) * #{q : (Fin n → X) × X | q.1 ∈ S ∧ update q.1 c q.2 ∉ S} := by + have hfib (t : X) : #{w : Fin n → X | w c = t} = Fintype.card X ^ (n - 1) := by + have := Fintype.card_filter_piFinset_const_eq_of_mem (univ : Finset X) c (mem_univ t) + simpa [Fintype.piFinset_univ] using this + simp only [card_filter, Fintype.sum_prod_type] + rw [mul_sum] + refine sum_congr rfl fun u _ => ?_ + have : (∑ w : Fin n → X, if u ∈ S ∧ update u c (w c) ∉ S then (1 : ℕ) else 0) = + ∑ t : X, ∑ w : Fin n → X, if w c = t then (if u ∈ S ∧ update u c t ∉ S then (1 : ℕ) else 0) + else 0 := by + rw [sum_comm] + refine sum_congr rfl fun w _ => ?_ + rw [sum_ite_eq] + simp + rw [this, mul_sum] + refine sum_congr rfl fun t _ => ?_ + rw [← sum_filter, sum_const, smul_eq_mul, hfib, mul_comm] + +/-- Each point outside `S` is the endpoint of at most `|X|` directed edges in direction `c` from +`S`. -/ +private theorem card_edges_le (S : Finset (Fin n → X)) (c : Fin n) : + #{q : (Fin n → X) × X | q.1 ∈ S ∧ update q.1 c q.2 ∉ S} ≤ + Fintype.card X * #(lineClosure S \ S) := by + refine card_le_mul_card_image_of_maps_to (f := fun q => update q.1 c q.2) (fun q hq => ?_) _ + fun y _ => ?_ + · simp only [mem_filter, mem_univ, true_and] at hq + simp only [mem_sdiff, mem_lineClosure] + exact ⟨⟨c, q.1 c, by simpa using hq.1⟩, hq.2⟩ + · rw [← card_univ] + refine card_le_card_of_injOn (fun q => q.1 c) (fun _ _ => mem_univ _) fun q hq q' hq' h => ?_ + simp only [coe_filter, mem_filter, mem_univ, true_and, Set.mem_ofPred_eq] at hq hq' + have h1 : q.1 = q'.1 := by + funext j + by_cases hj : j = c + · subst hj + exact h + · have := congrFun (hq.2.trans hq'.2.symm) j + simpa [update_of_ne hj] using this + have h2 : q.2 = q'.2 := by + have := congrFun (hq.2.trans hq'.2.symm) c + simpa using this + exact Prod.ext h1 h2 + +/-- **Edge counting for the line closure**: `|S| |Sᶜ| ≤ n |X| ^ n |S̄ \ S|`. -/ +theorem card_mul_card_compl_le (S : Finset (Fin n → X)) : + #S * #Sᶜ ≤ n * Fintype.card X ^ n * #(lineClosure S \ S) := by + calc #S * #Sᶜ = #(S ×ˢ Sᶜ) := (card_product _ _).symm + _ ≤ #(univ.biUnion fun c : Fin n => ({p : (Fin n → X) × (Fin n → X) | + mix c p.1 p.2 ∈ S ∧ update (mix c p.1 p.2) c (p.2 c) ∉ S} : + Finset ((Fin n → X) × (Fin n → X)))) := by + refine card_le_card fun p hp => ?_ + simp only [mem_product, mem_compl] at hp + obtain ⟨c, hc⟩ := exists_mix_mem_update_not_mem hp.1 hp.2 + simp only [mem_biUnion, mem_univ, true_and, mem_filter] + exact ⟨c, hc⟩ + _ ≤ ∑ c : Fin n, #({p : (Fin n → X) × (Fin n → X) | + mix c p.1 p.2 ∈ S ∧ update (mix c p.1 p.2) c (p.2 c) ∉ S} : + Finset ((Fin n → X) × (Fin n → X))) := card_biUnion_le + _ = ∑ c : Fin n, Fintype.card X ^ (n - 1) * + #{q : (Fin n → X) × X | q.1 ∈ S ∧ update q.1 c q.2 ∉ S} := by + refine sum_congr rfl fun c _ => ?_ + rw [card_filter_swap, card_filter_update_apply] + _ ≤ ∑ _c : Fin n, Fintype.card X ^ (n - 1) * (Fintype.card X * #(lineClosure S \ S)) := + sum_le_sum fun c _ => Nat.mul_le_mul_left _ (card_edges_le S c) + _ = n * Fintype.card X ^ n * #(lineClosure S \ S) := by + rcases Nat.eq_zero_or_pos n with rfl | hn + · simp + rw [sum_const, card_univ, Fintype.card_fin, smul_eq_mul, ← mul_assoc, ← mul_assoc, + mul_assoc n, ← pow_succ, Nat.sub_add_cancel hn] + +/-- **The Expansion Lemma**: if `S` has at most half of the points of `X ^ n`, then +`|S| ≤ 2 n |S̄ \ S|` [Babai, Fortnow, Lund, Lemma 5.8][BabaiFortnowLund1991]. -/ +theorem card_le_two_mul_card_lineClosure_sdiff {S : Finset (Fin n → X)} + (hS : 2 * #S ≤ Fintype.card X ^ n) : #S ≤ 2 * n * #(lineClosure S \ S) := by + have hcompl : #S + #Sᶜ = Fintype.card X ^ n := by + rw [card_add_card_compl, Fintype.card_pi, prod_const, card_univ, Fintype.card_fin] + have h := card_mul_card_compl_le S + rcases Nat.eq_zero_or_pos (Fintype.card X ^ n) with h0 | hpos + · omega + refine Nat.le_of_mul_le_mul_right ?_ hpos + calc #S * Fintype.card X ^ n ≤ 2 * (#S * #Sᶜ) := by + rw [← hcompl] + nlinarith + _ ≤ 2 * (n * Fintype.card X ^ n * #(lineClosure S \ S)) := Nat.mul_le_mul_left _ h + _ = 2 * n * #(lineClosure S \ S) * Fintype.card X ^ n := by ring + +/-- **The Expansion Lemma** in the form of [Babai, Fortnow, Lund, Lemma 5.8][BabaiFortnowLund1991]: +in positive dimension, if `|S| ≤ |X| ^ n / 2` then `|S̄| ≥ |S| (1 + 1 / (2 n))`. -/ +theorem card_lineClosure_ge {S : Finset (Fin n → X)} (hn : 0 < n) + (hS : 2 * #S ≤ Fintype.card X ^ n) : (2 * n + 1) * #S ≤ 2 * n * #(lineClosure S) := by + have h := card_le_two_mul_card_lineClosure_sdiff hS + have hsplit := card_sdiff_add_card_eq_card (subset_lineClosure (S := S) hn) + rw [← hsplit] + nlinarith + +end Cslib diff --git a/ComplexityTests/Code/MultilinearitySoundness.lean b/ComplexityTests/Code/MultilinearitySoundness.lean new file mode 100644 index 0000000000..f0e2a8bae9 --- /dev/null +++ b/ComplexityTests/Code/MultilinearitySoundness.lean @@ -0,0 +1,83 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Foundations.Data.Code.MultilinearitySoundness +import Mathlib.Data.ZMod.Basic +import Mathlib.FieldTheory.Finite.Basic + +/-! +# Tests: polynomial soundness of the multilinearity test + +Self-improvement applies to the product over `ZMod 5` corrupted at one point: the product is a +multilinear function within one point, and the lemma bounds the distance by +`5 * (5 + 5) + 2 * 2 ^ 2 * 5 = 90`. The hypotheses of the soundness theorem are satisfiable: over +`ZMod 41` (with `41 ≥ 40 * 1 ^ 2`) in one variable, a coordinate function has no wrong lines, and +the theorem applies with `ε = 1 / 800`. +-/ + +namespace ComplexityTests.Code.MultilinearitySoundness + +open Cslib Cslib.Code Finset + +instance : Fact (Nat.Prime 5) := ⟨by decide⟩ +instance : Fact (Nat.Prime 41) := ⟨by decide⟩ + +/-- The product over `ZMod 5`, corrupted at the point `(4, 4)`. -/ +private def corrupted (x : Fin 2 → ZMod 5) : ZMod 5 := + if x = ![4, 4] then 0 else x 0 * x 1 + +/-- The product of the two coordinates. -/ +private def prod2 (x : Fin 2 → ZMod 5) : ZMod 5 := x 0 * x 1 + +private theorem isMultilinear_prod2 : IsMultilinear prod2 := by + intro x i + obtain rfl | rfl : i = 0 ∨ i = 1 := by fin_cases i <;> simp + · have : lineRestrict prod2 x 0 = fun t => t * x 1 := by + funext t + simp [lineRestrict, prod2] + rw [this] + exact isAffineFun_id.mul_const _ + · have : lineRestrict prod2 x 1 = fun t => x 0 * t := by + funext t + simp [lineRestrict, prod2] + rw [this] + exact isAffineFun_id.const_mul _ + +private theorem hammingDist_corrupted : hammingDist corrupted prod2 = 1 := by decide + +private theorem card_wrongPoints_corrupted (i : Fin 2) : #(wrongPoints corrupted i) = 5 := by + fin_cases i <;> decide + +-- Self-improvement for the corrupted product: the hypothesis `2 * 1 ≤ 25` holds, and the bound is +-- `90`. +example : hammingDist corrupted prod2 ≤ 90 := by + have h := isMultilinear_prod2.hammingDist_le_of_two_mul_le (f := corrupted) + (by rw [hammingDist_corrupted]; decide) + simp only [Fin.sum_univ_two, card_wrongPoints_corrupted, ZMod.card] at h + simpa using h + +/-- A coordinate function in one variable over `ZMod 41`. -/ +private def coord (x : Fin 1 → ZMod 41) : ZMod 41 := x 0 + +-- The hypotheses of the soundness theorem hold for it, with `ε = 1 / 800`. +example : ∃ g, IsMultilinear g ∧ (hammingDist coord g : ℝ) < + 3 * 1 ^ 2 * (1 / 800 + 1 / 41) * 41 ^ 1 := by + have hcoord : IsMultilinear coord := by + intro x i + obtain rfl : i = 0 := Subsingleton.elim _ _ + have : lineRestrict coord x 0 = fun t => t := by + funext t + simp [lineRestrict, coord] + rw [this] + exact isAffineFun_id + have hW (i : Fin 1) : wrongPoints coord i = ∅ := by + ext x + simp [wrongPoints, hcoord x i] + have := exists_isMultilinear_hammingDist_lt coord (ε := 1 / 800) (by norm_num) + (by simp [ZMod.card]) (by norm_num) fun i => by simp [hW, ZMod.card] + simpa [ZMod.card] using this + +end ComplexityTests.Code.MultilinearitySoundness diff --git a/ComplexityTests/HammingExpansion.lean b/ComplexityTests/HammingExpansion.lean new file mode 100644 index 0000000000..d115bf4373 --- /dev/null +++ b/ComplexityTests/HammingExpansion.lean @@ -0,0 +1,56 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Foundations.Data.Hamming.Expansion +import Mathlib.Data.Fin.VecNotation +import Mathlib.Data.Fintype.Pi + +/-! +# Tests: expansion of the line closure + +In `Bool ^ 2`, the line closure of one point is the point and its two neighbours, and the line +closure of the line `x 0 = false` is the whole square. In `(Fin 3) ^ 2` the closure of one point +has `1 + 2 * 2 = 5` points, and the Expansion Lemma asks for at least `5 / 4` of a point beyond +the set. The full square shows that the hypothesis `|S| ≤ |X| ^ n / 2` cannot be dropped: it is +its own closure. +-/ + +namespace ComplexityTests.HammingExpansion + +open Cslib Finset + +/-- The origin of `Bool ^ 2`. -/ +private def origin : Finset (Fin 2 → Bool) := {![false, false]} + +-- One point: its closure is the point and its two neighbours. +example : #(lineClosure origin) = 3 := by decide + +/-- The line `x 0 = false` of `Bool ^ 2`. -/ +private def line0 : Finset (Fin 2 → Bool) := {x | x 0 = false} + +-- A line: its closure is the whole square, two points beyond the line. +example : #(lineClosure line0 \ line0) = 2 := by decide + +-- The Expansion Lemma for the line, with `|S| = 2 ≤ 4 / 2`. +example : #line0 ≤ 2 * 2 * #(lineClosure line0 \ line0) := + card_le_two_mul_card_lineClosure_sdiff (by decide) + +/-- The origin of `(Fin 3) ^ 2`. -/ +private def origin3 : Finset (Fin 2 → Fin 3) := {![0, 0]} + +-- Its closure has five points. +example : #(lineClosure origin3) = 5 := by decide + +-- The Expansion Lemma in the form `|S̄| ≥ |S| (1 + 1 / (2 n))`. +example : (2 * 2 + 1) * #origin3 ≤ 2 * 2 * #(lineClosure origin3) := + card_lineClosure_ge (by norm_num) (by decide) + +-- Without the size hypothesis the conclusion fails: the whole square is its own closure. +example : ¬#(univ : Finset (Fin 2 → Bool)) ≤ + 2 * 2 * #(lineClosure (univ : Finset (Fin 2 → Bool)) \ univ) := by + decide + +end ComplexityTests.HammingExpansion