From da700d59ab9cc380f07740dd401e10d94dc182df Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 23:17:17 +0000 Subject: [PATCH 1/7] =?UTF-8?q?feat(Expander):=20uniform=20spectral=20gap?= =?UTF-8?q?=20for=20the=20shear-translation=20graph=20on=20ZMod=20n=20?= =?UTF-8?q?=C3=97=20ZMod=20n=20(#1444)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Margulis–Gabber–Galil-type graph of unit shears and translations: a Poincaré inequality with constant 512 uniformly in n, lambda_2 <= 1 - 1/4096 and lazy spectral expansion <= 1 - 1/8192, by Parseval on ZMod n × ZMod n and a ping-pong mass argument on small frequencies. Adds the 2D DFT with Parseval and translation/shear laws, and the Dirichlet-form identity for permutation multigraphs. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 2 + .../Analysis/Fourier/ZModProd.lean | 149 ++++ .../Combinatorics/Expander/Perm.lean | 63 ++ .../Expander/ShearTranslation.lean | 683 ++++++++++++++++++ ComplexityTests/ShearTranslationExpander.lean | 65 ++ references.bib | 40 + 6 files changed, 1002 insertions(+) create mode 100644 Complexity/Foundations/Analysis/Fourier/ZModProd.lean create mode 100644 Complexity/Foundations/Combinatorics/Expander/ShearTranslation.lean create mode 100644 ComplexityTests/ShearTranslationExpander.lean diff --git a/Complexity.lean b/Complexity.lean index f59b96f22..f0509049d 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2279,6 +2279,7 @@ public import Complexity.Crypto.Protocols.Signature.RandomOracle public import Complexity.Foundations.Algebra.FiniteMagnitude public import Complexity.Foundations.Algebra.GeometricTail public import Complexity.Foundations.Analysis.BernoulliInequality +public import Complexity.Foundations.Analysis.Fourier.ZModProd public import Complexity.Foundations.Analysis.HarmonicMean public import Complexity.Foundations.Analysis.InnerProductSpace.Basic public import Complexity.Foundations.Analysis.LpNorm @@ -2373,6 +2374,7 @@ public import Complexity.Foundations.Combinatorics.Expander.Random public import Complexity.Foundations.Combinatorics.Expander.Reindex public import Complexity.Foundations.Combinatorics.Expander.Reingold public import Complexity.Foundations.Combinatorics.Expander.Replacement +public import Complexity.Foundations.Combinatorics.Expander.ShearTranslation public import Complexity.Foundations.Combinatorics.Expander.SimpleGraph public import Complexity.Foundations.Combinatorics.Expander.SlotGraph public import Complexity.Foundations.Combinatorics.Expander.Spectrum diff --git a/Complexity/Foundations/Analysis/Fourier/ZModProd.lean b/Complexity/Foundations/Analysis/Fourier/ZModProd.lean new file mode 100644 index 000000000..03ce150f2 --- /dev/null +++ b/Complexity/Foundations/Analysis/Fourier/ZModProd.lean @@ -0,0 +1,149 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar +import Mathlib.Analysis.Complex.Basic +import Mathlib.NumberTheory.LegendreSymbol.AddCharacter + +/-! +# The discrete Fourier transform on `ZMod N × ZMod N` + +The Fourier transform of `f : ZMod N × ZMod N → ℂ` at the frequency `ξ` is +`∑ v, e (-(ξ.1 * v.1 + ξ.2 * v.2)) * f v`, where `e = ZMod.stdAddChar` sends `j` to +`exp (2 π i j / N)`. This is Mathlib's `ZMod.dft` in each coordinate, written for the two +coordinates together. The characters `v ↦ e (ξ.1 * v.1 + ξ.2 * v.2)` are orthogonal, so the +transform preserves the `ℓ²` norm up to the factor `N ^ 2` (Parseval's identity). + +Translations and shears of the plane act on the transform by simple rules: a translation by `t` +multiplies the transform at `ξ` by `e (ξ.1 * t.1 + ξ.2 * t.2)`, and the shear +`(x, y) ↦ (x + k * y, y)` acts on the frequencies by the transposed inverse shear +`(a, b) ↦ (a, b - k * a)`, and symmetrically for `(x, y) ↦ (x, y + k * x)`. + +## Main definitions + +* `ZMod.dftProd`: the discrete Fourier transform on `ZMod N × ZMod N`. + +## Main results + +* `ZMod.sum_norm_sq_dftProd`: Parseval's identity + `∑ ξ, ‖dftProd f ξ‖ ^ 2 = N ^ 2 * ∑ v, ‖f v‖ ^ 2`. +* `ZMod.dftProd_zero`: the transform at the zero frequency is the sum of the values. +* `ZMod.dftProd_comp_add`: translation multiplies the transform by a character value. +* `ZMod.dftProd_comp_shearFst`, `ZMod.dftProd_comp_shearSnd`: shears permute the frequencies. +-/ + +public section + +namespace ZMod + +open Finset ComplexConjugate + +variable {N : ℕ} [NeZero N] + +/-- The discrete Fourier transform of `f : ZMod N × ZMod N → ℂ` at the frequency `ξ`: +`∑ v, e (-(ξ.1 * v.1 + ξ.2 * v.2)) * f v` with `e = ZMod.stdAddChar`. -/ +noncomputable def dftProd (f : ZMod N × ZMod N → ℂ) (ξ : ZMod N × ZMod N) : ℂ := + ∑ v, stdAddChar (-(ξ.1 * v.1 + ξ.2 * v.2)) * f v + +/-- The transform at the zero frequency is the sum of the values. -/ +@[simp] +theorem dftProd_zero (f : ZMod N × ZMod N → ℂ) : dftProd f 0 = ∑ v, f v := by + simp [dftProd] + +/-- The transform is additive. -/ +theorem dftProd_sub (f g : ZMod N × ZMod N → ℂ) : + dftProd (f - g) = dftProd f - dftProd g := by + ext ξ + simp only [dftProd, Pi.sub_apply, mul_sub, sum_sub_distrib] + +/-- **Orthogonality of the characters of `ZMod N × ZMod N`**: summed over all frequencies, a +nontrivial character value vanishes. -/ +private theorem sum_stdAddChar_mul_add (u : ZMod N × ZMod N) : + ∑ ξ : ZMod N × ZMod N, stdAddChar (ξ.1 * u.1 + ξ.2 * u.2) = + if u = 0 then (N : ℂ) ^ 2 else 0 := by + simp only [AddChar.map_add_eq_mul, Fintype.sum_prod_type, ← mul_sum, ← sum_mul, + AddChar.sum_mulShift _ (isPrimitive_stdAddChar N), ZMod.card] + rcases u with ⟨u₁, u₂⟩ + by_cases h₁ : u₁ = 0 <;> by_cases h₂ : u₂ = 0 <;> simp [h₁, h₂, sq] + +/-- **Parseval's identity** on `ZMod N × ZMod N`. -/ +theorem sum_norm_sq_dftProd (f : ZMod N × ZMod N → ℂ) : + ∑ ξ, ‖dftProd f ξ‖ ^ 2 = N ^ 2 * ∑ v, ‖f v‖ ^ 2 := by + apply Complex.ofReal_injective + push_cast + simp only [← Complex.mul_conj', dftProd, map_sum, map_mul, ← AddChar.map_neg_eq_conj, neg_neg, + sum_mul_sum] + calc ∑ ξ : ZMod N × ZMod N, ∑ v, ∑ w, + stdAddChar (-(ξ.1 * v.1 + ξ.2 * v.2)) * f v * (stdAddChar (ξ.1 * w.1 + ξ.2 * w.2) * + conj (f w)) + = ∑ v, ∑ w, f v * conj (f w) * + ∑ ξ : ZMod N × ZMod N, stdAddChar (ξ.1 * (w - v).1 + ξ.2 * (w - v).2) := by + rw [sum_comm] + refine sum_congr rfl fun v _ ↦ ?_ + rw [sum_comm] + refine sum_congr rfl fun w _ ↦ ?_ + rw [mul_sum] + refine sum_congr rfl fun ξ _ ↦ ?_ + have : stdAddChar (ξ.1 * (w - v).1 + ξ.2 * (w - v).2) = + stdAddChar (-(ξ.1 * v.1 + ξ.2 * v.2)) * stdAddChar (ξ.1 * w.1 + ξ.2 * w.2) := by + rw [← AddChar.map_add_eq_mul] + congr 1 + simp only [Prod.fst_sub, Prod.snd_sub] + ring + rw [this] + ring + _ = (N : ℂ) ^ 2 * ∑ v, f v * conj (f v) := by + simp only [sum_stdAddChar_mul_add, sub_eq_zero, mul_ite, mul_zero, sum_ite_eq', + mem_univ, ite_true, mul_sum] + exact sum_congr rfl fun v _ ↦ by ring + +/-- **Translation** multiplies the transform at `ξ` by `e (ξ.1 * t.1 + ξ.2 * t.2)`. -/ +theorem dftProd_comp_add (f : ZMod N × ZMod N → ℂ) (t ξ : ZMod N × ZMod N) : + dftProd (fun v ↦ f (v + t)) ξ = stdAddChar (ξ.1 * t.1 + ξ.2 * t.2) * dftProd f ξ := by + rw [dftProd, dftProd, mul_sum] + refine Fintype.sum_equiv (Equiv.addRight t) _ _ fun v ↦ ?_ + simp only [Equiv.coe_addRight, Prod.fst_add, Prod.snd_add, ← mul_assoc, + ← AddChar.map_add_eq_mul] + congr 2 + ring + +/-- The shear `(x, y) ↦ (x + k * y, y)` of `ZMod N × ZMod N`, as a permutation. -/ +private def shearFstEquiv (k : ZMod N) : Equiv.Perm (ZMod N × ZMod N) where + toFun v := (v.1 + k * v.2, v.2) + invFun v := (v.1 - k * v.2, v.2) + left_inv v := by simp + right_inv v := by simp + +/-- **The shear `(x, y) ↦ (x + k * y, y)`** acts on frequencies by `(a, b) ↦ (a, b - k * a)`. -/ +theorem dftProd_comp_shearFst (f : ZMod N × ZMod N → ℂ) (k : ZMod N) (ξ : ZMod N × ZMod N) : + dftProd (fun v ↦ f (v.1 + k * v.2, v.2)) ξ = dftProd f (ξ.1, ξ.2 - k * ξ.1) := by + rw [dftProd, dftProd] + refine Fintype.sum_equiv (shearFstEquiv k) _ _ fun v ↦ ?_ + simp only [shearFstEquiv, Equiv.coe_fn_mk] + congr 2 + ring + +/-- The shear `(x, y) ↦ (x, y + k * x)` of `ZMod N × ZMod N`, as a permutation. -/ +private def shearSndEquiv (k : ZMod N) : Equiv.Perm (ZMod N × ZMod N) where + toFun v := (v.1, v.2 + k * v.1) + invFun v := (v.1, v.2 - k * v.1) + left_inv v := by simp + right_inv v := by simp + +/-- **The shear `(x, y) ↦ (x, y + k * x)`** acts on frequencies by `(a, b) ↦ (a - k * b, b)`. -/ +theorem dftProd_comp_shearSnd (f : ZMod N × ZMod N → ℂ) (k : ZMod N) (ξ : ZMod N × ZMod N) : + dftProd (fun v ↦ f (v.1, v.2 + k * v.1)) ξ = dftProd f (ξ.1 - k * ξ.2, ξ.2) := by + rw [dftProd, dftProd] + refine Fintype.sum_equiv (shearSndEquiv k) _ _ fun v ↦ ?_ + simp only [shearSndEquiv, Equiv.coe_fn_mk] + congr 2 + ring + +end ZMod diff --git a/Complexity/Foundations/Combinatorics/Expander/Perm.lean b/Complexity/Foundations/Combinatorics/Expander/Perm.lean index 71d6d7202..9ef0e54fa 100644 --- a/Complexity/Foundations/Combinatorics/Expander/Perm.lean +++ b/Complexity/Foundations/Combinatorics/Expander/Perm.lean @@ -41,6 +41,10 @@ are expanders [Hoory, Linial and Wigderson, Theorem 4.16][HooryLinialWigderson20 permutations move out of it, twice. * `Cslib.RotationMap.le_edgeExpansion_ofPerms`: a lower bound on these counts for every set of at most half of the vertices bounds the edge expansion. +* `Cslib.RotationMap.expect_mul_walk_ofPerms`: the Dirichlet form of the walk is the total squared + change of a function along the permutations. +* `Cslib.RotationMap.secondEigenvalue_ofPerms_le`: a Poincaré inequality for the permutations + bounds the second eigenvalue. ## References @@ -133,4 +137,63 @@ theorem le_edgeExpansion_ofPerms [Nontrivial V] {c : ℝ} push_cast at this ⊢ linarith +omit [DecidableEq V] in +/-- **The Dirichlet form of a permutation multigraph**: the correlation of `f` with its walk is +`𝔼 f²` minus `1 / (2 |K|)` times the total squared change `∑ k, 𝔼 v, (f (σ k v) - f v) ^ 2` of `f` +along the permutations. -/ +theorem expect_mul_walk_ofPerms [Nonempty K] (f : V → ℝ) : + 𝔼 v, f v * (ofPerms σ).walk f v = + (𝔼 v, f v ^ 2) - (∑ k, 𝔼 v, (f (σ k v) - f v) ^ 2) / (2 * Fintype.card K) := by + have hK : (0 : ℝ) < Fintype.card K := Nat.cast_pos.2 Fintype.card_pos + have hwalk (v : V) : (ofPerms σ).walk f v = + (∑ k, (f (σ k v) + f ((σ k).symm v))) / (2 * Fintype.card K) := by + rw [walk_apply, Fintype.expect_eq_sum_div_card, Fintype.sum_prod_type, Fintype.card_prod, + Fintype.card_bool] + simp only [Fintype.sum_bool, neighbor_ofPerms_true, neighbor_ofPerms_false, + add_comm (f ((σ _).symm v))] + push_cast + ring + have hsymm (k : K) : ∑ v, f v * f ((σ k).symm v) = ∑ v, f v * f (σ k v) := by + rw [← Equiv.sum_comp (σ k)] + simp [mul_comm] + have hcross (k : K) : ∑ v, (f (σ k v) - f v) ^ 2 = + 2 * ∑ v, f v ^ 2 - 2 * ∑ v, f v * f (σ k v) := by + simp only [sub_sq, sum_add_distrib, sum_sub_distrib, Equiv.sum_comp (σ k) (fun v ↦ f v ^ 2), + mul_sum] + ring_nf + simp only [← sum_mul, mul_comm (f _) (f _)] + calc 𝔼 v, f v * (ofPerms σ).walk f v + = (∑ v, f v * ∑ k, (f (σ k v) + f ((σ k).symm v))) / (2 * Fintype.card K) / + Fintype.card V := by + simp only [hwalk, Fintype.expect_eq_sum_div_card, ← mul_div_assoc, ← sum_div] + _ = (2 * ∑ k, ∑ v, f v * f (σ k v)) / (2 * Fintype.card K) / Fintype.card V := by + congr 2 + simp only [mul_sum, mul_add, sum_add_distrib] + rw [sum_comm, sum_comm (f := fun v k ↦ f v * f ((σ k).symm v))] + simp only [hsymm, ← two_mul, mul_sum] + _ = _ := by + simp only [Fintype.expect_eq_sum_div_card, ← sum_div, hcross, sum_sub_distrib, sum_const, + card_univ, nsmul_eq_mul, ← mul_sum] + field_simp + ring + +omit [DecidableEq V] in +/-- **A Poincaré inequality bounds the second eigenvalue** of a permutation multigraph on at least +two vertices: if `c 𝔼 f² ≤ ∑ k, 𝔼 v, (f (σ k v) - f v) ^ 2` for every `f` of expectation zero, then +`λ₂ ≤ 1 - c / (2 |K|)`. -/ +theorem secondEigenvalue_ofPerms_le [Nonempty K] [Nontrivial V] {c : ℝ} + (h : ∀ f : V → ℝ, 𝔼 v, f v = 0 → c * (𝔼 v, f v ^ 2) ≤ ∑ k, 𝔼 v, (f (σ k v) - f v) ^ 2) : + (ofPerms σ).secondEigenvalue ≤ 1 - c / (2 * Fintype.card K) := by + refine (ofPerms σ).secondEigenvalue_le_iff.2 fun f hf ↦ ?_ + have hK : (0 : ℝ) < 2 * Fintype.card K := by + have := Fintype.card_pos (α := K) + positivity + calc 𝔼 v, f v * (ofPerms σ).walk f v + = (𝔼 v, f v ^ 2) - (∑ k, 𝔼 v, (f (σ k v) - f v) ^ 2) / (2 * Fintype.card K) := + expect_mul_walk_ofPerms σ f + _ ≤ (𝔼 v, f v ^ 2) - c * (𝔼 v, f v ^ 2) / (2 * Fintype.card K) := by + have := div_le_div_of_nonneg_right (h f hf) hK.le + linarith + _ = (1 - c / (2 * Fintype.card K)) * 𝔼 v, f v ^ 2 := by ring + end Cslib.RotationMap diff --git a/Complexity/Foundations/Combinatorics/Expander/ShearTranslation.lean b/Complexity/Foundations/Combinatorics/Expander/ShearTranslation.lean new file mode 100644 index 000000000..c23b98d39 --- /dev/null +++ b/Complexity/Foundations/Combinatorics/Expander/ShearTranslation.lean @@ -0,0 +1,683 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Combinatorics.Expander.Lazy +public import Complexity.Foundations.Combinatorics.Expander.Perm +public import Mathlib.Data.ZMod.Basic +import Complexity.Foundations.Analysis.Fourier.ZModProd +import Mathlib.Algebra.Order.Chebyshev +import Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds +import Mathlib.Data.ZMod.ValMinAbs + +/-! +# The shear-translation expander on `ZMod n × ZMod n` + +The four moves `(x, y) ↦ (x + y, y)`, `(x, y) ↦ (x, y + x)`, `(x, y) ↦ (x + 1, y)` and +`(x, y) ↦ (x, y + 1)` of `ZMod n × ZMod n` and their inverses form an `8`-regular multigraph +(`shearTranslation n`). It is an expander uniformly in `n`: its second eigenvalue is at most +`1 - 1 / 4096`, and its lazy version has spectral expansion at most `1 - 1 / 8192`, for every +`n ≥ 1`. It is a variant of the graphs of Margulis [Margulis][Margulis1973] and of Gabber and +Galil [Gabber and Galil][GabberGalil1981], whose expansion the chapter on the Margulis construction +[Hoory, Linial and Wigderson, Section 8][HooryLinialWigderson2006] proves by Fourier analysis +on `ZMod n × ZMod n`, following Jimbo and Maruoka [Jimbo and Maruoka][JimboMaruoka1987]. Here +the translations are separate moves rather than combined with the shears. + +The proof is elementary Fourier analysis, organised differently from the cited one. Write `F` for +the discrete Fourier transform of a function `f` of sum zero (`ZMod.dftProd`), so `F 0 = 0`. By +Parseval's identity, the squared changes of `f` along the moves are the corresponding quantities +for `F`: a translation multiplies `F ξ` by a root of unity, which is far from `1` unless `ξ` is a +small frequency, and a shear permutes the frequencies by a shear. So if `f` changes little along +the moves, the mass `‖F ξ‖ ^ 2` lies mostly on small frequencies and is almost invariant under the +dual shears. On the small frequencies, whose centered representatives are at most `n / 11` in +absolute value, the dual shears by `±4` act as integer shears, and they play ping-pong: they move +the frequencies `(a, b)` with `|b| < |a|` to two disjoint sets of frequencies with `|a| < |b|`, +and those with `0 < |b|`, `|a| ≤ |b|` to two disjoint sets with `|b| < |a|`. Each class therefore +carries at least twice the mass of the other, up to small errors, so both are nearly empty. This +is a finite, quantitative argument in the spirit of the proof of the relative property (T) of +`SL₂(ℤ) ⋉ ℤ²` [Burger][Burger1991]. + +The explicit constants are far from optimal; the point is that they do not depend on `n`. + +## Main definitions + +* `Cslib.shearFst`, `Cslib.shearSnd`: the shears `(x, y) ↦ (x + k * y, y)` and + `(x, y) ↦ (x, y + k * x)` of `R × R`. +* `Cslib.RotationMap.shearTranslationMove`: the four moves of the graph. +* `Cslib.RotationMap.shearTranslation`: the `8`-regular shear-translation multigraph on + `ZMod n × ZMod n`. + +## Main results + +* `Cslib.RotationMap.sum_norm_sq_le_shearTranslation`: the Poincaré inequality + `∑ v, ‖f v‖ ^ 2 ≤ 512 * ∑ k, ∑ v, ‖f (shearTranslationMove n k v) - f v‖ ^ 2` for every + complex function of sum zero. +* `Cslib.RotationMap.secondEigenvalue_shearTranslation_le`: `λ₂ ≤ 1 - 1 / 4096`. +* `Cslib.RotationMap.spectralExpansion_lazy_shearTranslation_le`: the lazy graph has spectral + expansion at most `1 - 1 / 8192`. + +## References + +* [G. A. Margulis, *Explicit constructions of expanders*][Margulis1973] +* [O. Gabber, Z. Galil, *Explicit constructions of linear-sized + superconcentrators*][GabberGalil1981] +* [S. Jimbo, A. Maruoka, *Expanders obtained from affine transformations*][JimboMaruoka1987] +* [M. Burger, *Kazhdan constants for SL(3, ℤ)*][Burger1991] +* [S. Hoory, N. Linial, A. Wigderson, *Expander graphs and their + applications*][HooryLinialWigderson2006] +-/ + +@[expose] public section + +namespace Cslib + +open Finset + +section Shear + +variable {R : Type*} [CommRing R] + +/-- The shear `(x, y) ↦ (x + k * y, y)` of `R × R`, as a permutation. -/ +def shearFst (k : R) : Equiv.Perm (R × R) where + toFun v := (v.1 + k * v.2, v.2) + invFun v := (v.1 - k * v.2, v.2) + left_inv v := by simp + right_inv v := by simp + +/-- The shear `(x, y) ↦ (x, y + k * x)` of `R × R`, as a permutation. -/ +def shearSnd (k : R) : Equiv.Perm (R × R) where + toFun v := (v.1, v.2 + k * v.1) + invFun v := (v.1, v.2 - k * v.1) + left_inv v := by simp + right_inv v := by simp + +@[simp] +theorem shearFst_apply (k : R) (v : R × R) : shearFst k v = (v.1 + k * v.2, v.2) := + rfl + +@[simp] +theorem shearSnd_apply (k : R) (v : R × R) : shearSnd k v = (v.1, v.2 + k * v.1) := + rfl + +/-- The inverse of a shear is the opposite shear. -/ +theorem shearFst_symm (k : R) : (shearFst k).symm = shearFst (-k) := by + ext v <;> simp [shearFst, sub_eq_add_neg] + +/-- The inverse of a shear is the opposite shear. -/ +theorem shearSnd_symm (k : R) : (shearSnd k).symm = shearSnd (-k) := by + ext v <;> simp [shearSnd, sub_eq_add_neg] + +/-- Iterating a shear multiplies its parameter. -/ +theorem shearFst_pow (k : R) (m : ℕ) : shearFst k ^ m = shearFst (m * k) := by + induction m with + | zero => ext v <;> simp + | succ m ih => + rw [pow_succ', ih] + ext v + · simp only [Equiv.Perm.mul_apply, shearFst_apply] + push_cast + ring + · rfl + +/-- Iterating a shear multiplies its parameter. -/ +theorem shearSnd_pow (k : R) (m : ℕ) : shearSnd k ^ m = shearSnd (m * k) := by + induction m with + | zero => ext v <;> simp + | succ m ih => + rw [pow_succ', ih] + ext v + · rfl + · simp only [Equiv.Perm.mul_apply, shearSnd_apply] + push_cast + ring + +end Shear + +namespace RotationMap + +/-- The four moves of the shear-translation graph on `ZMod n × ZMod n`: the shears +`(x, y) ↦ (x + y, y)` and `(x, y) ↦ (x, y + x)` and the translations by `(1, 0)` and `(0, 1)`. -/ +def shearTranslationMove (n : ℕ) : Fin 4 → Equiv.Perm (ZMod n × ZMod n) := + ![shearFst 1, shearSnd 1, Equiv.addRight (1, 0), Equiv.addRight (0, 1)] + +/-- The **shear-translation graph** on `ZMod n × ZMod n`: the `8`-regular multigraph of the two +unit shears and the two unit translations, a variant of the Margulis–Gabber–Galil graphs +[Hoory, Linial and Wigderson, Section 8][HooryLinialWigderson2006]. -/ +def shearTranslation (n : ℕ) : RotationMap (ZMod n × ZMod n) (Fin 4 × Bool) := + ofPerms (shearTranslationMove n) + +/-! ### Squared changes along permutations -/ + +section Energy + +variable {α : Type*} [Fintype α] + +/-- The squared change of `f` along `σ ^ m` is at most `m ^ 2` times that along `σ`. -/ +private theorem sum_norm_sub_sq_pow_le (f : α → ℂ) (σ : Equiv.Perm α) (m : ℕ) : + ∑ v, ‖f ((σ ^ m) v) - f v‖ ^ 2 ≤ m ^ 2 * ∑ v, ‖f (σ v) - f v‖ ^ 2 := by + have htel (v : α) : f ((σ ^ m) v) - f v = + ∑ j ∈ range m, (f (σ ((σ ^ j) v)) - f ((σ ^ j) v)) := by + have := Finset.sum_range_sub (fun j ↦ f ((σ ^ j) v)) m + simp only [pow_succ', Equiv.Perm.mul_apply, pow_zero, Equiv.Perm.one_apply] at this + exact this.symm + calc ∑ v, ‖f ((σ ^ m) v) - f v‖ ^ 2 + ≤ ∑ v, m * ∑ j ∈ range m, ‖f (σ ((σ ^ j) v)) - f ((σ ^ j) v)‖ ^ 2 := by + refine sum_le_sum fun v _ ↦ ?_ + rw [htel] + calc ‖∑ j ∈ range m, (f (σ ((σ ^ j) v)) - f ((σ ^ j) v))‖ ^ 2 + ≤ (∑ j ∈ range m, ‖f (σ ((σ ^ j) v)) - f ((σ ^ j) v)‖) ^ 2 := by + gcongr + exact norm_sum_le _ _ + _ ≤ _ := by + simpa using sq_sum_le_card_mul_sum_sq (s := range m) + (f := fun j ↦ ‖f (σ ((σ ^ j) v)) - f ((σ ^ j) v)‖) + _ = m * ∑ j ∈ range m, ∑ v, ‖f (σ ((σ ^ j) v)) - f ((σ ^ j) v)‖ ^ 2 := by + rw [← mul_sum, sum_comm] + _ = m * ∑ _j ∈ range m, ∑ v, ‖f (σ v) - f v‖ ^ 2 := by + congr 1 + exact sum_congr rfl fun j _ ↦ + Equiv.sum_comp (σ ^ j) (fun v ↦ ‖f (σ v) - f v‖ ^ 2) + _ = _ := by + rw [sum_const, card_range, nsmul_eq_mul] + ring + +/-- The squared change of `f` along `σ⁻¹` equals that along `σ`. -/ +private theorem sum_norm_sub_sq_symm (f : α → ℂ) (σ : Equiv.Perm α) : + ∑ v, ‖f (σ.symm v) - f v‖ ^ 2 = ∑ v, ‖f (σ v) - f v‖ ^ 2 := by + rw [← Equiv.sum_comp σ] + simp [norm_sub_rev] + +/-- **Mass transfer**: moving a set of points by a permutation `g` changes the mass `‖F z‖ ^ 2` +on it by at most `8` times the squared change of `F` along `g` plus `1 / 8` of the total mass. -/ +private theorem sum_norm_sq_le_sum_comp (F : α → ℂ) (g : Equiv.Perm α) (E : Finset α) : + ∑ z ∈ E, ‖F z‖ ^ 2 ≤ + ∑ z ∈ E, ‖F (g z)‖ ^ 2 + 8 * ∑ z, ‖F (g z) - F z‖ ^ 2 + (∑ z, ‖F z‖ ^ 2) / 8 := by + have hpt (x y : ℂ) : ‖x‖ ^ 2 ≤ ‖y‖ ^ 2 + 8 * ‖y - x‖ ^ 2 + (‖x‖ ^ 2 + ‖y‖ ^ 2) / 16 := by + have h : ‖x‖ - ‖y‖ ≤ ‖y - x‖ := by + rw [norm_sub_rev] + exact norm_sub_norm_le x y + nlinarith [mul_le_mul_of_nonneg_right h (add_nonneg (norm_nonneg x) (norm_nonneg y)), + sq_nonneg (‖x‖ + ‖y‖ - 16 * ‖y - x‖), sq_nonneg (‖x‖ - ‖y‖)] + have hE (u : α → ℝ) (hu : ∀ z, 0 ≤ u z) : ∑ z ∈ E, u z ≤ ∑ z, u z := + sum_le_univ_sum_of_nonneg hu + have hg : ∑ z, ‖F (g z)‖ ^ 2 = ∑ z, ‖F z‖ ^ 2 := Equiv.sum_comp g fun z ↦ ‖F z‖ ^ 2 + calc ∑ z ∈ E, ‖F z‖ ^ 2 + ≤ ∑ z ∈ E, (‖F (g z)‖ ^ 2 + 8 * ‖F (g z) - F z‖ ^ 2 + + (‖F z‖ ^ 2 + ‖F (g z)‖ ^ 2) / 16) := sum_le_sum fun z _ ↦ hpt _ _ + _ = ∑ z ∈ E, ‖F (g z)‖ ^ 2 + 8 * ∑ z ∈ E, ‖F (g z) - F z‖ ^ 2 + + (∑ z ∈ E, ‖F z‖ ^ 2 + ∑ z ∈ E, ‖F (g z)‖ ^ 2) / 16 := by + rw [sum_add_distrib, sum_add_distrib, ← mul_sum, ← sum_div, sum_add_distrib] + _ ≤ _ := by + have h₁ := hE (fun z ↦ ‖F (g z) - F z‖ ^ 2) fun _ ↦ by positivity + have h₂ := hE (fun z ↦ ‖F z‖ ^ 2) fun _ ↦ by positivity + have h₃ := hE (fun z ↦ ‖F (g z)‖ ^ 2) fun _ ↦ by positivity + linarith + +omit [Fintype α] in +/-- **Two disjoint images**: if `g₁` and `g₂` map `E` into `T` with disjoint images, the mass of +`T` is at least the masses of the two images together. -/ +private theorem sum_comp_add_sum_comp_le (F : α → ℂ) (g₁ g₂ : Equiv.Perm α) + (E T : Finset α) (h₁ : ∀ z ∈ E, g₁ z ∈ T) (h₂ : ∀ z ∈ E, g₂ z ∈ T) + (hd : ∀ z ∈ E, ∀ w ∈ E, g₁ z ≠ g₂ w) : + ∑ z ∈ E, ‖F (g₁ z)‖ ^ 2 + ∑ z ∈ E, ‖F (g₂ z)‖ ^ 2 ≤ ∑ z ∈ T, ‖F z‖ ^ 2 := by + classical + have hmap (g : Equiv.Perm α) : ∑ z ∈ E, ‖F (g z)‖ ^ 2 = + ∑ z ∈ E.map g.toEmbedding, ‖F z‖ ^ 2 := by + rw [sum_map] + rfl + rw [hmap, hmap, ← sum_union] + · refine sum_le_sum_of_subset_of_nonneg (fun w hw ↦ ?_) fun _ _ _ ↦ by positivity + rcases mem_union.1 hw with hw | hw <;> obtain ⟨z, hz, rfl⟩ := mem_map.1 hw + exacts [h₁ z hz, h₂ z hz] + · refine disjoint_left.2 fun w hw₁ hw₂ ↦ ?_ + obtain ⟨z, hz, rfl⟩ := mem_map.1 hw₁ + obtain ⟨z', hz', hzz'⟩ := mem_map.1 hw₂ + exact hd z hz z' hz' hzz'.symm + +end Energy + +/-! ### Small frequencies -/ + +section Frequencies + +variable {n : ℕ} [NeZero n] + +/-- On small frequencies, a shear by at most `4` acts on the centered representatives as the +integer shear. -/ +private theorem valMinAbs_add_mul {a b : ZMod n} {k : ℤ} (hk : |k| ≤ 4) + (ha : 11 * |a.valMinAbs| ≤ n) (hb : 11 * |b.valMinAbs| ≤ n) : + (a + k * b).valMinAbs = a.valMinAbs + k * b.valMinAbs := by + rw [ZMod.valMinAbs_spec] + refine ⟨by push_cast [ZMod.coe_valMinAbs]; rfl, ?_⟩ + have hn : (0 : ℤ) < n := by exact_mod_cast Nat.pos_of_ne_zero (NeZero.ne n) + have h₁ : |a.valMinAbs + k * b.valMinAbs| ≤ |a.valMinAbs| + |k| * |b.valMinAbs| := + (abs_add_le _ _).trans_eq (by rw [abs_mul]) + have h₂ : |k| * |b.valMinAbs| ≤ 4 * |b.valMinAbs| := + mul_le_mul_of_nonneg_right hk (abs_nonneg _) + have h₃ := neg_abs_le (a.valMinAbs + k * b.valMinAbs) + have h₄ := le_abs_self (a.valMinAbs + k * b.valMinAbs) + constructor <;> linarith + +/-- The ping-pong inequality: a shear by `±4` moves a frequency `(p, q)` with `|p| ≤ |q|` and +`q ≠ 0` to one whose first coordinate is larger than the second. -/ +private theorem abs_lt_abs_add_mul {p q k : ℤ} (hk : |k| = 4) (hpq : |p| ≤ |q|) (hq : q ≠ 0) : + |q| < |p + k * q| := by + have h : |k * q| ≤ |p + k * q| + |p| := by + have := abs_sub (p + k * q) p + rwa [add_sub_cancel_left] at this + rw [abs_mul, hk] at h + have := abs_pos.2 hq + linarith + +/-- The images of a frequency `(p, q)` with `|p| ≤ |q|` under the shears by `4` and `-4` differ. -/ +private theorem add_four_mul_ne {p p' q : ℤ} (hp : |p| ≤ |q|) (hp' : |p'| ≤ |q|) (hq : q ≠ 0) : + p + 4 * q ≠ p' + -4 * q := by + intro h + have h' : p' - p = 8 * q := by linarith + have h₁ : |p' - p| ≤ |p'| + |p| := abs_sub _ _ + rw [h', abs_mul, show |(8 : ℤ)| = 8 by norm_num] at h₁ + have := abs_pos.2 hq + linarith + +/-- A frequency outside the small box is moved far by one of the unit translations: the +corresponding root of unity is at distance at least `1 / sqrt 8` from `1`. -/ +private theorem one_div_eight_le_norm_stdAddChar_sub_one {a : ZMod n} + (ha : (n : ℤ) < 11 * |a.valMinAbs|) : 1 / 8 ≤ ‖ZMod.stdAddChar a - 1‖ ^ 2 := by + set A := a.valMinAbs with hA + have hn : (0 : ℝ) < n := by exact_mod_cast Nat.pos_of_ne_zero (NeZero.ne n) + have hhalf : 2 * |(A : ℝ)| ≤ n := by + have h := ZMod.natAbs_valMinAbs_le a + have : 2 * A.natAbs ≤ n := by omega + rw [← Int.cast_abs, ← Int.natCast_natAbs] + exact_mod_cast this + have hbig : (n : ℝ) < 11 * |(A : ℝ)| := by + rw [← Int.cast_abs] + exact_mod_cast ha + have hexp : ZMod.stdAddChar a = Complex.exp (Complex.I * ((2 * Real.pi * A / n : ℝ) : ℂ)) := by + conv_lhs => rw [← ZMod.coe_valMinAbs a, ← hA, ZMod.stdAddChar_coe] + congr 1 + push_cast + ring + rw [hexp, Complex.norm_exp_I_mul_ofReal_sub_one, norm_mul, Real.norm_eq_abs, + Real.norm_eq_abs, abs_two] + have hsin : 2 / 11 ≤ |Real.sin (2 * Real.pi * A / n / 2)| := by + have hx : 2 * Real.pi * A / n / 2 = Real.pi * A / n := by ring + have hxabs : |Real.sin (Real.pi * A / n)| = Real.sin (Real.pi * |(A : ℝ)| / n) := by + have hle : Real.pi * |(A : ℝ)| / n ≤ Real.pi := by + rw [div_le_iff₀ hn] + nlinarith [Real.pi_pos, abs_nonneg (A : ℝ)] + have hs := Real.sin_nonneg_of_nonneg_of_le_pi (by positivity) hle + rcases le_or_gt 0 (A : ℝ) with h | h + · rw [abs_of_nonneg h] at hs ⊢ + exact abs_of_nonneg hs + · have e : Real.sin (Real.pi * -(A : ℝ) / n) = -Real.sin (Real.pi * A / n) := by + rw [mul_neg, neg_div, Real.sin_neg] + rw [abs_of_neg h, e] at hs ⊢ + exact abs_of_nonpos (by linarith) + rw [hx, hxabs] + have hle : Real.pi * |(A : ℝ)| / n ≤ Real.pi / 2 := by + rw [div_le_iff₀ hn] + nlinarith [Real.pi_pos] + have := Real.mul_le_sin (by positivity) hle + have heq : 2 / Real.pi * (Real.pi * |(A : ℝ)| / n) = 2 * |(A : ℝ)| / n := by + field_simp + rw [heq] at this + have : 2 / 11 ≤ 2 * |(A : ℝ)| / n := by + rw [le_div_iff₀ hn] + linarith + linarith + nlinarith [abs_nonneg (Real.sin (2 * Real.pi * A / n / 2))] + +end Frequencies + +/-! ### The ping-pong argument on the frequencies -/ + +section PingPong + +variable {n : ℕ} [NeZero n] + +/-- The frequencies whose centered representatives are both at most `n / 11` in absolute value. -/ +private def IsSmall (ξ : ZMod n × ZMod n) : Prop := + 11 * |ξ.1.valMinAbs| ≤ n ∧ 11 * |ξ.2.valMinAbs| ≤ n + +private instance : DecidablePred (IsSmall (n := n)) := fun _ ↦ instDecidableAnd + +/-- **The ping-pong inequality** for a function on the frequencies vanishing at `0`: its mass is +at most `6` times its mass outside the small box plus `16` times its squared changes along the +four dual shears by `±4`. -/ +private theorem sum_norm_sq_le_pingPong (F : ZMod n × ZMod n → ℂ) (h0 : F 0 = 0) : + ∑ ξ, ‖F ξ‖ ^ 2 ≤ 6 * ∑ ξ ∈ univ.filter (fun ξ ↦ ¬ IsSmall ξ), ‖F ξ‖ ^ 2 + + 16 * (∑ ξ, ‖F (shearSnd (4 : ZMod n) ξ) - F ξ‖ ^ 2 + + ∑ ξ, ‖F (shearSnd (-4 : ZMod n) ξ) - F ξ‖ ^ 2 + + ∑ ξ, ‖F (shearFst (4 : ZMod n) ξ) - F ξ‖ ^ 2 + + ∑ ξ, ‖F (shearFst (-4 : ZMod n) ξ) - F ξ‖ ^ 2) := by + obtain ⟨Out, hOut⟩ : ∃ s : Finset (ZMod n × ZMod n), s = univ.filter (¬ IsSmall ·) := + ⟨_, rfl⟩ + obtain ⟨X, hX⟩ : ∃ s : Finset (ZMod n × ZMod n), + s = univ.filter (fun ξ ↦ IsSmall ξ ∧ |ξ.2.valMinAbs| < |ξ.1.valMinAbs|) := ⟨_, rfl⟩ + obtain ⟨Y, hY⟩ : ∃ s : Finset (ZMod n × ZMod n), + s = univ.filter (fun ξ ↦ IsSmall ξ ∧ |ξ.1.valMinAbs| ≤ |ξ.2.valMinAbs| ∧ ξ ≠ 0) := + ⟨_, rfl⟩ + rw [← hOut] + have hite (p : Prop) [Decidable p] (ξ : ZMod n × ZMod n) : + 0 ≤ if p then ‖F ξ‖ ^ 2 else 0 := by + split_ifs <;> positivity + -- The two classes and the large frequencies cover everything but `0`, where `F` vanishes. + have hpart : ∑ ξ, ‖F ξ‖ ^ 2 ≤ + ∑ ξ ∈ Out, ‖F ξ‖ ^ 2 + ∑ ξ ∈ X, ‖F ξ‖ ^ 2 + ∑ ξ ∈ Y, ‖F ξ‖ ^ 2 := by + rw [hOut, hX, hY, sum_filter, sum_filter, sum_filter, ← sum_add_distrib, ← sum_add_distrib] + refine sum_le_sum fun ξ _ ↦ ?_ + by_cases h : ξ = 0 + · subst h + simp [h0] + have h₁ := hite (¬ IsSmall ξ) ξ + have h₂ := hite (IsSmall ξ ∧ |ξ.2.valMinAbs| < |ξ.1.valMinAbs|) ξ + have h₃ := hite (IsSmall ξ ∧ |ξ.1.valMinAbs| ≤ |ξ.2.valMinAbs| ∧ ξ ≠ 0) ξ + by_cases hs : IsSmall ξ + · by_cases hlt : |ξ.2.valMinAbs| < |ξ.1.valMinAbs| + · rw [ite_eq_left (show IsSmall ξ ∧ |ξ.2.valMinAbs| < |ξ.1.valMinAbs| from ⟨hs, hlt⟩)] + linarith + · rw [ite_eq_left (show IsSmall ξ ∧ |ξ.1.valMinAbs| ≤ |ξ.2.valMinAbs| ∧ ξ ≠ 0 from + ⟨hs, not_lt.1 hlt, h⟩)] + linarith + · rw [ite_eq_left hs] + linarith + -- A frequency with a larger second coordinate is small and in `Y`, or large. + have hY' : ∑ ξ ∈ univ.filter (fun ξ : ZMod n × ZMod n ↦ |ξ.1.valMinAbs| < |ξ.2.valMinAbs|), + ‖F ξ‖ ^ 2 ≤ ∑ ξ ∈ Y, ‖F ξ‖ ^ 2 + ∑ ξ ∈ Out, ‖F ξ‖ ^ 2 := by + rw [hOut, hY, sum_filter, sum_filter, sum_filter, ← sum_add_distrib] + refine sum_le_sum fun ξ _ ↦ ?_ + have h₁ := hite (¬ IsSmall ξ) ξ + have h₃ := hite (IsSmall ξ ∧ |ξ.1.valMinAbs| ≤ |ξ.2.valMinAbs| ∧ ξ ≠ 0) ξ + by_cases hlt : |ξ.1.valMinAbs| < |ξ.2.valMinAbs| + · have hne : ξ ≠ 0 := by + rintro rfl + simp at hlt + rw [ite_eq_left hlt] + by_cases hs : IsSmall ξ + · rw [ite_eq_left (show IsSmall ξ ∧ |ξ.1.valMinAbs| ≤ |ξ.2.valMinAbs| ∧ ξ ≠ 0 from + ⟨hs, hlt.le, hne⟩)] + linarith + · rw [ite_eq_left hs] + linarith + · rw [ite_eq_right hlt] + linarith + have hX' : ∑ ξ ∈ univ.filter (fun ξ : ZMod n × ZMod n ↦ |ξ.2.valMinAbs| < |ξ.1.valMinAbs|), + ‖F ξ‖ ^ 2 ≤ ∑ ξ ∈ X, ‖F ξ‖ ^ 2 + ∑ ξ ∈ Out, ‖F ξ‖ ^ 2 := by + rw [hOut, hX, sum_filter, sum_filter, sum_filter, ← sum_add_distrib] + refine sum_le_sum fun ξ _ ↦ ?_ + have h₁ := hite (¬ IsSmall ξ) ξ + have h₂ := hite (IsSmall ξ ∧ |ξ.2.valMinAbs| < |ξ.1.valMinAbs|) ξ + by_cases hlt : |ξ.2.valMinAbs| < |ξ.1.valMinAbs| + · rw [ite_eq_left hlt] + by_cases hs : IsSmall ξ + · rw [ite_eq_left (show IsSmall ξ ∧ |ξ.2.valMinAbs| < |ξ.1.valMinAbs| from ⟨hs, hlt⟩)] + linarith + · rw [ite_eq_left hs] + linarith + · rw [ite_eq_right hlt] + linarith + -- The dual shears `(a, b) ↦ (a, b ± 4 a)` move `X` into two disjoint sets of `Y'`. + have hXY : ∑ ξ ∈ X, ‖F (shearSnd (4 : ZMod n) ξ)‖ ^ 2 + + ∑ ξ ∈ X, ‖F (shearSnd (-4 : ZMod n) ξ)‖ ^ 2 ≤ + ∑ ξ ∈ univ.filter (fun ξ : ZMod n × ZMod n ↦ |ξ.1.valMinAbs| < |ξ.2.valMinAbs|), + ‖F ξ‖ ^ 2 := by + have himage (k : ℤ) (hk : |k| = 4) (ξ : ZMod n × ZMod n) (hξ : ξ ∈ X) : + (shearSnd (k : ZMod n) ξ).2.valMinAbs = ξ.2.valMinAbs + k * ξ.1.valMinAbs ∧ + |ξ.1.valMinAbs| < |(shearSnd (k : ZMod n) ξ).2.valMinAbs| := by + simp only [hX, mem_filter, mem_univ, true_and] at hξ + unfold IsSmall at hξ + have h := valMinAbs_add_mul (a := ξ.2) (b := ξ.1) hk.le hξ.1.2 hξ.1.1 + refine ⟨h, ?_⟩ + rw [shearSnd_apply, h] + refine abs_lt_abs_add_mul hk hξ.2.le fun h0 ↦ ?_ + rw [h0, abs_zero] at hξ + exact (abs_nonneg _).not_gt hξ.2 + refine sum_comp_add_sum_comp_le F _ _ X _ (fun ξ hξ ↦ ?_) (fun ξ hξ ↦ ?_) + fun ξ hξ ξ' hξ' h ↦ ?_ + · simpa using (himage 4 (by norm_num) ξ hξ).2 + · simpa using (himage (-4) (by norm_num) ξ hξ).2 + · have h₁ := (himage 4 (by norm_num) ξ hξ).1 + have h₂ := (himage (-4) (by norm_num) ξ' hξ').1 + simp only [Int.cast_ofNat, Int.cast_neg] at h₁ h₂ + have hfst : ξ.1 = ξ'.1 := by simpa using congrArg Prod.fst h + rw [h, h₂, ← hfst] at h₁ + simp only [hX, mem_filter, mem_univ, true_and] at hξ hξ' + refine add_four_mul_ne hξ.2.le (hfst ▸ hξ'.2.le) ?_ h₁.symm + intro h0 + rw [h0, abs_zero] at hξ + exact (abs_nonneg _).not_gt hξ.2 + -- The dual shears `(a, b) ↦ (a ± 4 b, b)` move `Y` into two disjoint sets of `X'`. + have hYX : ∑ ξ ∈ Y, ‖F (shearFst (4 : ZMod n) ξ)‖ ^ 2 + + ∑ ξ ∈ Y, ‖F (shearFst (-4 : ZMod n) ξ)‖ ^ 2 ≤ + ∑ ξ ∈ univ.filter (fun ξ : ZMod n × ZMod n ↦ |ξ.2.valMinAbs| < |ξ.1.valMinAbs|), + ‖F ξ‖ ^ 2 := by + have hq (ξ : ZMod n × ZMod n) (hξ : ξ ∈ Y) : ξ.2.valMinAbs ≠ 0 := by + simp only [hY, mem_filter, mem_univ, true_and] at hξ + intro h0 + rw [h0, abs_zero, abs_nonpos_iff, ZMod.valMinAbs_eq_zero] at hξ + rw [ZMod.valMinAbs_eq_zero] at h0 + exact hξ.2.2 (Prod.ext hξ.2.1 h0) + have himage (k : ℤ) (hk : |k| = 4) (ξ : ZMod n × ZMod n) (hξ : ξ ∈ Y) : + (shearFst (k : ZMod n) ξ).1.valMinAbs = ξ.1.valMinAbs + k * ξ.2.valMinAbs ∧ + |ξ.2.valMinAbs| < |(shearFst (k : ZMod n) ξ).1.valMinAbs| := by + have hq := hq ξ hξ + simp only [hY, mem_filter, mem_univ, true_and] at hξ + unfold IsSmall at hξ + have h := valMinAbs_add_mul (a := ξ.1) (b := ξ.2) hk.le hξ.1.1 hξ.1.2 + refine ⟨h, ?_⟩ + rw [shearFst_apply, h] + exact abs_lt_abs_add_mul hk hξ.2.1 hq + refine sum_comp_add_sum_comp_le F _ _ Y _ (fun ξ hξ ↦ ?_) (fun ξ hξ ↦ ?_) + fun ξ hξ ξ' hξ' h ↦ ?_ + · simpa using (himage 4 (by norm_num) ξ hξ).2 + · simpa using (himage (-4) (by norm_num) ξ hξ).2 + · have h₁ := (himage 4 (by norm_num) ξ hξ).1 + have h₂ := (himage (-4) (by norm_num) ξ' hξ').1 + simp only [Int.cast_ofNat, Int.cast_neg] at h₁ h₂ + have hsnd : ξ.2 = ξ'.2 := by simpa using congrArg Prod.snd h + rw [h, h₂, ← hsnd] at h₁ + have hq := hq ξ hξ + simp only [hY, mem_filter, mem_univ, true_and] at hξ hξ' + exact add_four_mul_ne hξ.2.1 (hsnd ▸ hξ'.2.1) hq h₁.symm + -- Mass transfer along each of the four dual shears. + have t₁ : ∑ ξ ∈ X, ‖F ξ‖ ^ 2 ≤ ∑ ξ ∈ X, ‖F (shearSnd (4 : ZMod n) ξ)‖ ^ 2 + + 8 * ∑ ξ, ‖F (shearSnd (4 : ZMod n) ξ) - F ξ‖ ^ 2 + (∑ ξ, ‖F ξ‖ ^ 2) / 8 := + sum_norm_sq_le_sum_comp F _ X + have t₂ : ∑ ξ ∈ X, ‖F ξ‖ ^ 2 ≤ ∑ ξ ∈ X, ‖F (shearSnd (-4 : ZMod n) ξ)‖ ^ 2 + + 8 * ∑ ξ, ‖F (shearSnd (-4 : ZMod n) ξ) - F ξ‖ ^ 2 + (∑ ξ, ‖F ξ‖ ^ 2) / 8 := + sum_norm_sq_le_sum_comp F _ X + have t₃ : ∑ ξ ∈ Y, ‖F ξ‖ ^ 2 ≤ ∑ ξ ∈ Y, ‖F (shearFst (4 : ZMod n) ξ)‖ ^ 2 + + 8 * ∑ ξ, ‖F (shearFst (4 : ZMod n) ξ) - F ξ‖ ^ 2 + (∑ ξ, ‖F ξ‖ ^ 2) / 8 := + sum_norm_sq_le_sum_comp F _ Y + have t₄ : ∑ ξ ∈ Y, ‖F ξ‖ ^ 2 ≤ ∑ ξ ∈ Y, ‖F (shearFst (-4 : ZMod n) ξ)‖ ^ 2 + + 8 * ∑ ξ, ‖F (shearFst (-4 : ZMod n) ξ) - F ξ‖ ^ 2 + (∑ ξ, ‖F ξ‖ ^ 2) / 8 := + sum_norm_sq_le_sum_comp F _ Y + have s₁ : 2 * ∑ ξ ∈ X, ‖F ξ‖ ^ 2 ≤ (∑ ξ ∈ Y, ‖F ξ‖ ^ 2 + ∑ ξ ∈ Out, ‖F ξ‖ ^ 2) + + 8 * (∑ ξ, ‖F (shearSnd (4 : ZMod n) ξ) - F ξ‖ ^ 2 + + ∑ ξ, ‖F (shearSnd (-4 : ZMod n) ξ) - F ξ‖ ^ 2) + (∑ ξ, ‖F ξ‖ ^ 2) / 4 := by + calc 2 * ∑ ξ ∈ X, ‖F ξ‖ ^ 2 = ∑ ξ ∈ X, ‖F ξ‖ ^ 2 + ∑ ξ ∈ X, ‖F ξ‖ ^ 2 := two_mul _ + _ ≤ _ := add_le_add t₁ t₂ + _ = (∑ ξ ∈ X, ‖F (shearSnd (4 : ZMod n) ξ)‖ ^ 2 + + ∑ ξ ∈ X, ‖F (shearSnd (-4 : ZMod n) ξ)‖ ^ 2) + + 8 * (∑ ξ, ‖F (shearSnd (4 : ZMod n) ξ) - F ξ‖ ^ 2 + + ∑ ξ, ‖F (shearSnd (-4 : ZMod n) ξ) - F ξ‖ ^ 2) + (∑ ξ, ‖F ξ‖ ^ 2) / 4 := by + ring + _ ≤ _ := add_le_add (add_le_add (hXY.trans hY') le_rfl) le_rfl + have s₂ : 2 * ∑ ξ ∈ Y, ‖F ξ‖ ^ 2 ≤ (∑ ξ ∈ X, ‖F ξ‖ ^ 2 + ∑ ξ ∈ Out, ‖F ξ‖ ^ 2) + + 8 * (∑ ξ, ‖F (shearFst (4 : ZMod n) ξ) - F ξ‖ ^ 2 + + ∑ ξ, ‖F (shearFst (-4 : ZMod n) ξ) - F ξ‖ ^ 2) + (∑ ξ, ‖F ξ‖ ^ 2) / 4 := by + calc 2 * ∑ ξ ∈ Y, ‖F ξ‖ ^ 2 = ∑ ξ ∈ Y, ‖F ξ‖ ^ 2 + ∑ ξ ∈ Y, ‖F ξ‖ ^ 2 := two_mul _ + _ ≤ _ := add_le_add t₃ t₄ + _ = (∑ ξ ∈ Y, ‖F (shearFst (4 : ZMod n) ξ)‖ ^ 2 + + ∑ ξ ∈ Y, ‖F (shearFst (-4 : ZMod n) ξ)‖ ^ 2) + + 8 * (∑ ξ, ‖F (shearFst (4 : ZMod n) ξ) - F ξ‖ ^ 2 + + ∑ ξ, ‖F (shearFst (-4 : ZMod n) ξ) - F ξ‖ ^ 2) + (∑ ξ, ‖F ξ‖ ^ 2) / 4 := by + ring + _ ≤ _ := add_le_add (add_le_add (hYX.trans hX') le_rfl) le_rfl + linarith only [s₁, s₂, hpart] + +end PingPong + +/-! ### The Poincaré inequality and the spectral gap -/ + +section Gap + +variable {n : ℕ} [NeZero n] + +/-- Parseval's identity for the change of `f` along a translation. -/ +private theorem sum_norm_sq_translate (f : ZMod n × ZMod n → ℂ) (t : ZMod n × ZMod n) : + ∑ ξ, ‖ZMod.stdAddChar (ξ.1 * t.1 + ξ.2 * t.2) - 1‖ ^ 2 * ‖ZMod.dftProd f ξ‖ ^ 2 = + n ^ 2 * ∑ v, ‖f (v + t) - f v‖ ^ 2 := by + rw [← ZMod.sum_norm_sq_dftProd (fun v ↦ f (v + t) - f v)] + refine sum_congr rfl fun ξ _ ↦ ?_ + have : (fun v ↦ f (v + t) - f v) = (fun v ↦ f (v + t)) - f := rfl + rw [this, ZMod.dftProd_sub, Pi.sub_apply, ZMod.dftProd_comp_add, ← sub_one_mul, norm_mul, + mul_pow] + +/-- Parseval's identity for the change of `f` along the shear `(x, y) ↦ (x + k * y, y)`. -/ +private theorem sum_norm_sq_shearFst (f : ZMod n × ZMod n → ℂ) (k : ZMod n) : + ∑ ξ, ‖ZMod.dftProd f (shearSnd (-k) ξ) - ZMod.dftProd f ξ‖ ^ 2 = + n ^ 2 * ∑ v, ‖f (shearFst k v) - f v‖ ^ 2 := by + rw [← ZMod.sum_norm_sq_dftProd (fun v ↦ f (shearFst k v) - f v)] + refine sum_congr rfl fun ξ _ ↦ ?_ + have : (fun v ↦ f (shearFst k v) - f v) = (fun v ↦ f (v.1 + k * v.2, v.2)) - f := rfl + rw [this, ZMod.dftProd_sub, Pi.sub_apply, ZMod.dftProd_comp_shearFst, shearSnd_apply, neg_mul, + ← sub_eq_add_neg] + +/-- Parseval's identity for the change of `f` along the shear `(x, y) ↦ (x, y + k * x)`. -/ +private theorem sum_norm_sq_shearSnd (f : ZMod n × ZMod n → ℂ) (k : ZMod n) : + ∑ ξ, ‖ZMod.dftProd f (shearFst (-k) ξ) - ZMod.dftProd f ξ‖ ^ 2 = + n ^ 2 * ∑ v, ‖f (shearSnd k v) - f v‖ ^ 2 := by + rw [← ZMod.sum_norm_sq_dftProd (fun v ↦ f (shearSnd k v) - f v)] + refine sum_congr rfl fun ξ _ ↦ ?_ + have : (fun v ↦ f (shearSnd k v) - f v) = (fun v ↦ f (v.1, v.2 + k * v.1)) - f := rfl + rw [this, ZMod.dftProd_sub, Pi.sub_apply, ZMod.dftProd_comp_shearSnd, shearFst_apply, neg_mul, + ← sub_eq_add_neg] + +/-- The change along the shears by `4` and `-4` is at most `16` times that along the unit +shear. -/ +private theorem sum_norm_sq_shearFst_four_le (f : ZMod n × ZMod n → ℂ) : + ∑ v, ‖f (shearFst (4 : ZMod n) v) - f v‖ ^ 2 ≤ 16 * ∑ v, ‖f (shearFst 1 v) - f v‖ ^ 2 ∧ + ∑ v, ‖f (shearFst (-4 : ZMod n) v) - f v‖ ^ 2 ≤ + 16 * ∑ v, ‖f (shearFst 1 v) - f v‖ ^ 2 := by + have h4 : shearFst (4 : ZMod n) = shearFst 1 ^ 4 := by + rw [shearFst_pow] + norm_num + have hle := sum_norm_sub_sq_pow_le f (shearFst (1 : ZMod n)) 4 + rw [← h4, show ((4 : ℕ) : ℝ) ^ 2 = 16 by norm_num] at hle + refine ⟨hle, ?_⟩ + rw [← shearFst_symm, sum_norm_sub_sq_symm] + exact hle + +/-- The change along the shears by `4` and `-4` is at most `16` times that along the unit +shear. -/ +private theorem sum_norm_sq_shearSnd_four_le (f : ZMod n × ZMod n → ℂ) : + ∑ v, ‖f (shearSnd (4 : ZMod n) v) - f v‖ ^ 2 ≤ 16 * ∑ v, ‖f (shearSnd 1 v) - f v‖ ^ 2 ∧ + ∑ v, ‖f (shearSnd (-4 : ZMod n) v) - f v‖ ^ 2 ≤ + 16 * ∑ v, ‖f (shearSnd 1 v) - f v‖ ^ 2 := by + have h4 : shearSnd (4 : ZMod n) = shearSnd 1 ^ 4 := by + rw [shearSnd_pow] + norm_num + have hle := sum_norm_sub_sq_pow_le f (shearSnd (1 : ZMod n)) 4 + rw [← h4, show ((4 : ℕ) : ℝ) ^ 2 = 16 by norm_num] at hle + refine ⟨hle, ?_⟩ + rw [← shearSnd_symm, sum_norm_sub_sq_symm] + exact hle + +/-- **The Poincaré inequality for the shear-translation graph**, uniformly in `n`: a complex +function of sum zero on `ZMod n × ZMod n` has squared norm at most `512` times its total squared +change along the four moves. -/ +theorem sum_norm_sq_le_shearTranslation (f : ZMod n × ZMod n → ℂ) (hf : ∑ v, f v = 0) : + ∑ v, ‖f v‖ ^ 2 ≤ 512 * ∑ k, ∑ v, ‖f (shearTranslationMove n k v) - f v‖ ^ 2 := by + set F := ZMod.dftProd f with hF + have h0 : F 0 = 0 := by simp [F, hf] + have hpp := sum_norm_sq_le_pingPong F h0 + have hM : ∑ ξ, ‖F ξ‖ ^ 2 = n ^ 2 * ∑ v, ‖f v‖ ^ 2 := ZMod.sum_norm_sq_dftProd f + -- Large frequencies are paid for by the translations. + have hOut : ∑ ξ ∈ univ.filter (fun ξ ↦ ¬ IsSmall ξ), ‖F ξ‖ ^ 2 ≤ + 8 * (n ^ 2 * ∑ v, ‖f (v + (1, 0)) - f v‖ ^ 2 + n ^ 2 * ∑ v, ‖f (v + (0, 1)) - f v‖ ^ 2) := by + have hw (ξ : ZMod n × ZMod n) (hs : ¬ IsSmall ξ) : + 1 / 8 ≤ ‖ZMod.stdAddChar ξ.1 - 1‖ ^ 2 + ‖ZMod.stdAddChar ξ.2 - 1‖ ^ 2 := by + unfold IsSmall at hs + rcases not_and_or.1 hs with hs | hs + · linarith [one_div_eight_le_norm_stdAddChar_sub_one (not_le.1 hs), + sq_nonneg ‖ZMod.stdAddChar ξ.2 - 1‖] + · linarith [one_div_eight_le_norm_stdAddChar_sub_one (not_le.1 hs), + sq_nonneg ‖ZMod.stdAddChar ξ.1 - 1‖] + rw [← sum_norm_sq_translate, ← sum_norm_sq_translate, ← sum_add_distrib, mul_sum, sum_filter] + refine sum_le_sum fun ξ _ ↦ ?_ + have e₁ : ξ.1 * ((1, 0) : ZMod n × ZMod n).1 + ξ.2 * ((1, 0) : ZMod n × ZMod n).2 = ξ.1 := by + simp + have e₂ : ξ.1 * ((0, 1) : ZMod n × ZMod n).1 + ξ.2 * ((0, 1) : ZMod n × ZMod n).2 = ξ.2 := by + simp + rw [e₁, e₂] + split_ifs with hs + · positivity + · have := mul_le_mul_of_nonneg_right (hw ξ hs) (sq_nonneg ‖F ξ‖) + linarith + -- The dual shears are paid for by the primal shears. + have hD₁ := sum_norm_sq_shearFst f (-4 : ZMod n) + have hD₂ := sum_norm_sq_shearFst f (4 : ZMod n) + have hD₃ := sum_norm_sq_shearSnd f (-4 : ZMod n) + have hD₄ := sum_norm_sq_shearSnd f (4 : ZMod n) + rw [neg_neg] at hD₁ hD₃ + rw [← hF] at hD₁ hD₂ hD₃ hD₄ + have e₁ := sum_norm_sq_shearFst_four_le f + have e₂ := sum_norm_sq_shearSnd_four_le f + have hn : (0 : ℝ) < (n : ℝ) ^ 2 := by + have : (0 : ℝ) < n := by exact_mod_cast Nat.pos_of_ne_zero (NeZero.ne n) + positivity + simp only [Fin.sum_univ_four, shearTranslationMove, Matrix.cons_val_zero, Matrix.cons_val_one, + Matrix.cons_val_two, Matrix.cons_val_three, Matrix.head_cons, Matrix.tail_cons, + Equiv.coe_addRight] + rw [← mul_le_mul_iff_right₀ hn] + have k₁ := mul_le_mul_of_nonneg_left e₁.1 hn.le + have k₂ := mul_le_mul_of_nonneg_left e₁.2 hn.le + have k₃ := mul_le_mul_of_nonneg_left e₂.1 hn.le + have k₄ := mul_le_mul_of_nonneg_left e₂.2 hn.le + have p₁ : 0 ≤ (n : ℝ) ^ 2 * ∑ v, ‖f (v + (1, 0)) - f v‖ ^ 2 := by positivity + have p₂ : 0 ≤ (n : ℝ) ^ 2 * ∑ v, ‖f (v + (0, 1)) - f v‖ ^ 2 := by positivity + linarith + +/-- **The spectral gap of the shear-translation graph**, uniformly in `n`: its second eigenvalue +is at most `1 - 1 / 4096`. -/ +theorem secondEigenvalue_shearTranslation_le (n : ℕ) [NeZero n] : + (shearTranslation n).secondEigenvalue ≤ 1 - 1 / 4096 := by + rcases subsingleton_or_nontrivial (ZMod n × ZMod n) with hV | hV + · rw [secondEigenvalue_eq_zero_of_subsingleton] + norm_num + have h := secondEigenvalue_ofPerms_le (shearTranslationMove n) (c := 1 / 512) fun f hf ↦ ?_ + · rw [shearTranslation] + refine h.trans_eq ?_ + norm_num + have hsum : ∑ v, (f v : ℂ) = 0 := by + rw [Fintype.expect_eq_sum_div_card, div_eq_zero_iff] at hf + rcases hf with hf | hf + · exact_mod_cast hf + · exact absurd hf (by positivity) + have hP := sum_norm_sq_le_shearTranslation (fun v ↦ (f v : ℂ)) hsum + simp only [← Complex.ofReal_sub, Complex.norm_real, Real.norm_eq_abs, sq_abs] at hP + simp only [Fintype.expect_eq_sum_div_card, ← sum_div] + have hcard : (0 : ℝ) < Fintype.card (ZMod n × ZMod n) := by positivity + rw [← mul_div_assoc, div_le_div_iff_of_pos_right hcard] + linarith + +/-- **The lazy shear-translation graph is an expander** uniformly in `n`: its spectral expansion is +at most `1 - 1 / 8192`. -/ +theorem spectralExpansion_lazy_shearTranslation_le (n : ℕ) [NeZero n] : + (shearTranslation n).lazy.spectralExpansion ≤ 1 - 1 / 8192 := by + have := (shearTranslation n).spectralExpansion_lazy_le_one_add_secondEigenvalue_div_two + have := secondEigenvalue_shearTranslation_le n + linarith + +end Gap + +end RotationMap + +end Cslib diff --git a/ComplexityTests/ShearTranslationExpander.lean b/ComplexityTests/ShearTranslationExpander.lean new file mode 100644 index 000000000..f9461ae48 --- /dev/null +++ b/ComplexityTests/ShearTranslationExpander.lean @@ -0,0 +1,65 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +import Complexity.Foundations.Analysis.Fourier.ZModProd +import Complexity.Foundations.Combinatorics.Expander.ShearTranslation +import Complexity.Foundations.Combinatorics.Expander.Mixing +import Mathlib.Algebra.Order.BigOperators.Expect + +/-! +# The shear-translation expander + +Concrete rotations of the shear-translation graph, the Fourier transform at the zero frequency, +and clients of the uniform spectral gap: the Poincaré inequality applied to a concrete function, +and a lower bound on the edges leaving every vertex set, for every `n`. +-/ + +namespace ComplexityTests.ShearTranslationExpander + +open Cslib Cslib.RotationMap Finset + +-- The four forward moves at `(1, 2)` in `ZMod 5 × ZMod 5`, with their return labels. +example : (shearTranslation 5).rot ((1, 2), (0, false)) = ((3, 2), (0, true)) := by decide +example : (shearTranslation 5).rot ((1, 2), (1, false)) = ((1, 3), (1, true)) := by decide +example : (shearTranslation 5).rot ((1, 2), (2, false)) = ((2, 2), (2, true)) := by decide +example : (shearTranslation 5).rot ((1, 2), (3, false)) = ((1, 3), (3, true)) := by decide +-- The backward shear wraps around: `(1, 2) ↦ (1 - 2, 2) = (4, 2)`. +example : (shearTranslation 5).rot ((1, 2), (0, true)) = ((4, 2), (0, false)) := by decide + +-- Iterated shears and their inverses. +example : shearFst (1 : ZMod 7) ^ 3 = shearFst 3 := by + rw [shearFst_pow] + norm_num +example : (shearSnd (2 : ZMod 7)).symm (3, 4) = (3, 5) := by decide + +-- At the zero frequency the transform is the sum: here `5 * 5 = 25` ones. +example : ZMod.dftProd (fun _ : ZMod 5 × ZMod 5 ↦ (1 : ℂ)) 0 = 25 := by + simp only [ZMod.dftProd_zero, sum_const, card_univ, Fintype.card_prod, ZMod.card] + norm_num + +/-- A sum-zero test function: `1` at `(0, 0)` and `-1` at `(1, 0)`. -/ +private noncomputable def dipole (v : ZMod 3 × ZMod 3) : ℂ := + (if v = (0, 0) then 1 else 0) - (if v = (1, 0) then 1 else 0) + +-- The Poincaré inequality applies to it: its hypothesis holds for this concrete function. +example : ∑ v, ‖dipole v‖ ^ 2 ≤ + 512 * ∑ k, ∑ v, ‖dipole (shearTranslationMove 3 k v) - dipole v‖ ^ 2 := + sum_norm_sq_le_shearTranslation dipole (by simp [dipole, sum_sub_distrib]) + +-- The uniform gap bounds the edges leaving every vertex set, for every `n`. +example (n : ℕ) [NeZero n] (S : Finset (ZMod n × ZMod n)) : + (1 - (1 - 1 / 4096) : ℝ) * Fintype.card (Fin 4 × Bool) * #S * #Sᶜ / + Fintype.card (ZMod n × ZMod n) ≤ #((shearTranslation n).interedges S Sᶜ) := by + refine (shearTranslation n).le_card_interedges_compl_of_expect_mul_walk_le (fun f hf ↦ ?_) S + refine ((shearTranslation n).expect_mul_walk_le_secondEigenvalue_mul hf).trans ?_ + exact mul_le_mul_of_nonneg_right (secondEigenvalue_shearTranslation_le n) + (expect_nonneg fun _ _ ↦ sq_nonneg _) + +-- The lazy graph has the uniform spectral expansion bound on, for example, `ZMod 1000`. +example : (shearTranslation 1000).lazy.spectralExpansion < 1 := + (spectralExpansion_lazy_shearTranslation_le 1000).trans_lt (by norm_num) + +end ComplexityTests.ShearTranslationExpander diff --git a/references.bib b/references.bib index ffd09ecfe..d9e33b33a 100644 --- a/references.bib +++ b/references.bib @@ -800,6 +800,15 @@ @article{BuhrmanFortnowVanMelkebeekTorenvliet2000 doi = {10.1137/S0097539798334736} } +@article{Burger1991, + author = {Burger, Marc}, + title = {Kazhdan Constants for {SL}(3, {Z})}, + journal = {Journal f{\"u}r die reine und angewandte Mathematik}, + volume = {413}, + pages = {36--67}, + year = {1991} +} + @misc{Burghardt2018, title = {Simple {Laws} about {Nonprominent} {Properties} of {Binary} {Relations}}, url = {https://arxiv.org/abs/1806.05036v2}, @@ -1680,6 +1689,17 @@ @article{Gabbay2002 keywords = {Keywords: Abstract syntax; Alpha-conversion; Permutation actions; Set theory; Structural induction} } +@article{GabberGalil1981, + author = {Gabber, Ofer and Galil, Zvi}, + title = {Explicit Constructions of Linear-Sized Superconcentrators}, + journal = {Journal of Computer and System Sciences}, + volume = {22}, + number = {3}, + pages = {407--420}, + year = {1981}, + doi = {10.1016/0022-0000(81)90040-4} +} + @book{GareyJohnson1979, author = {Garey, Michael R. and Johnson, David S.}, title = {Computers and Intractability: A Guide to the Theory of {NP}-Completeness}, @@ -2366,6 +2386,16 @@ @inproceedings{ImpagliazzoWigderson1997 doi = {10.1145/258533.258590} } +@article{JimboMaruoka1987, + author = {Jimbo, Shuji and Maruoka, Akira}, + title = {Expanders Obtained from Affine Transformations}, + journal = {Combinatorica}, + volume = {7}, + number = {4}, + pages = {343--355}, + year = {1987} +} + @article{Johnson1962, author = {Johnson, Selmer M.}, title = {A New Upper Bound for Error-Correcting Codes}, @@ -3021,6 +3051,16 @@ @misc{ Malkin2024 url = {https://www.cs.columbia.edu/~tal/3261/fall24/Handouts/3_Myhill_Nerode.pdf} } +@article{Margulis1973, + author = {Margulis, Grigorii A.}, + title = {Explicit Constructions of Expanders}, + journal = {Problemy Peredachi Informatsii}, + volume = {9}, + number = {4}, + pages = {71--80}, + year = {1973} +} + @incollection{McDiarmid1989, author = {McDiarmid, Colin}, title = {On the Method of Bounded Differences}, From 6553d6d4c7194d0c78ccf25f7d652235965a8056 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Fri, 30 Oct 2026 00:03:56 +0000 Subject: [PATCH 2/7] =?UTF-8?q?refactor(Expander):=20share=20the=20shears?= =?UTF-8?q?=20of=20R=20=C3=97=20R;=20credit=20the=20OpenAI=20preprint=20(#?= =?UTF-8?q?1444)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Move Cslib.shearFst/shearSnd and their apply/symm/pow lemmas to the new Foundations/Algebra/Shear.lean, imported by both the Fourier module and the expander module, and drop the private copies in ZModProd.lean. Cite the OpenAI log-space preprint for the Fourier ping-pong idea (7'), adding its bib entry byte-identically to #1676. Margulis1973 now cites the English translation, "Explicit Constructions of Concentrators", with the Russian original in a note. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 1 + Complexity/Foundations/Algebra/Shear.lean | 94 +++++++++++++++++++ .../Analysis/Fourier/ZModProd.lean | 23 +---- .../Expander/ShearTranslation.lean | 72 ++------------ references.bib | 18 +++- 5 files changed, 122 insertions(+), 86 deletions(-) create mode 100644 Complexity/Foundations/Algebra/Shear.lean diff --git a/Complexity.lean b/Complexity.lean index f0509049d..8d2ee4953 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2278,6 +2278,7 @@ public import Complexity.Crypto.Protocols.SigmaProtocol.SchnorrSignature public import Complexity.Crypto.Protocols.Signature.RandomOracle public import Complexity.Foundations.Algebra.FiniteMagnitude public import Complexity.Foundations.Algebra.GeometricTail +public import Complexity.Foundations.Algebra.Shear public import Complexity.Foundations.Analysis.BernoulliInequality public import Complexity.Foundations.Analysis.Fourier.ZModProd public import Complexity.Foundations.Analysis.HarmonicMean diff --git a/Complexity/Foundations/Algebra/Shear.lean b/Complexity/Foundations/Algebra/Shear.lean new file mode 100644 index 000000000..7edbf52e8 --- /dev/null +++ b/Complexity/Foundations/Algebra/Shear.lean @@ -0,0 +1,94 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Algebra.Group.End +public import Mathlib.Algebra.Ring.Defs +import Mathlib.Tactic.Ring + +/-! +# Shears of `R × R` + +The shears `(x, y) ↦ (x + k * y, y)` and `(x, y) ↦ (x, y + k * x)` of `R × R` over a commutative +ring, as permutations. The inverse of a shear is the opposite shear, and iterating a shear `m` +times multiplies its parameter by `m`. + +## Main definitions + +* `Cslib.shearFst`, `Cslib.shearSnd`: the shears `(x, y) ↦ (x + k * y, y)` and + `(x, y) ↦ (x, y + k * x)` of `R × R`. + +## Main results + +* `Cslib.shearFst_symm`, `Cslib.shearSnd_symm`: the inverse of a shear is the opposite shear. +* `Cslib.shearFst_pow`, `Cslib.shearSnd_pow`: iterating a shear `m` times multiplies its + parameter by `m`. +-/ + +@[expose] public section + +namespace Cslib + +variable {R : Type*} [CommRing R] + +/-- The shear `(x, y) ↦ (x + k * y, y)` of `R × R`, as a permutation. -/ +def shearFst (k : R) : Equiv.Perm (R × R) where + toFun v := (v.1 + k * v.2, v.2) + invFun v := (v.1 - k * v.2, v.2) + left_inv v := by simp + right_inv v := by simp + +/-- The shear `(x, y) ↦ (x, y + k * x)` of `R × R`, as a permutation. -/ +def shearSnd (k : R) : Equiv.Perm (R × R) where + toFun v := (v.1, v.2 + k * v.1) + invFun v := (v.1, v.2 - k * v.1) + left_inv v := by simp + right_inv v := by simp + +@[simp] +theorem shearFst_apply (k : R) (v : R × R) : shearFst k v = (v.1 + k * v.2, v.2) := + rfl + +@[simp] +theorem shearSnd_apply (k : R) (v : R × R) : shearSnd k v = (v.1, v.2 + k * v.1) := + rfl + +/-- The inverse of a shear is the opposite shear. -/ +theorem shearFst_symm (k : R) : (shearFst k).symm = shearFst (-k) := by + ext v <;> simp [shearFst, sub_eq_add_neg] + +/-- The inverse of a shear is the opposite shear. -/ +theorem shearSnd_symm (k : R) : (shearSnd k).symm = shearSnd (-k) := by + ext v <;> simp [shearSnd, sub_eq_add_neg] + +/-- Iterating a shear multiplies its parameter. -/ +theorem shearFst_pow (k : R) (m : ℕ) : shearFst k ^ m = shearFst (m * k) := by + induction m with + | zero => ext v <;> simp + | succ m ih => + rw [pow_succ', ih] + ext v + · simp only [Equiv.Perm.mul_apply, shearFst_apply] + push_cast + ring + · rfl + +/-- Iterating a shear multiplies its parameter. -/ +theorem shearSnd_pow (k : R) (m : ℕ) : shearSnd k ^ m = shearSnd (m * k) := by + induction m with + | zero => ext v <;> simp + | succ m ih => + rw [pow_succ', ih] + ext v + · rfl + · simp only [Equiv.Perm.mul_apply, shearSnd_apply] + push_cast + ring + +end Cslib diff --git a/Complexity/Foundations/Analysis/Fourier/ZModProd.lean b/Complexity/Foundations/Analysis/Fourier/ZModProd.lean index 03ce150f2..11214c9ca 100644 --- a/Complexity/Foundations/Analysis/Fourier/ZModProd.lean +++ b/Complexity/Foundations/Analysis/Fourier/ZModProd.lean @@ -9,6 +9,7 @@ module public import Complexity.Init public import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar +import Complexity.Foundations.Algebra.Shear import Mathlib.Analysis.Complex.Basic import Mathlib.NumberTheory.LegendreSymbol.AddCharacter @@ -114,35 +115,21 @@ theorem dftProd_comp_add (f : ZMod N × ZMod N → ℂ) (t ξ : ZMod N × ZMod N congr 2 ring -/-- The shear `(x, y) ↦ (x + k * y, y)` of `ZMod N × ZMod N`, as a permutation. -/ -private def shearFstEquiv (k : ZMod N) : Equiv.Perm (ZMod N × ZMod N) where - toFun v := (v.1 + k * v.2, v.2) - invFun v := (v.1 - k * v.2, v.2) - left_inv v := by simp - right_inv v := by simp - /-- **The shear `(x, y) ↦ (x + k * y, y)`** acts on frequencies by `(a, b) ↦ (a, b - k * a)`. -/ theorem dftProd_comp_shearFst (f : ZMod N × ZMod N → ℂ) (k : ZMod N) (ξ : ZMod N × ZMod N) : dftProd (fun v ↦ f (v.1 + k * v.2, v.2)) ξ = dftProd f (ξ.1, ξ.2 - k * ξ.1) := by rw [dftProd, dftProd] - refine Fintype.sum_equiv (shearFstEquiv k) _ _ fun v ↦ ?_ - simp only [shearFstEquiv, Equiv.coe_fn_mk] + refine Fintype.sum_equiv (Cslib.shearFst k) _ _ fun v ↦ ?_ + rw [Cslib.shearFst_apply] congr 2 ring -/-- The shear `(x, y) ↦ (x, y + k * x)` of `ZMod N × ZMod N`, as a permutation. -/ -private def shearSndEquiv (k : ZMod N) : Equiv.Perm (ZMod N × ZMod N) where - toFun v := (v.1, v.2 + k * v.1) - invFun v := (v.1, v.2 - k * v.1) - left_inv v := by simp - right_inv v := by simp - /-- **The shear `(x, y) ↦ (x, y + k * x)`** acts on frequencies by `(a, b) ↦ (a - k * b, b)`. -/ theorem dftProd_comp_shearSnd (f : ZMod N × ZMod N → ℂ) (k : ZMod N) (ξ : ZMod N × ZMod N) : dftProd (fun v ↦ f (v.1, v.2 + k * v.1)) ξ = dftProd f (ξ.1 - k * ξ.2, ξ.2) := by rw [dftProd, dftProd] - refine Fintype.sum_equiv (shearSndEquiv k) _ _ fun v ↦ ?_ - simp only [shearSndEquiv, Equiv.coe_fn_mk] + refine Fintype.sum_equiv (Cslib.shearSnd k) _ _ fun v ↦ ?_ + rw [Cslib.shearSnd_apply] congr 2 ring diff --git a/Complexity/Foundations/Combinatorics/Expander/ShearTranslation.lean b/Complexity/Foundations/Combinatorics/Expander/ShearTranslation.lean index c23b98d39..bef483af2 100644 --- a/Complexity/Foundations/Combinatorics/Expander/ShearTranslation.lean +++ b/Complexity/Foundations/Combinatorics/Expander/ShearTranslation.lean @@ -9,6 +9,7 @@ module public import Complexity.Foundations.Combinatorics.Expander.Lazy public import Complexity.Foundations.Combinatorics.Expander.Perm +public import Complexity.Foundations.Algebra.Shear public import Mathlib.Data.ZMod.Basic import Complexity.Foundations.Analysis.Fourier.ZModProd import Mathlib.Algebra.Order.Chebyshev @@ -40,14 +41,16 @@ the frequencies `(a, b)` with `|b| < |a|` to two disjoint sets of frequencies wi and those with `0 < |b|`, `|a| ≤ |b|` to two disjoint sets with `|b| < |a|`. Each class therefore carries at least twice the mass of the other, up to small errors, so both are nearly empty. This is a finite, quantitative argument in the spirit of the proof of the relative property (T) of -`SL₂(ℤ) ⋉ ℤ²` [Burger][Burger1991]. +`SL₂(ℤ) ⋉ ℤ²` [Burger][Burger1991]. The idea of proving a uniform gap for a shear-translation +graph on `ZMod n × ZMod n` by an elementary Fourier ping-pong argument, rather than by property +(T), is taken from the OpenAI preprint on derandomizing logarithmic space [OpenAI2026LogSpace]. +The formulation here is our own: the frequency box, the shears by `±4`, the disjoint-image mass +transfer and the constants differ from the preprint's. The explicit constants are far from optimal; the point is that they do not depend on `n`. ## Main definitions -* `Cslib.shearFst`, `Cslib.shearSnd`: the shears `(x, y) ↦ (x + k * y, y)` and - `(x, y) ↦ (x, y + k * x)` of `R × R`. * `Cslib.RotationMap.shearTranslationMove`: the four moves of the graph. * `Cslib.RotationMap.shearTranslation`: the `8`-regular shear-translation multigraph on `ZMod n × ZMod n`. @@ -63,13 +66,14 @@ The explicit constants are far from optimal; the point is that they do not depen ## References -* [G. A. Margulis, *Explicit constructions of expanders*][Margulis1973] +* [G. A. Margulis, *Explicit constructions of concentrators*][Margulis1973] * [O. Gabber, Z. Galil, *Explicit constructions of linear-sized superconcentrators*][GabberGalil1981] * [S. Jimbo, A. Maruoka, *Expanders obtained from affine transformations*][JimboMaruoka1987] * [M. Burger, *Kazhdan constants for SL(3, ℤ)*][Burger1991] * [S. Hoory, N. Linial, A. Wigderson, *Expander graphs and their applications*][HooryLinialWigderson2006] +* [OpenAI, *Exact derandomization of logarithmic space: L = RL = BPL*][OpenAI2026LogSpace] -/ @[expose] public section @@ -78,66 +82,6 @@ namespace Cslib open Finset -section Shear - -variable {R : Type*} [CommRing R] - -/-- The shear `(x, y) ↦ (x + k * y, y)` of `R × R`, as a permutation. -/ -def shearFst (k : R) : Equiv.Perm (R × R) where - toFun v := (v.1 + k * v.2, v.2) - invFun v := (v.1 - k * v.2, v.2) - left_inv v := by simp - right_inv v := by simp - -/-- The shear `(x, y) ↦ (x, y + k * x)` of `R × R`, as a permutation. -/ -def shearSnd (k : R) : Equiv.Perm (R × R) where - toFun v := (v.1, v.2 + k * v.1) - invFun v := (v.1, v.2 - k * v.1) - left_inv v := by simp - right_inv v := by simp - -@[simp] -theorem shearFst_apply (k : R) (v : R × R) : shearFst k v = (v.1 + k * v.2, v.2) := - rfl - -@[simp] -theorem shearSnd_apply (k : R) (v : R × R) : shearSnd k v = (v.1, v.2 + k * v.1) := - rfl - -/-- The inverse of a shear is the opposite shear. -/ -theorem shearFst_symm (k : R) : (shearFst k).symm = shearFst (-k) := by - ext v <;> simp [shearFst, sub_eq_add_neg] - -/-- The inverse of a shear is the opposite shear. -/ -theorem shearSnd_symm (k : R) : (shearSnd k).symm = shearSnd (-k) := by - ext v <;> simp [shearSnd, sub_eq_add_neg] - -/-- Iterating a shear multiplies its parameter. -/ -theorem shearFst_pow (k : R) (m : ℕ) : shearFst k ^ m = shearFst (m * k) := by - induction m with - | zero => ext v <;> simp - | succ m ih => - rw [pow_succ', ih] - ext v - · simp only [Equiv.Perm.mul_apply, shearFst_apply] - push_cast - ring - · rfl - -/-- Iterating a shear multiplies its parameter. -/ -theorem shearSnd_pow (k : R) (m : ℕ) : shearSnd k ^ m = shearSnd (m * k) := by - induction m with - | zero => ext v <;> simp - | succ m ih => - rw [pow_succ', ih] - ext v - · rfl - · simp only [Equiv.Perm.mul_apply, shearSnd_apply] - push_cast - ring - -end Shear - namespace RotationMap /-- The four moves of the shear-translation graph on `ZMod n × ZMod n`: the shears diff --git a/references.bib b/references.bib index d9e33b33a..7cae42ed4 100644 --- a/references.bib +++ b/references.bib @@ -3053,12 +3053,13 @@ @misc{ Malkin2024 @article{Margulis1973, author = {Margulis, Grigorii A.}, - title = {Explicit Constructions of Expanders}, - journal = {Problemy Peredachi Informatsii}, + title = {Explicit Constructions of Concentrators}, + journal = {Problems of Information Transmission}, volume = {9}, number = {4}, - pages = {71--80}, - year = {1973} + pages = {325--332}, + year = {1973}, + note = {Translated from Problemy Peredachi Informatsii 9(4):71--80, 1973, whose Russian title means ``Explicit constructions of expanders''} } @incollection{McDiarmid1989, @@ -3491,6 +3492,15 @@ @misc{OpenAI2026ETH url = {https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/preprints/The-Exponential-Time-Hypothesis-is-False-October-25-2026/paper.pdf} } +@misc{OpenAI2026LogSpace, + author = {{OpenAI}}, + title = {Exact Derandomization of Logarithmic Space: {L} = {RL} = {BPL}}, + year = {2026}, + howpublished = {Preprint}, + note = {Dated 23 September 2026, not peer reviewed; source revision 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a}, + url = {https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/preprints/Exact-Derandomization-of-Logarithmic-Space-L-equals-RL-equals-BPL-September-23-2026/paper.pdf} +} + @misc{OpenAI2026RationalHitting, author = {{OpenAI}}, title = {{Rational} matrix hitting lists for noncommutative rational formulas}, From c1e205d1130ab22d0be2331dfe076d579dc71a2c Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Fri, 30 Oct 2026 00:13:31 +0000 Subject: [PATCH 3/7] docs(Expander): credit the OpenAI Lean development for the Fourier ping-pong (#1444) The preprint's text derives its mixing bound from Shalom's property (T); the elementary route is in OpenAI's AffineSampling.lean at rev 7ef5c0cc (ExactDerandomization.Analysis.Square, ping/squash). Name that file and those declarations, mark the classical sources as background, and align the preprint's reference title with #1676. Co-Authored-By: Claude Opus 5.5 --- .../Expander/ShearTranslation.lean | 20 +++++++++++++------ 1 file changed, 14 insertions(+), 6 deletions(-) diff --git a/Complexity/Foundations/Combinatorics/Expander/ShearTranslation.lean b/Complexity/Foundations/Combinatorics/Expander/ShearTranslation.lean index bef483af2..3efde6834 100644 --- a/Complexity/Foundations/Combinatorics/Expander/ShearTranslation.lean +++ b/Complexity/Foundations/Combinatorics/Expander/ShearTranslation.lean @@ -41,11 +41,17 @@ the frequencies `(a, b)` with `|b| < |a|` to two disjoint sets of frequencies wi and those with `0 < |b|`, `|a| ≤ |b|` to two disjoint sets with `|b| < |a|`. Each class therefore carries at least twice the mass of the other, up to small errors, so both are nearly empty. This is a finite, quantitative argument in the spirit of the proof of the relative property (T) of -`SL₂(ℤ) ⋉ ℤ²` [Burger][Burger1991]. The idea of proving a uniform gap for a shear-translation -graph on `ZMod n × ZMod n` by an elementary Fourier ping-pong argument, rather than by property -(T), is taken from the OpenAI preprint on derandomizing logarithmic space [OpenAI2026LogSpace]. -The formulation here is our own: the frequency box, the shears by `±4`, the disjoint-image mass -transfer and the constants differ from the preprint's. +`SL₂(ℤ) ⋉ ℤ²` [Burger][Burger1991]. + +The OpenAI preprint on derandomizing logarithmic space [OpenAI2026LogSpace] derives its uniform +mixing bound from Shalom's property (T) results. The elementary route used here, a Fourier +ping-pong on the small frequencies of `ZMod n × ZMod n` instead of property (T), follows the Lean +development accompanying the preprint, the file +[`AffineSampling.lean`](https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/lean/OAI/Computability/Logspace/AffineSampling.lean) +at revision `7ef5c0cc`, namespace `ExactDerandomization.Analysis.Square`, lemmas `ping` and +`squash`. The proof here is an independent formulation: the frequency box, the shears by `±4`, +the disjoint-image mass transfer, the constants and all names differ. The works of Margulis, +Gabber and Galil, Jimbo and Maruoka, Burger and Hoory, Linial and Wigderson are background. The explicit constants are far from optimal; the point is that they do not depend on `n`. @@ -73,7 +79,9 @@ The explicit constants are far from optimal; the point is that they do not depen * [M. Burger, *Kazhdan constants for SL(3, ℤ)*][Burger1991] * [S. Hoory, N. Linial, A. Wigderson, *Expander graphs and their applications*][HooryLinialWigderson2006] -* [OpenAI, *Exact derandomization of logarithmic space: L = RL = BPL*][OpenAI2026LogSpace] +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + and its Lean development, the file `AffineSampling.lean` linked above (revision `7ef5c0cc`, + `ExactDerandomization.Analysis.Square.ping`, `squash`), for the elementary route -/ @[expose] public section From 40d6f146b4f3a5c872eb23b323ae549501d11684 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Fri, 30 Oct 2026 01:02:41 +0000 Subject: [PATCH 4/7] =?UTF-8?q?feat(Expander):=20relative=20Poincar=C3=A9?= =?UTF-8?q?=20inequality=20for=20shears=20and=20translations=20with=20a=20?= =?UTF-8?q?spectator=20(#1682)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit From the uniform Poincaré inequality of the shear-translation graph: - on the frequencies: for Φ vanishing at 0, its mass is at most 512 times its changes along the dual unit shears plus its mass weighted by the translation weights ‖e(ξᵢ) - 1‖² (via the bijectivity of dftProd); - with a spectator: when the shears also permute a finite set X and the translations fix it, every function on X × (ZMod n × ZMod n) is within 512 times its total squared change of its fiber averages over ZMod n × ZMod n (complex sums and real averages). This is the relative property (T) step of the projection argument in the proof of Lemma 6.1 of the OpenAI preprint, step (A) of the frame-lifted gap plan on #1682. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 1 + .../Expander/RelativeShearTranslation.lean | 351 ++++++++++++++++++ ComplexityTests/RelativeShearTranslation.lean | 47 +++ 3 files changed, 399 insertions(+) create mode 100644 Complexity/Foundations/Combinatorics/Expander/RelativeShearTranslation.lean create mode 100644 ComplexityTests/RelativeShearTranslation.lean diff --git a/Complexity.lean b/Complexity.lean index 8d2ee4953..e2466576e 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2374,6 +2374,7 @@ public import Complexity.Foundations.Combinatorics.Expander.Power public import Complexity.Foundations.Combinatorics.Expander.Random public import Complexity.Foundations.Combinatorics.Expander.Reindex public import Complexity.Foundations.Combinatorics.Expander.Reingold +public import Complexity.Foundations.Combinatorics.Expander.RelativeShearTranslation public import Complexity.Foundations.Combinatorics.Expander.Replacement public import Complexity.Foundations.Combinatorics.Expander.ShearTranslation public import Complexity.Foundations.Combinatorics.Expander.SimpleGraph diff --git a/Complexity/Foundations/Combinatorics/Expander/RelativeShearTranslation.lean b/Complexity/Foundations/Combinatorics/Expander/RelativeShearTranslation.lean new file mode 100644 index 000000000..d96c0046b --- /dev/null +++ b/Complexity/Foundations/Combinatorics/Expander/RelativeShearTranslation.lean @@ -0,0 +1,351 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Analysis.Fourier.ZModProd +public import Complexity.Foundations.Algebra.Shear +public import Complexity.Foundations.Combinatorics.Expander.ShearTranslation +public import Mathlib.Analysis.InnerProductSpace.PiL2 +-- `import all`: the linearity of `ZMod.dftProd` unfolds its body, and the frequency-side +-- inequality reuses the private Parseval identity for translations, `sum_norm_sq_translate`. +import all Complexity.Foundations.Analysis.Fourier.ZModProd +import all Complexity.Foundations.Combinatorics.Expander.ShearTranslation +import Mathlib.LinearAlgebra.FiniteDimensional.Basic + +/-! +# The relative Poincaré inequality for shears and translations + +The Poincaré inequality for the shear-translation graph on `ZMod n × ZMod n` +(`sum_norm_sq_le_shearTranslation`) has two consequences proved here. + +**On the frequencies.** Through the Fourier transform `ZMod.dftProd`, which is a bijection, the +inequality gives one for an arbitrary function `Φ` on the frequencies that vanishes at +`0` (`sum_norm_sq_le_dual_shearTranslation`). The translations become the weights +`‖e (ξ.1) - 1‖ ^ 2` and `‖e (ξ.2) - 1‖ ^ 2`, and the unit shears become the dual shears by `-1`. + +**With a spectator.** Let the shears act on `X × (ZMod n × ZMod n)` together with permutations +`π₁`, `π₂` of a finite set `X`, while the translations leave `X` fixed +(`twistedShearTranslationMove`). Then every function `f` is close to its averages over the fibers +`{x} × (ZMod n × ZMod n)`: their squared distance is at most `512` times the total squared change +of `f` along the four moves (`sum_norm_sq_sub_fiber_le_twistedShearTranslation`, and +`expect_sq_sub_expect_fiber_le_twistedShearTranslation` for real functions and averages). Unlike a +spectral gap, this does not ask the moves to mix `X`: it is a *relative* Poincaré inequality, which +in a representation-theoretic language says that vectors almost invariant under shears and +translations are close to vectors invariant under the translations. The proof transforms `f` in +the second coordinate, `F x = dftProd (f (x, ·))`, and applies the inequality on the frequencies to +`Φ ξ = ‖F · ξ‖` (the `ℓ²` norm over `X`) for `ξ ≠ 0`. The spectator permutations only reindex +this norm, and the reverse triangle inequality bounds the changes of `Φ` by those of `F`. + +This is the step that turns the uniform gap on `ZMod n × ZMod n` into closeness to the vectors +fixed by the translations of one coordinate pair, as in the projection argument of the OpenAI +preprint on derandomizing logarithmic space for its affine walks +[OpenAI, proof of Lemma 6.1][OpenAI2026LogSpace]. The preprint takes it from Shalom's quantitative +relative property (T) of `(SL₂(ℤ) ⋉ ℤ², ℤ²)`; see also [Burger][Burger1991]. The elementary route +through the uniform Fourier gap is credited in the module of `Cslib.RotationMap.shearTranslation`. +The statements and proofs here are ours. + +## Main definitions + +* `Cslib.RotationMap.twistedShearTranslationMove`: the shears and translations of the second + coordinate of `X × (ZMod n × ZMod n)`, with the shears also permuting `X`. + +## Main results + +* `ZMod.dftProd_add`, `ZMod.dftProd_smul`: the transform is linear. +* `ZMod.dftProd_injective`, `ZMod.dftProd_surjective`: the transform is a bijection. +* `ZMod.sum_norm_sq_dftProd_shearFst_sub`, `ZMod.sum_norm_sq_dftProd_shearSnd_sub`: Parseval's + identity for the difference of two functions, one of them sheared. +* `ZMod.dftProd_const_of_ne_zero`: a constant has no nonzero frequencies. +* `Cslib.RotationMap.sum_norm_sq_le_dual_shearTranslation`: the Poincaré inequality on the + frequencies. +* `Cslib.RotationMap.sum_norm_sq_sub_fiber_le_twistedShearTranslation`, + `Cslib.RotationMap.expect_sq_sub_expect_fiber_le_twistedShearTranslation`: the relative + Poincaré inequality with a spectator. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace] +* [M. Burger, *Kazhdan constants for SL(3, ℤ)*][Burger1991] +-/ + +public section + +open Finset +open scoped BigOperators + +namespace ZMod + +variable {N : ℕ} [NeZero N] + +/-- The transform is additive. -/ +theorem dftProd_add (f g : ZMod N × ZMod N → ℂ) : dftProd (f + g) = dftProd f + dftProd g := by + ext ξ + simp only [dftProd, Pi.add_apply, mul_add, sum_add_distrib] + +/-- The transform is homogeneous. -/ +theorem dftProd_smul (c : ℂ) (f : ZMod N × ZMod N → ℂ) : dftProd (c • f) = c • dftProd f := by + ext ξ + simp only [dftProd, Pi.smul_apply, smul_eq_mul, mul_sum] + exact sum_congr rfl fun _ _ ↦ by ring + +/-- The transform is injective, by Parseval's identity. -/ +theorem dftProd_injective : Function.Injective (dftProd (N := N)) := by + intro f g h + have hP := sum_norm_sq_dftProd (f - g) + rw [dftProd_sub, h, sub_self] at hP + simp only [Pi.zero_apply, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, + sum_const_zero] at hP + have hN : (N : ℝ) ^ 2 ≠ 0 := pow_ne_zero _ (Nat.cast_ne_zero.2 (NeZero.ne N)) + have h0 := (mul_eq_zero.1 hP.symm).resolve_left hN + rw [sum_eq_zero_iff_of_nonneg fun _ _ ↦ by positivity] at h0 + funext v + simpa [sub_eq_zero] using h0 v (mem_univ v) + +/-- The transform as a linear map. -/ +private noncomputable def dftProdLinearMap : + (ZMod N × ZMod N → ℂ) →ₗ[ℂ] (ZMod N × ZMod N → ℂ) where + toFun := dftProd + map_add' := dftProd_add + map_smul' := dftProd_smul + +/-- The transform is surjective: an injective linear endomorphism of a finite-dimensional space. -/ +theorem dftProd_surjective : Function.Surjective (dftProd (N := N)) := + LinearMap.injective_iff_surjective.1 (show Function.Injective dftProdLinearMap from + dftProd_injective (N := N)) + +/-- **A constant has no nonzero frequencies**: Parseval's identity puts all of its mass at `0`. -/ +theorem dftProd_const_of_ne_zero (c : ℂ) {ξ : ZMod N × ZMod N} (hξ : ξ ≠ 0) : + dftProd (fun _ ↦ c) ξ = 0 := by + have hP := sum_norm_sq_dftProd (N := N) fun _ ↦ c + rw [← add_sum_erase _ _ (mem_univ (0 : ZMod N × ZMod N)), dftProd_zero] at hP + simp only [sum_const, card_univ, Fintype.card_prod, ZMod.card, nsmul_eq_mul, norm_mul, + Complex.norm_natCast, Nat.cast_mul] at hP + have h0 : ∑ ζ ∈ univ.erase (0 : ZMod N × ZMod N), ‖dftProd (fun _ ↦ c) ζ‖ ^ 2 = 0 := by linarith + rw [sum_eq_zero_iff_of_nonneg fun _ _ ↦ by positivity] at h0 + simpa using h0 ξ (mem_erase.2 ⟨hξ, mem_univ ξ⟩) + +/-- **Parseval's identity for the difference of two functions along the shear** +`(x, y) ↦ (x + k * y, y)`: it acts on the frequencies by the dual shear `(a, b) ↦ (a, b - k * a)`. +-/ +theorem sum_norm_sq_dftProd_shearFst_sub (f g : ZMod N × ZMod N → ℂ) (k : ZMod N) : + ∑ ξ, ‖dftProd f (Cslib.shearSnd (-k) ξ) - dftProd g ξ‖ ^ 2 = + N ^ 2 * ∑ v, ‖f (Cslib.shearFst k v) - g v‖ ^ 2 := by + rw [← sum_norm_sq_dftProd (fun v ↦ f (Cslib.shearFst k v) - g v)] + refine sum_congr rfl fun ξ _ ↦ ?_ + have : (fun v ↦ f (Cslib.shearFst k v) - g v) = (fun v ↦ f (v.1 + k * v.2, v.2)) - g := rfl + rw [this, dftProd_sub, Pi.sub_apply, dftProd_comp_shearFst, Cslib.shearSnd_apply, neg_mul, + ← sub_eq_add_neg] + +/-- **Parseval's identity for the difference of two functions along the shear** +`(x, y) ↦ (x, y + k * x)`: it acts on the frequencies by the dual shear `(a, b) ↦ (a - k * b, b)`. +-/ +theorem sum_norm_sq_dftProd_shearSnd_sub (f g : ZMod N × ZMod N → ℂ) (k : ZMod N) : + ∑ ξ, ‖dftProd f (Cslib.shearFst (-k) ξ) - dftProd g ξ‖ ^ 2 = + N ^ 2 * ∑ v, ‖f (Cslib.shearSnd k v) - g v‖ ^ 2 := by + rw [← sum_norm_sq_dftProd (fun v ↦ f (Cslib.shearSnd k v) - g v)] + refine sum_congr rfl fun ξ _ ↦ ?_ + have : (fun v ↦ f (Cslib.shearSnd k v) - g v) = (fun v ↦ f (v.1, v.2 + k * v.1)) - g := rfl + rw [this, dftProd_sub, Pi.sub_apply, dftProd_comp_shearSnd, Cslib.shearFst_apply, neg_mul, + ← sub_eq_add_neg] + +end ZMod + +namespace Cslib.RotationMap + +variable {n : ℕ} [NeZero n] + +/-- **The Poincaré inequality for shears and translations, on the frequencies**: a function `Φ` on +`ZMod n × ZMod n` vanishing at `0` has squared norm at most `512` times the sum of its squared +changes along the dual unit shears and of its squared norm weighted by the translation weights +`‖e (ξ.1) - 1‖ ^ 2` and `‖e (ξ.2) - 1‖ ^ 2`, where `e = ZMod.stdAddChar`. -/ +theorem sum_norm_sq_le_dual_shearTranslation (Φ : ZMod n × ZMod n → ℂ) (h0 : Φ 0 = 0) : + ∑ ξ, ‖Φ ξ‖ ^ 2 ≤ 512 * (∑ ξ, ‖Φ (shearSnd (-1) ξ) - Φ ξ‖ ^ 2 + + ∑ ξ, ‖Φ (shearFst (-1) ξ) - Φ ξ‖ ^ 2 + + ∑ ξ, ‖ZMod.stdAddChar ξ.1 - 1‖ ^ 2 * ‖Φ ξ‖ ^ 2 + + ∑ ξ, ‖ZMod.stdAddChar ξ.2 - 1‖ ^ 2 * ‖Φ ξ‖ ^ 2) := by + obtain ⟨f, rfl⟩ := ZMod.dftProd_surjective Φ + have hf : ∑ v, f v = 0 := by rwa [ZMod.dftProd_zero] at h0 + have hP := sum_norm_sq_le_shearTranslation f hf + simp only [Fin.sum_univ_four, shearTranslationMove, Matrix.cons_val_zero, Matrix.cons_val_one, + Matrix.cons_val_two, Matrix.cons_val_three, Matrix.head_cons, Matrix.tail_cons, + Equiv.coe_addRight] at hP + have e₁ := ZMod.sum_norm_sq_dftProd_shearFst_sub f f 1 + have e₂ := ZMod.sum_norm_sq_dftProd_shearSnd_sub f f 1 + have e₃ := sum_norm_sq_translate f (1, 0) + have e₄ := sum_norm_sq_translate f (0, 1) + simp only [mul_one, mul_zero, add_zero, zero_add] at e₃ e₄ + have hM := ZMod.sum_norm_sq_dftProd f + have hn : (0 : ℝ) ≤ (n : ℝ) ^ 2 := by positivity + have := mul_le_mul_of_nonneg_left hP hn + rw [hM, e₁, e₂, e₃, e₄] + linarith + +omit [NeZero n] in +/-- Only the zero vector is sheared to zero. -/ +private theorem shearFst_eq_zero_iff (k : ZMod n) (ξ : ZMod n × ZMod n) : + shearFst k ξ = 0 ↔ ξ = 0 := by + have h0 : shearFst k (0 : ZMod n × ZMod n) = 0 := by simp [shearFst_apply] + exact ⟨fun h ↦ (shearFst k).injective (h.trans h0.symm), fun h ↦ h ▸ h0⟩ + +omit [NeZero n] in +private theorem shearSnd_eq_zero_iff (k : ZMod n) (ξ : ZMod n × ZMod n) : + shearSnd k ξ = 0 ↔ ξ = 0 := by + have h0 : shearSnd k (0 : ZMod n × ZMod n) = 0 := by simp [shearSnd_apply] + exact ⟨fun h ↦ (shearSnd k).injective (h.trans h0.symm), fun h ↦ h ▸ h0⟩ + +variable {X : Type*} + +/-- The shears and translations of the second coordinate of `X × (ZMod n × ZMod n)`, with the +shears also permuting the spectator coordinate: `(x, w) ↦ (π₁ x, shearFst 1 w)`, +`(x, w) ↦ (π₂ x, shearSnd 1 w)`, `(x, w) ↦ (x, w + (1, 0))` and `(x, w) ↦ (x, w + (0, 1))`. -/ +@[expose] +def twistedShearTranslationMove (π₁ π₂ : Equiv.Perm X) (n : ℕ) : + Fin 4 → Equiv.Perm (X × (ZMod n × ZMod n)) := + ![π₁.prodCongr (shearFst 1), π₂.prodCongr (shearSnd 1), + (Equiv.refl X).prodCongr (Equiv.addRight (1, 0)), + (Equiv.refl X).prodCongr (Equiv.addRight (0, 1))] + +/-- The reverse triangle inequality for the `ℓ²` norm of complex functions on a finite set. -/ +private theorem sq_sqrt_sub_sqrt_le [Fintype X] (a b : X → ℂ) : + (√(∑ x, ‖a x‖ ^ 2) - √(∑ x, ‖b x‖ ^ 2)) ^ 2 ≤ ∑ x, ‖a x - b x‖ ^ 2 := by + have h := abs_norm_sub_norm_le (WithLp.toLp 2 a : EuclideanSpace ℂ X) (WithLp.toLp 2 b) + rw [EuclideanSpace.norm_eq, EuclideanSpace.norm_eq, EuclideanSpace.norm_eq] at h + simp only [PiLp.sub_apply] at h + calc _ = |√(∑ x, ‖a x‖ ^ 2) - √(∑ x, ‖b x‖ ^ 2)| ^ 2 := (sq_abs _).symm + _ ≤ √(∑ x, ‖a x - b x‖ ^ 2) ^ 2 := pow_le_pow_left₀ (abs_nonneg _) h 2 + _ = _ := Real.sq_sqrt (sum_nonneg fun _ _ ↦ by positivity) + +variable [Fintype X] + +/-- **The relative Poincaré inequality for shears and translations**, uniformly in `n` and with a +spectator: every complex function `f` on `X × (ZMod n × ZMod n)` is within `512` times its total +squared change along the four moves of its averages over the fibers `{x} × (ZMod n × ZMod n)`. -/ +theorem sum_norm_sq_sub_fiber_le_twistedShearTranslation (π₁ π₂ : Equiv.Perm X) + (f : X × (ZMod n × ZMod n) → ℂ) : + ∑ p, ‖f p - (∑ w, f (p.1, w)) / (n : ℂ) ^ 2‖ ^ 2 ≤ + 512 * ∑ k, ∑ p, ‖f (twistedShearTranslationMove π₁ π₂ n k p) - f p‖ ^ 2 := by + have hn : (0 : ℝ) < (n : ℝ) ^ 2 := by + have : (0 : ℝ) < n := by exact_mod_cast Nat.pos_of_ne_zero (NeZero.ne n) + positivity + have hnC : (n : ℂ) ^ 2 ≠ 0 := pow_ne_zero _ (Nat.cast_ne_zero.2 (NeZero.ne n)) + -- The transforms of the fibers, and of the fibers minus their averages. + set F : X → ZMod n × ZMod n → ℂ := fun x ↦ ZMod.dftProd fun w ↦ f (x, w) with hF + set g : X → ℂ := fun x ↦ (∑ w, f (x, w)) / (n : ℂ) ^ 2 with hg + have hcard : (Fintype.card (ZMod n × ZMod n) : ℂ) = (n : ℂ) ^ 2 := by + simp [Fintype.card_prod, ZMod.card, sq] + have hdft (x : X) (ξ : ZMod n × ZMod n) : + ‖ZMod.dftProd (fun w ↦ f (x, w) - g x) ξ‖ ^ 2 = if ξ = 0 then 0 else ‖F x ξ‖ ^ 2 := by + split_ifs with hξ + · subst hξ + rw [ZMod.dftProd_zero, sum_sub_distrib, sum_const, card_univ, nsmul_eq_mul, hcard] + simp only [hg] + rw [mul_div_cancel₀ _ hnC, sub_self, norm_zero, sq, mul_zero] + · have : (fun w ↦ f (x, w) - g x) = (fun w ↦ f (x, w)) - fun _ ↦ g x := rfl + rw [this, ZMod.dftProd_sub, Pi.sub_apply, ZMod.dftProd_const_of_ne_zero _ hξ, sub_zero] + -- The function on the frequencies: the `ℓ²` norm over `X` of the nonzero frequencies. + set ψ : ZMod n × ZMod n → ℝ := fun ξ ↦ if ξ = 0 then 0 else √(∑ x, ‖F x ξ‖ ^ 2) with hψ + have hψsq (ξ : ZMod n × ZMod n) : + ‖(ψ ξ : ℂ)‖ ^ 2 = ∑ x, if ξ = 0 then 0 else ‖F x ξ‖ ^ 2 := by + rw [Complex.norm_real, Real.norm_eq_abs, sq_abs] + simp only [hψ] + split_ifs + · simp + · exact Real.sq_sqrt (sum_nonneg fun _ _ ↦ by positivity) + have hmain := sum_norm_sq_le_dual_shearTranslation (fun ξ ↦ (ψ ξ : ℂ)) (by simp [hψ]) + -- The mass of `ψ` is that of the fibers minus their averages. + have hL : ∑ ξ, ‖(ψ ξ : ℂ)‖ ^ 2 = + (n : ℝ) ^ 2 * ∑ p, ‖f p - (∑ w, f (p.1, w)) / (n : ℂ) ^ 2‖ ^ 2 := by + calc ∑ ξ, ‖(ψ ξ : ℂ)‖ ^ 2 = ∑ x, ∑ ξ, if ξ = 0 then 0 else ‖F x ξ‖ ^ 2 := by + simp only [hψsq] + exact sum_comm + _ = ∑ x, ∑ ξ, ‖ZMod.dftProd (fun w ↦ f (x, w) - g x) ξ‖ ^ 2 := by simp only [hdft] + _ = ∑ x, (n : ℝ) ^ 2 * ∑ w, ‖f (x, w) - g x‖ ^ 2 := + sum_congr rfl fun x _ ↦ ZMod.sum_norm_sq_dftProd _ + _ = _ := by rw [← mul_sum, Fintype.sum_prod_type] + -- The changes of `ψ` along the dual shears are at most those of `F`. + have hshear (π : Equiv.Perm X) (s : Equiv.Perm (ZMod n × ZMod n)) (hs : ∀ ξ, s ξ = 0 ↔ ξ = 0) + (ξ : ZMod n × ZMod n) : + ‖(ψ (s ξ) : ℂ) - ψ ξ‖ ^ 2 ≤ ∑ x, ‖F (π x) (s ξ) - F x ξ‖ ^ 2 := by + rw [← Complex.ofReal_sub, Complex.norm_real, Real.norm_eq_abs, sq_abs] + by_cases hξ : ξ = 0 + · subst hξ + have h0 : s 0 = 0 := (hs 0).2 rfl + have e : ψ (s 0) - ψ 0 = 0 := by simp only [hψ, h0, ite_true, sub_self] + rw [e, sq, mul_zero] + exact sum_nonneg fun _ _ ↦ by positivity + · have : s ξ ≠ 0 := fun h ↦ hξ ((hs ξ).1 h) + simp only [hψ, this, hξ, ite_false] + rw [← Equiv.sum_comp π fun x ↦ ‖F x (s ξ)‖ ^ 2] + exact sq_sqrt_sub_sqrt_le (fun x ↦ F (π x) (s ξ)) (fun x ↦ F x ξ) + have hS₁ : ∑ ξ, ‖(ψ (shearSnd (-1) ξ) : ℂ) - ψ ξ‖ ^ 2 ≤ + (n : ℝ) ^ 2 * ∑ p, ‖f (twistedShearTranslationMove π₁ π₂ n 0 p) - f p‖ ^ 2 := by + calc _ ≤ ∑ ξ, ∑ x, ‖F (π₁ x) (shearSnd (-1) ξ) - F x ξ‖ ^ 2 := + sum_le_sum fun ξ _ ↦ hshear π₁ _ (shearSnd_eq_zero_iff _) ξ + _ = _ := by + rw [sum_comm, Fintype.sum_prod_type, mul_sum] + refine sum_congr rfl fun x _ ↦ ?_ + exact ZMod.sum_norm_sq_dftProd_shearFst_sub (fun w ↦ f (π₁ x, w)) (fun w ↦ f (x, w)) 1 + have hS₂ : ∑ ξ, ‖(ψ (shearFst (-1) ξ) : ℂ) - ψ ξ‖ ^ 2 ≤ + (n : ℝ) ^ 2 * ∑ p, ‖f (twistedShearTranslationMove π₁ π₂ n 1 p) - f p‖ ^ 2 := by + calc _ ≤ ∑ ξ, ∑ x, ‖F (π₂ x) (shearFst (-1) ξ) - F x ξ‖ ^ 2 := + sum_le_sum fun ξ _ ↦ hshear π₂ _ (shearFst_eq_zero_iff _) ξ + _ = _ := by + rw [sum_comm, Fintype.sum_prod_type, mul_sum] + refine sum_congr rfl fun x _ ↦ ?_ + exact ZMod.sum_norm_sq_dftProd_shearSnd_sub (fun w ↦ f (π₂ x, w)) (fun w ↦ f (x, w)) 1 + -- The translation weights of `ψ` are those of `F`. + have hweight (c : ZMod n × ZMod n → ℝ) (hc : ∀ ξ, 0 ≤ c ξ) : + ∑ ξ, c ξ * ‖(ψ ξ : ℂ)‖ ^ 2 ≤ ∑ x, ∑ ξ, c ξ * ‖F x ξ‖ ^ 2 := by + rw [sum_comm] + refine sum_le_sum fun ξ _ ↦ ?_ + rw [hψsq, mul_sum] + refine sum_le_sum fun x _ ↦ ?_ + split_ifs + · have := hc ξ + simp only [mul_zero] + positivity + · exact le_rfl + have hT₁ : ∑ ξ, ‖ZMod.stdAddChar ξ.1 - 1‖ ^ 2 * ‖(ψ ξ : ℂ)‖ ^ 2 ≤ + (n : ℝ) ^ 2 * ∑ p, ‖f (twistedShearTranslationMove π₁ π₂ n 2 p) - f p‖ ^ 2 := by + refine (hweight _ fun _ ↦ by positivity).trans_eq ?_ + rw [Fintype.sum_prod_type, mul_sum] + refine sum_congr rfl fun x _ ↦ ?_ + have := sum_norm_sq_translate (fun w ↦ f (x, w)) (1, 0) + simp only [mul_one, mul_zero, add_zero] at this + exact this + have hT₂ : ∑ ξ, ‖ZMod.stdAddChar ξ.2 - 1‖ ^ 2 * ‖(ψ ξ : ℂ)‖ ^ 2 ≤ + (n : ℝ) ^ 2 * ∑ p, ‖f (twistedShearTranslationMove π₁ π₂ n 3 p) - f p‖ ^ 2 := by + refine (hweight _ fun _ ↦ by positivity).trans_eq ?_ + rw [Fintype.sum_prod_type, mul_sum] + refine sum_congr rfl fun x _ ↦ ?_ + have := sum_norm_sq_translate (fun w ↦ f (x, w)) (0, 1) + simp only [mul_one, mul_zero, zero_add] at this + exact this + refine le_of_mul_le_mul_left ?_ hn + rw [← hL, Fin.sum_univ_four, mul_left_comm] + linarith + +/-- **The relative Poincaré inequality for shears and translations**, for real functions and +averages: the second moment of `f` about its averages over the fibers `{x} × (ZMod n × ZMod n)` is +at most `512` times the sum of its mean squared changes along the four moves. -/ +theorem expect_sq_sub_expect_fiber_le_twistedShearTranslation (π₁ π₂ : Equiv.Perm X) + (f : X × (ZMod n × ZMod n) → ℝ) : + 𝔼 p, (f p - 𝔼 w, f (p.1, w)) ^ 2 ≤ + 512 * ∑ k, 𝔼 p, (f (twistedShearTranslationMove π₁ π₂ n k p) - f p) ^ 2 := by + have h := sum_norm_sq_sub_fiber_le_twistedShearTranslation π₁ π₂ fun p ↦ (f p : ℂ) + have hfib (x : X) : (∑ w, (f (x, w) : ℂ)) / (n : ℂ) ^ 2 = ((𝔼 w, f (x, w) : ℝ) : ℂ) := by + rw [Fintype.expect_eq_sum_div_card, Fintype.card_prod, ZMod.card] + push_cast + ring + simp only [hfib, ← Complex.ofReal_sub, Complex.norm_real, Real.norm_eq_abs, sq_abs] at h + simp only [Fintype.expect_eq_sum_div_card, ← sum_div] + rw [← mul_div_assoc] + exact div_le_div_of_nonneg_right (by simpa [Fintype.expect_eq_sum_div_card] using h) + (Nat.cast_nonneg _) + +end Cslib.RotationMap diff --git a/ComplexityTests/RelativeShearTranslation.lean b/ComplexityTests/RelativeShearTranslation.lean new file mode 100644 index 000000000..43e7fa54a --- /dev/null +++ b/ComplexityTests/RelativeShearTranslation.lean @@ -0,0 +1,47 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +import Complexity.Foundations.Combinatorics.Expander.RelativeShearTranslation + +/-! +# The relative Poincaré inequality for shears and translations + +Concrete moves with a spectator, the transform of a constant, and a client of the relative +Poincaré inequality: a function invariant under the four moves is constant on every fiber +`{x} × (ZMod n × ZMod n)`, for every `n` and every pair of spectator permutations. +-/ + +namespace ComplexityTests.RelativeShearTranslation + +open Cslib Cslib.RotationMap Finset +open scoped BigOperators + +-- The shears move the spectator; the translations do not. +example : twistedShearTranslationMove (Equiv.addRight (1 : ZMod 3)) (Equiv.refl _) 5 0 + (0, (1, 2)) = (1, (3, 2)) := by decide +example : twistedShearTranslationMove (Equiv.addRight (1 : ZMod 3)) (Equiv.refl _) 5 1 + (0, (1, 2)) = (0, (1, 3)) := by decide +example : twistedShearTranslationMove (Equiv.addRight (1 : ZMod 3)) (Equiv.refl _) 5 2 + (2, (4, 2)) = (2, (0, 2)) := by decide + +-- A constant has no nonzero frequencies. +example : ZMod.dftProd (N := 4) (fun _ ↦ (7 : ℂ)) (1, 3) = 0 := + ZMod.dftProd_const_of_ne_zero 7 (by decide) + +/-- **A client**: a real function on `X × (ZMod n × ZMod n)` invariant under the four moves is +constant on every fiber, whatever the spectator permutations. -/ +example {X : Type*} [Fintype X] (n : ℕ) [NeZero n] (π₁ π₂ : Equiv.Perm X) + (f : X × (ZMod n × ZMod n) → ℝ) + (hf : ∀ k p, f (twistedShearTranslationMove π₁ π₂ n k p) = f p) (p : X × (ZMod n × ZMod n)) : + f p = 𝔼 w, f (p.1, w) := by + have h := expect_sq_sub_expect_fiber_le_twistedShearTranslation π₁ π₂ f + simp only [hf, sub_self, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, + expect_const_zero, sum_const_zero, mul_zero] at h + have h0 := (Fintype.expect_eq_zero_iff_of_nonneg fun q ↦ sq_nonneg + (f q - 𝔼 w, f (q.1, w))).1 (le_antisymm h (expect_nonneg fun _ _ ↦ sq_nonneg _)) + exact sub_eq_zero.1 (pow_eq_zero_iff two_ne_zero |>.1 (congrFun h0 p)) + +end ComplexityTests.RelativeShearTranslation From 3db1f8fc0c541caf41f9068a34bb0f6b72a2ee0c Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Fri, 30 Oct 2026 01:09:46 +0000 Subject: [PATCH 5/7] refactor(Expander): move the dftProd lemmas to ZModProd and drop import all; credit AffineSampling.lean (#1682) Review fixes for #1695: - the linearity, bijectivity and constant lemmas for ZMod.dftProd, and the Parseval identities for translations and sheared differences, now live in Foundations/Analysis/Fourier/ZModProd.lean; - ShearTranslation.lean's private Parseval helpers are replaced by these public lemmas (the shear ones are the case f = g); - RelativeShearTranslation.lean no longer uses import all; - the module docstring credits OpenAI's AffineSampling.lean at 7ef5c0cc (square_gap with the external permutations u in changeF; the frame lift slice_frame, frame_gap, slice_gap); our proof is independent. Co-Authored-By: Claude Opus 5.5 --- .../Analysis/Fourier/ZModProd.lean | 90 ++++++++++++++- .../Expander/RelativeShearTranslation.lean | 108 +++--------------- .../Expander/ShearTranslation.lean | 41 +------ 3 files changed, 108 insertions(+), 131 deletions(-) diff --git a/Complexity/Foundations/Analysis/Fourier/ZModProd.lean b/Complexity/Foundations/Analysis/Fourier/ZModProd.lean index 11214c9ca..a50ae059e 100644 --- a/Complexity/Foundations/Analysis/Fourier/ZModProd.lean +++ b/Complexity/Foundations/Analysis/Fourier/ZModProd.lean @@ -9,8 +9,9 @@ module public import Complexity.Init public import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar -import Complexity.Foundations.Algebra.Shear +public import Complexity.Foundations.Algebra.Shear import Mathlib.Analysis.Complex.Basic +import Mathlib.LinearAlgebra.FiniteDimensional.Basic import Mathlib.NumberTheory.LegendreSymbol.AddCharacter /-! @@ -38,6 +39,12 @@ multiplies the transform at `ξ` by `e (ξ.1 * t.1 + ξ.2 * t.2)`, and the shear * `ZMod.dftProd_zero`: the transform at the zero frequency is the sum of the values. * `ZMod.dftProd_comp_add`: translation multiplies the transform by a character value. * `ZMod.dftProd_comp_shearFst`, `ZMod.dftProd_comp_shearSnd`: shears permute the frequencies. +* `ZMod.dftProd_add`, `ZMod.dftProd_smul`, `ZMod.dftProd_injective`, `ZMod.dftProd_surjective`: the + transform is a linear bijection. +* `ZMod.dftProd_const_of_ne_zero`: a constant has no nonzero frequencies. +* `ZMod.sum_norm_sq_dftProd_translate`, `ZMod.sum_norm_sq_dftProd_shearFst_sub`, + `ZMod.sum_norm_sq_dftProd_shearSnd_sub`: Parseval's identity for the change along a translation, + and for the difference of two functions, one of them sheared. -/ public section @@ -133,4 +140,85 @@ theorem dftProd_comp_shearSnd (f : ZMod N × ZMod N → ℂ) (k : ZMod N) (ξ : congr 2 ring +/-- The transform is additive. -/ +theorem dftProd_add (f g : ZMod N × ZMod N → ℂ) : dftProd (f + g) = dftProd f + dftProd g := by + ext ξ + simp only [dftProd, Pi.add_apply, mul_add, sum_add_distrib] + +/-- The transform is homogeneous. -/ +theorem dftProd_smul (c : ℂ) (f : ZMod N × ZMod N → ℂ) : dftProd (c • f) = c • dftProd f := by + ext ξ + simp only [dftProd, Pi.smul_apply, smul_eq_mul, mul_sum] + exact sum_congr rfl fun _ _ ↦ by ring + +/-- The transform is injective, by Parseval's identity. -/ +theorem dftProd_injective : Function.Injective (dftProd (N := N)) := by + intro f g h + have hP := sum_norm_sq_dftProd (f - g) + rw [dftProd_sub, h, sub_self] at hP + simp only [Pi.zero_apply, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, + sum_const_zero] at hP + have hN : (N : ℝ) ^ 2 ≠ 0 := pow_ne_zero _ (Nat.cast_ne_zero.2 (NeZero.ne N)) + have h0 := (mul_eq_zero.1 hP.symm).resolve_left hN + rw [sum_eq_zero_iff_of_nonneg fun _ _ ↦ by positivity] at h0 + funext v + simpa [sub_eq_zero] using h0 v (mem_univ v) + +/-- The transform as a linear map. -/ +private noncomputable def dftProdLinearMap : + (ZMod N × ZMod N → ℂ) →ₗ[ℂ] (ZMod N × ZMod N → ℂ) where + toFun := dftProd + map_add' := dftProd_add + map_smul' := dftProd_smul + +/-- The transform is surjective: an injective linear endomorphism of a finite-dimensional space. -/ +theorem dftProd_surjective : Function.Surjective (dftProd (N := N)) := + LinearMap.injective_iff_surjective.1 (show Function.Injective dftProdLinearMap from + dftProd_injective (N := N)) + +/-- **A constant has no nonzero frequencies**: Parseval's identity puts all of its mass at `0`. -/ +theorem dftProd_const_of_ne_zero (c : ℂ) {ξ : ZMod N × ZMod N} (hξ : ξ ≠ 0) : + dftProd (fun _ ↦ c) ξ = 0 := by + have hP := sum_norm_sq_dftProd (N := N) fun _ ↦ c + rw [← add_sum_erase _ _ (mem_univ (0 : ZMod N × ZMod N)), dftProd_zero] at hP + simp only [sum_const, card_univ, Fintype.card_prod, ZMod.card, nsmul_eq_mul, norm_mul, + Complex.norm_natCast, Nat.cast_mul] at hP + have h0 : ∑ ζ ∈ univ.erase (0 : ZMod N × ZMod N), ‖dftProd (fun _ ↦ c) ζ‖ ^ 2 = 0 := by linarith + rw [sum_eq_zero_iff_of_nonneg fun _ _ ↦ by positivity] at h0 + simpa using h0 ξ (mem_erase.2 ⟨hξ, mem_univ ξ⟩) + +/-- **Parseval's identity for the change along a translation**: the transform of the change of +`f` along the translation by `t` is the transform of `f` times `e (ξ.1 * t.1 + ξ.2 * t.2) - 1`. -/ +theorem sum_norm_sq_dftProd_translate (f : ZMod N × ZMod N → ℂ) (t : ZMod N × ZMod N) : + ∑ ξ, ‖stdAddChar (ξ.1 * t.1 + ξ.2 * t.2) - 1‖ ^ 2 * ‖dftProd f ξ‖ ^ 2 = + N ^ 2 * ∑ v, ‖f (v + t) - f v‖ ^ 2 := by + rw [← sum_norm_sq_dftProd (fun v ↦ f (v + t) - f v)] + refine sum_congr rfl fun ξ _ ↦ ?_ + have : (fun v ↦ f (v + t) - f v) = (fun v ↦ f (v + t)) - f := rfl + rw [this, dftProd_sub, Pi.sub_apply, dftProd_comp_add, ← sub_one_mul, norm_mul, mul_pow] + +/-- **Parseval's identity for the difference of two functions along the shear** +`(x, y) ↦ (x + k * y, y)`: it acts on the frequencies by the dual shear `(a, b) ↦ (a, b - k * a)`. +-/ +theorem sum_norm_sq_dftProd_shearFst_sub (f g : ZMod N × ZMod N → ℂ) (k : ZMod N) : + ∑ ξ, ‖dftProd f (Cslib.shearSnd (-k) ξ) - dftProd g ξ‖ ^ 2 = + N ^ 2 * ∑ v, ‖f (Cslib.shearFst k v) - g v‖ ^ 2 := by + rw [← sum_norm_sq_dftProd (fun v ↦ f (Cslib.shearFst k v) - g v)] + refine sum_congr rfl fun ξ _ ↦ ?_ + have : (fun v ↦ f (Cslib.shearFst k v) - g v) = (fun v ↦ f (v.1 + k * v.2, v.2)) - g := rfl + rw [this, dftProd_sub, Pi.sub_apply, dftProd_comp_shearFst, Cslib.shearSnd_apply, neg_mul, + ← sub_eq_add_neg] + +/-- **Parseval's identity for the difference of two functions along the shear** +`(x, y) ↦ (x, y + k * x)`: it acts on the frequencies by the dual shear `(a, b) ↦ (a - k * b, b)`. +-/ +theorem sum_norm_sq_dftProd_shearSnd_sub (f g : ZMod N × ZMod N → ℂ) (k : ZMod N) : + ∑ ξ, ‖dftProd f (Cslib.shearFst (-k) ξ) - dftProd g ξ‖ ^ 2 = + N ^ 2 * ∑ v, ‖f (Cslib.shearSnd k v) - g v‖ ^ 2 := by + rw [← sum_norm_sq_dftProd (fun v ↦ f (Cslib.shearSnd k v) - g v)] + refine sum_congr rfl fun ξ _ ↦ ?_ + have : (fun v ↦ f (Cslib.shearSnd k v) - g v) = (fun v ↦ f (v.1, v.2 + k * v.1)) - g := rfl + rw [this, dftProd_sub, Pi.sub_apply, dftProd_comp_shearSnd, Cslib.shearFst_apply, neg_mul, + ← sub_eq_add_neg] + end ZMod diff --git a/Complexity/Foundations/Combinatorics/Expander/RelativeShearTranslation.lean b/Complexity/Foundations/Combinatorics/Expander/RelativeShearTranslation.lean index d96c0046b..700aad5c7 100644 --- a/Complexity/Foundations/Combinatorics/Expander/RelativeShearTranslation.lean +++ b/Complexity/Foundations/Combinatorics/Expander/RelativeShearTranslation.lean @@ -11,11 +11,6 @@ public import Complexity.Foundations.Analysis.Fourier.ZModProd public import Complexity.Foundations.Algebra.Shear public import Complexity.Foundations.Combinatorics.Expander.ShearTranslation public import Mathlib.Analysis.InnerProductSpace.PiL2 --- `import all`: the linearity of `ZMod.dftProd` unfolds its body, and the frequency-side --- inequality reuses the private Parseval identity for translations, `sum_norm_sq_translate`. -import all Complexity.Foundations.Analysis.Fourier.ZModProd -import all Complexity.Foundations.Combinatorics.Expander.ShearTranslation -import Mathlib.LinearAlgebra.FiniteDimensional.Basic /-! # The relative Poincaré inequality for shears and translations @@ -44,10 +39,15 @@ this norm, and the reverse triangle inequality bounds the changes of `Φ` by tho This is the step that turns the uniform gap on `ZMod n × ZMod n` into closeness to the vectors fixed by the translations of one coordinate pair, as in the projection argument of the OpenAI preprint on derandomizing logarithmic space for its affine walks -[OpenAI, proof of Lemma 6.1][OpenAI2026LogSpace]. The preprint takes it from Shalom's quantitative -relative property (T) of `(SL₂(ℤ) ⋉ ℤ², ℤ²)`; see also [Burger][Burger1991]. The elementary route -through the uniform Fourier gap is credited in the module of `Cslib.RotationMap.shearTranslation`. -The statements and proofs here are ours. +[OpenAI, proof of Lemma 6.1][OpenAI2026LogSpace]. The preprint's text takes it from Shalom's +quantitative relative property (T) of `(SL₂(ℤ) ⋉ ℤ², ℤ²)`; see also [Burger][Burger1991]. An +elementary version with external permutations of a spectator, built on a uniform Fourier gap, is +in OpenAI's Lean development, the file +[`AffineSampling.lean`](https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/lean/OAI/Computability/Logspace/AffineSampling.lean) +at revision `7ef5c0cc`: `ExactDerandomization.Analysis.Square.square_gap`, with the external +permutations `u` in `changeF`. The same file lifts it to frames (`slice_frame`, `frame_gap`, +`slice_gap`). The statements and the proof here are independent of that code, which was not +consulted: they are derived from `sum_norm_sq_le_shearTranslation`. ## Main definitions @@ -56,11 +56,6 @@ The statements and proofs here are ours. ## Main results -* `ZMod.dftProd_add`, `ZMod.dftProd_smul`: the transform is linear. -* `ZMod.dftProd_injective`, `ZMod.dftProd_surjective`: the transform is a bijection. -* `ZMod.sum_norm_sq_dftProd_shearFst_sub`, `ZMod.sum_norm_sq_dftProd_shearSnd_sub`: Parseval's - identity for the difference of two functions, one of them sheared. -* `ZMod.dftProd_const_of_ne_zero`: a constant has no nonzero frequencies. * `Cslib.RotationMap.sum_norm_sq_le_dual_shearTranslation`: the Poincaré inequality on the frequencies. * `Cslib.RotationMap.sum_norm_sq_sub_fiber_le_twistedShearTranslation`, @@ -78,83 +73,6 @@ public section open Finset open scoped BigOperators -namespace ZMod - -variable {N : ℕ} [NeZero N] - -/-- The transform is additive. -/ -theorem dftProd_add (f g : ZMod N × ZMod N → ℂ) : dftProd (f + g) = dftProd f + dftProd g := by - ext ξ - simp only [dftProd, Pi.add_apply, mul_add, sum_add_distrib] - -/-- The transform is homogeneous. -/ -theorem dftProd_smul (c : ℂ) (f : ZMod N × ZMod N → ℂ) : dftProd (c • f) = c • dftProd f := by - ext ξ - simp only [dftProd, Pi.smul_apply, smul_eq_mul, mul_sum] - exact sum_congr rfl fun _ _ ↦ by ring - -/-- The transform is injective, by Parseval's identity. -/ -theorem dftProd_injective : Function.Injective (dftProd (N := N)) := by - intro f g h - have hP := sum_norm_sq_dftProd (f - g) - rw [dftProd_sub, h, sub_self] at hP - simp only [Pi.zero_apply, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, - sum_const_zero] at hP - have hN : (N : ℝ) ^ 2 ≠ 0 := pow_ne_zero _ (Nat.cast_ne_zero.2 (NeZero.ne N)) - have h0 := (mul_eq_zero.1 hP.symm).resolve_left hN - rw [sum_eq_zero_iff_of_nonneg fun _ _ ↦ by positivity] at h0 - funext v - simpa [sub_eq_zero] using h0 v (mem_univ v) - -/-- The transform as a linear map. -/ -private noncomputable def dftProdLinearMap : - (ZMod N × ZMod N → ℂ) →ₗ[ℂ] (ZMod N × ZMod N → ℂ) where - toFun := dftProd - map_add' := dftProd_add - map_smul' := dftProd_smul - -/-- The transform is surjective: an injective linear endomorphism of a finite-dimensional space. -/ -theorem dftProd_surjective : Function.Surjective (dftProd (N := N)) := - LinearMap.injective_iff_surjective.1 (show Function.Injective dftProdLinearMap from - dftProd_injective (N := N)) - -/-- **A constant has no nonzero frequencies**: Parseval's identity puts all of its mass at `0`. -/ -theorem dftProd_const_of_ne_zero (c : ℂ) {ξ : ZMod N × ZMod N} (hξ : ξ ≠ 0) : - dftProd (fun _ ↦ c) ξ = 0 := by - have hP := sum_norm_sq_dftProd (N := N) fun _ ↦ c - rw [← add_sum_erase _ _ (mem_univ (0 : ZMod N × ZMod N)), dftProd_zero] at hP - simp only [sum_const, card_univ, Fintype.card_prod, ZMod.card, nsmul_eq_mul, norm_mul, - Complex.norm_natCast, Nat.cast_mul] at hP - have h0 : ∑ ζ ∈ univ.erase (0 : ZMod N × ZMod N), ‖dftProd (fun _ ↦ c) ζ‖ ^ 2 = 0 := by linarith - rw [sum_eq_zero_iff_of_nonneg fun _ _ ↦ by positivity] at h0 - simpa using h0 ξ (mem_erase.2 ⟨hξ, mem_univ ξ⟩) - -/-- **Parseval's identity for the difference of two functions along the shear** -`(x, y) ↦ (x + k * y, y)`: it acts on the frequencies by the dual shear `(a, b) ↦ (a, b - k * a)`. --/ -theorem sum_norm_sq_dftProd_shearFst_sub (f g : ZMod N × ZMod N → ℂ) (k : ZMod N) : - ∑ ξ, ‖dftProd f (Cslib.shearSnd (-k) ξ) - dftProd g ξ‖ ^ 2 = - N ^ 2 * ∑ v, ‖f (Cslib.shearFst k v) - g v‖ ^ 2 := by - rw [← sum_norm_sq_dftProd (fun v ↦ f (Cslib.shearFst k v) - g v)] - refine sum_congr rfl fun ξ _ ↦ ?_ - have : (fun v ↦ f (Cslib.shearFst k v) - g v) = (fun v ↦ f (v.1 + k * v.2, v.2)) - g := rfl - rw [this, dftProd_sub, Pi.sub_apply, dftProd_comp_shearFst, Cslib.shearSnd_apply, neg_mul, - ← sub_eq_add_neg] - -/-- **Parseval's identity for the difference of two functions along the shear** -`(x, y) ↦ (x, y + k * x)`: it acts on the frequencies by the dual shear `(a, b) ↦ (a - k * b, b)`. --/ -theorem sum_norm_sq_dftProd_shearSnd_sub (f g : ZMod N × ZMod N → ℂ) (k : ZMod N) : - ∑ ξ, ‖dftProd f (Cslib.shearFst (-k) ξ) - dftProd g ξ‖ ^ 2 = - N ^ 2 * ∑ v, ‖f (Cslib.shearSnd k v) - g v‖ ^ 2 := by - rw [← sum_norm_sq_dftProd (fun v ↦ f (Cslib.shearSnd k v) - g v)] - refine sum_congr rfl fun ξ _ ↦ ?_ - have : (fun v ↦ f (Cslib.shearSnd k v) - g v) = (fun v ↦ f (v.1, v.2 + k * v.1)) - g := rfl - rw [this, dftProd_sub, Pi.sub_apply, dftProd_comp_shearSnd, Cslib.shearFst_apply, neg_mul, - ← sub_eq_add_neg] - -end ZMod - namespace Cslib.RotationMap variable {n : ℕ} [NeZero n] @@ -176,8 +94,8 @@ theorem sum_norm_sq_le_dual_shearTranslation (Φ : ZMod n × ZMod n → ℂ) (h0 Equiv.coe_addRight] at hP have e₁ := ZMod.sum_norm_sq_dftProd_shearFst_sub f f 1 have e₂ := ZMod.sum_norm_sq_dftProd_shearSnd_sub f f 1 - have e₃ := sum_norm_sq_translate f (1, 0) - have e₄ := sum_norm_sq_translate f (0, 1) + have e₃ := ZMod.sum_norm_sq_dftProd_translate f (1, 0) + have e₄ := ZMod.sum_norm_sq_dftProd_translate f (0, 1) simp only [mul_one, mul_zero, add_zero, zero_add] at e₃ e₄ have hM := ZMod.sum_norm_sq_dftProd f have hn : (0 : ℝ) ≤ (n : ℝ) ^ 2 := by positivity @@ -315,7 +233,7 @@ theorem sum_norm_sq_sub_fiber_le_twistedShearTranslation (π₁ π₂ : Equiv.Pe refine (hweight _ fun _ ↦ by positivity).trans_eq ?_ rw [Fintype.sum_prod_type, mul_sum] refine sum_congr rfl fun x _ ↦ ?_ - have := sum_norm_sq_translate (fun w ↦ f (x, w)) (1, 0) + have := ZMod.sum_norm_sq_dftProd_translate (fun w ↦ f (x, w)) (1, 0) simp only [mul_one, mul_zero, add_zero] at this exact this have hT₂ : ∑ ξ, ‖ZMod.stdAddChar ξ.2 - 1‖ ^ 2 * ‖(ψ ξ : ℂ)‖ ^ 2 ≤ @@ -323,7 +241,7 @@ theorem sum_norm_sq_sub_fiber_le_twistedShearTranslation (π₁ π₂ : Equiv.Pe refine (hweight _ fun _ ↦ by positivity).trans_eq ?_ rw [Fintype.sum_prod_type, mul_sum] refine sum_congr rfl fun x _ ↦ ?_ - have := sum_norm_sq_translate (fun w ↦ f (x, w)) (0, 1) + have := ZMod.sum_norm_sq_dftProd_translate (fun w ↦ f (x, w)) (0, 1) simp only [mul_one, mul_zero, zero_add] at this exact this refine le_of_mul_le_mul_left ?_ hn diff --git a/Complexity/Foundations/Combinatorics/Expander/ShearTranslation.lean b/Complexity/Foundations/Combinatorics/Expander/ShearTranslation.lean index 3efde6834..17e725f07 100644 --- a/Complexity/Foundations/Combinatorics/Expander/ShearTranslation.lean +++ b/Complexity/Foundations/Combinatorics/Expander/ShearTranslation.lean @@ -482,36 +482,6 @@ section Gap variable {n : ℕ} [NeZero n] -/-- Parseval's identity for the change of `f` along a translation. -/ -private theorem sum_norm_sq_translate (f : ZMod n × ZMod n → ℂ) (t : ZMod n × ZMod n) : - ∑ ξ, ‖ZMod.stdAddChar (ξ.1 * t.1 + ξ.2 * t.2) - 1‖ ^ 2 * ‖ZMod.dftProd f ξ‖ ^ 2 = - n ^ 2 * ∑ v, ‖f (v + t) - f v‖ ^ 2 := by - rw [← ZMod.sum_norm_sq_dftProd (fun v ↦ f (v + t) - f v)] - refine sum_congr rfl fun ξ _ ↦ ?_ - have : (fun v ↦ f (v + t) - f v) = (fun v ↦ f (v + t)) - f := rfl - rw [this, ZMod.dftProd_sub, Pi.sub_apply, ZMod.dftProd_comp_add, ← sub_one_mul, norm_mul, - mul_pow] - -/-- Parseval's identity for the change of `f` along the shear `(x, y) ↦ (x + k * y, y)`. -/ -private theorem sum_norm_sq_shearFst (f : ZMod n × ZMod n → ℂ) (k : ZMod n) : - ∑ ξ, ‖ZMod.dftProd f (shearSnd (-k) ξ) - ZMod.dftProd f ξ‖ ^ 2 = - n ^ 2 * ∑ v, ‖f (shearFst k v) - f v‖ ^ 2 := by - rw [← ZMod.sum_norm_sq_dftProd (fun v ↦ f (shearFst k v) - f v)] - refine sum_congr rfl fun ξ _ ↦ ?_ - have : (fun v ↦ f (shearFst k v) - f v) = (fun v ↦ f (v.1 + k * v.2, v.2)) - f := rfl - rw [this, ZMod.dftProd_sub, Pi.sub_apply, ZMod.dftProd_comp_shearFst, shearSnd_apply, neg_mul, - ← sub_eq_add_neg] - -/-- Parseval's identity for the change of `f` along the shear `(x, y) ↦ (x, y + k * x)`. -/ -private theorem sum_norm_sq_shearSnd (f : ZMod n × ZMod n → ℂ) (k : ZMod n) : - ∑ ξ, ‖ZMod.dftProd f (shearFst (-k) ξ) - ZMod.dftProd f ξ‖ ^ 2 = - n ^ 2 * ∑ v, ‖f (shearSnd k v) - f v‖ ^ 2 := by - rw [← ZMod.sum_norm_sq_dftProd (fun v ↦ f (shearSnd k v) - f v)] - refine sum_congr rfl fun ξ _ ↦ ?_ - have : (fun v ↦ f (shearSnd k v) - f v) = (fun v ↦ f (v.1, v.2 + k * v.1)) - f := rfl - rw [this, ZMod.dftProd_sub, Pi.sub_apply, ZMod.dftProd_comp_shearSnd, shearFst_apply, neg_mul, - ← sub_eq_add_neg] - /-- The change along the shears by `4` and `-4` is at most `16` times that along the unit shear. -/ private theorem sum_norm_sq_shearFst_four_le (f : ZMod n × ZMod n → ℂ) : @@ -562,7 +532,8 @@ theorem sum_norm_sq_le_shearTranslation (f : ZMod n × ZMod n → ℂ) (hf : ∑ sq_nonneg ‖ZMod.stdAddChar ξ.2 - 1‖] · linarith [one_div_eight_le_norm_stdAddChar_sub_one (not_le.1 hs), sq_nonneg ‖ZMod.stdAddChar ξ.1 - 1‖] - rw [← sum_norm_sq_translate, ← sum_norm_sq_translate, ← sum_add_distrib, mul_sum, sum_filter] + rw [← ZMod.sum_norm_sq_dftProd_translate, ← ZMod.sum_norm_sq_dftProd_translate, + ← sum_add_distrib, mul_sum, sum_filter] refine sum_le_sum fun ξ _ ↦ ?_ have e₁ : ξ.1 * ((1, 0) : ZMod n × ZMod n).1 + ξ.2 * ((1, 0) : ZMod n × ZMod n).2 = ξ.1 := by simp @@ -574,10 +545,10 @@ theorem sum_norm_sq_le_shearTranslation (f : ZMod n × ZMod n → ℂ) (hf : ∑ · have := mul_le_mul_of_nonneg_right (hw ξ hs) (sq_nonneg ‖F ξ‖) linarith -- The dual shears are paid for by the primal shears. - have hD₁ := sum_norm_sq_shearFst f (-4 : ZMod n) - have hD₂ := sum_norm_sq_shearFst f (4 : ZMod n) - have hD₃ := sum_norm_sq_shearSnd f (-4 : ZMod n) - have hD₄ := sum_norm_sq_shearSnd f (4 : ZMod n) + have hD₁ := ZMod.sum_norm_sq_dftProd_shearFst_sub f f (-4 : ZMod n) + have hD₂ := ZMod.sum_norm_sq_dftProd_shearFst_sub f f (4 : ZMod n) + have hD₃ := ZMod.sum_norm_sq_dftProd_shearSnd_sub f f (-4 : ZMod n) + have hD₄ := ZMod.sum_norm_sq_dftProd_shearSnd_sub f f (4 : ZMod n) rw [neg_neg] at hD₁ hD₃ rw [← hF] at hD₁ hD₂ hD₃ hD₄ have e₁ := sum_norm_sq_shearFst_four_le f From 073614394dee338a170f8e56eba57ad2cc557770 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Fri, 30 Oct 2026 01:15:49 +0000 Subject: [PATCH 6/7] =?UTF-8?q?feat(Expander):=20Efron=E2=80=93Stein=20and?= =?UTF-8?q?=20the=20pair-move=20bound=20on=20Y=20=C3=97=20(Fin=20H=20?= =?UTF-8?q?=E2=86=92=20ZMod=20L)=20(#1682)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Step (B) of the frame-lifted gap plan on #1682: - Fintype.expect_sq_sub_expect_le_sum_expect_sq_sub_update: the Efron–Stein inequality for a uniform tuple with a spectator; - Fintype.expect_sq_sub_expect_update_le: the average over one coordinate is the best approximation by functions not depending on it; - pairShearTranslationMove and expect_sq_sub_expect_le_pairShearTranslation: the second moment of f about its average over w is at most 512 times the sum over i of the Dirichlet form of the elementary shears and unit translations of the pair (i, σ i), using the relative Poincaré inequality of #1695 per pair. Co-Authored-By: Claude Opus 5.5 --- Complexity.lean | 2 + .../Expander/PairShearTranslation.lean | 167 ++++++++++++++++++ .../Foundations/Probability/EfronStein.lean | 141 +++++++++++++++ ComplexityTests/PairShearTranslation.lean | 52 ++++++ 4 files changed, 362 insertions(+) create mode 100644 Complexity/Foundations/Combinatorics/Expander/PairShearTranslation.lean create mode 100644 Complexity/Foundations/Probability/EfronStein.lean create mode 100644 ComplexityTests/PairShearTranslation.lean diff --git a/Complexity.lean b/Complexity.lean index e2466576e..19a2904f6 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2369,6 +2369,7 @@ public import Complexity.Foundations.Combinatorics.Expander.Loops public import Complexity.Foundations.Combinatorics.Expander.LowerBound public import Complexity.Foundations.Combinatorics.Expander.Mixing public import Complexity.Foundations.Combinatorics.Expander.Multigraph +public import Complexity.Foundations.Combinatorics.Expander.PairShearTranslation public import Complexity.Foundations.Combinatorics.Expander.Perm public import Complexity.Foundations.Combinatorics.Expander.Power public import Complexity.Foundations.Combinatorics.Expander.Random @@ -2651,6 +2652,7 @@ public import Complexity.Foundations.NumberTheory.SqrtPrimeWindow public import Complexity.Foundations.Order.BooleanSubalgebra public import Complexity.Foundations.Order.Changes public import Complexity.Foundations.Order.UpperLower +public import Complexity.Foundations.Probability.EfronStein public import Complexity.Foundations.Probability.Gaussian.Multivariate public import Complexity.Foundations.Probability.Gaussian.Real public import Complexity.Foundations.Probability.Gaussian.Sheppard diff --git a/Complexity/Foundations/Combinatorics/Expander/PairShearTranslation.lean b/Complexity/Foundations/Combinatorics/Expander/PairShearTranslation.lean new file mode 100644 index 000000000..0ab4b088a --- /dev/null +++ b/Complexity/Foundations/Combinatorics/Expander/PairShearTranslation.lean @@ -0,0 +1,167 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Combinatorics.Expander.RelativeShearTranslation +import Complexity.Foundations.Probability.EfronStein + +/-! +# Shears and translations of coordinate pairs + +Let `Y` be a finite set and consider functions on `Y × (Fin H → ZMod L)`. For a pair `i ≠ j` of +coordinates, the elementary moves are (`pairShearTranslationMove`): the elementary shears +`w ↦ w + w j • e i` and `w ↦ w + w i • e j`, which also act on `Y` by given permutations `ρ`, `ρ'`, +and the unit translations `w ↦ w + e i` and `w ↦ w + e j`. These are the moves of the elementary +matrices of `SL_H(ℤ)` and of the unit translations on a retention slice `Frame P H r × (ZMod L)^H`, +where `ρ` is the action of the same elementary matrix on the frames. + +The second moment of `f` about its average over the whole tuple `w` is at most `512` times the sum, +over the coordinates `i`, of the total squared change of `f` along the moves of a pair `(i, σ i)` +with `σ i ≠ i` (`expect_sq_sub_expect_le_pairShearTranslation`). The proof combines: + +* the Efron–Stein inequality (`Fintype.expect_sq_sub_expect_le_sum_expect_sq_sub_update`), which + reduces the distance from the functions of `y` alone to the distances from the functions not + depending on one coordinate `w i`; +* the best-approximation property of the average over `w i` + (`Fintype.expect_sq_sub_expect_update_le`), which bounds that distance by the distance from the + average over the pair `(w i, w j)`; +* the relative Poincaré inequality with a spectator + (`expect_sq_sub_expect_fiber_le_twistedShearTranslation`), applied to `f` with the pair + `(w i, w j)` resampled and everything else as the spectator + (`expect_sq_sub_expect_update_le_pairShearTranslation`). + +This is the step from the coordinate-pair projections `P_ij` to the projection onto the vectors +fixed by all translations in the OpenAI preprint on derandomizing logarithmic space +[OpenAI, proof of Lemma 6.1][OpenAI2026LogSpace], where the commuting projections are telescoped; +here the Efron–Stein inequality takes the place of the telescoping. The elementary lift of the +relative gap to frames is in OpenAI's Lean development, the file +[`AffineSampling.lean`](https://github.com/openai/math/blob/7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a/lean/OAI/Computability/Logspace/AffineSampling.lean) +at revision `7ef5c0cc` (`slice_frame`, `frame_gap`, `slice_gap`). The statements and the proof here +are independent of that code, which was not consulted. + +## Main definitions + +* `Cslib.RotationMap.pairShearTranslationMove`: the four moves of a coordinate pair. + +## Main results + +* `Cslib.RotationMap.expect_sq_sub_expect_update_le_pairShearTranslation`: one coordinate, from + the moves of a pair containing it. +* `Cslib.RotationMap.expect_sq_sub_expect_le_pairShearTranslation`: all coordinates. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace] +-/ + +public section + +open Finset Function +open scoped BigOperators + +namespace Cslib.RotationMap + +variable {Y : Type*} [Fintype Y] {H L : ℕ} + +/-- The four moves of the coordinate pair `(i, j)` on `Y × (Fin H → ZMod L)`: the elementary +shears `w ↦ w + w j • e i` (with `ρ` on `Y`) and `w ↦ w + w i • e j` (with `ρ'` on `Y`), and the +unit translations `w ↦ w + e i` and `w ↦ w + e j`. -/ +@[expose] +def pairShearTranslationMove (ρ ρ' : Equiv.Perm Y) (i j : Fin H) : + Fin 4 → Y × (Fin H → ZMod L) → Y × (Fin H → ZMod L) := + ![fun p ↦ (ρ p.1, update p.2 i (p.2 i + p.2 j)), fun p ↦ (ρ' p.1, update p.2 j (p.2 j + p.2 i)), + fun p ↦ (p.1, update p.2 i (p.2 i + 1)), fun p ↦ (p.1, update p.2 j (p.2 j + 1))] + +/-- Overwriting the coordinates `i` and then `j` of `w`. -/ +private abbrev upd2 (i j : Fin H) (w : Fin H → ZMod L) (a b : ZMod L) : Fin H → ZMod L := + update (update w i a) j b + +omit [Fintype Y] in +private theorem upd2_upd2 (i j : Fin H) (w : Fin H → ZMod L) (a b a' b' : ZMod L) : + upd2 i j (upd2 i j w a b) a' b' = upd2 i j w a' b' := by + funext k + simp only [upd2, update_apply] + split_ifs <;> simp_all + +omit [Fintype Y] in +private theorem update_upd2_fst {i j : Fin H} (hij : i ≠ j) (w : Fin H → ZMod L) (a b c : ZMod L) : + update (upd2 i j w a b) i c = upd2 i j w c b := by + funext k + simp only [upd2, update_apply] + split_ifs <;> simp_all + +omit [Fintype Y] in +private theorem upd2_apply_fst {i j : Fin H} (hij : i ≠ j) (w : Fin H → ZMod L) (a b : ZMod L) : + upd2 i j w a b i = a := by + simp [upd2, hij] + +variable [NeZero L] + +/-- Resampling the pair `(i, j)` of a uniformly random tuple keeps it uniformly random. -/ +private theorem expect_upd2 (i j : Fin H) (Φ : Y × (Fin H → ZMod L) → ℝ) : + 𝔼 q : (Y × (Fin H → ZMod L)) × (ZMod L × ZMod L), Φ (q.1.1, upd2 i j q.1.2 q.2.1 q.2.2) = + 𝔼 p, Φ p := by + rw [Fintype.expect_prod_type, Fintype.expect_prod_type, Fintype.expect_prod_type] + refine expect_congr rfl fun y _ ↦ ?_ + simp only [Fintype.expect_prod_type, upd2] + rw [Fintype.expect_expect_update (fun s ↦ 𝔼 b, Φ (y, update s j b)) i, + Fintype.expect_expect_update (fun s ↦ Φ (y, s)) j] + +/-- **One coordinate, from the moves of a pair containing it**: the second moment of `f` about its +average over `w i` is at most `512` times the total squared change of `f` along the four moves of +the pair `(i, j)`, for `i ≠ j`. -/ +theorem expect_sq_sub_expect_update_le_pairShearTranslation (ρ ρ' : Equiv.Perm Y) {i j : Fin H} + (hij : i ≠ j) (f : Y × (Fin H → ZMod L) → ℝ) : + 𝔼 p, (f p - 𝔼 a, f (p.1, update p.2 i a)) ^ 2 ≤ + 512 * ∑ k, 𝔼 p, (f (pairShearTranslationMove ρ ρ' i j k p) - f p) ^ 2 := by + -- The average over the pair `(w i, w j)`. + set G : Y × (Fin H → ZMod L) → ℝ := fun p ↦ 𝔼 a, 𝔼 b, f (p.1, upd2 i j p.2 a b) with hG + have hGinv (p : Y × (Fin H → ZMod L)) (a b : ZMod L) : G (p.1, upd2 i j p.2 a b) = G p := by + simp only [hG, upd2_upd2] + refine (Fintype.expect_sq_sub_expect_update_le i f G fun p c ↦ ?_).trans ?_ + · have := hGinv p c (update p.2 i c j) + simpa only [upd2, update_eq_self] using this + -- The relative Poincaré inequality, with everything but the pair as the spectator. + set F : (Y × (Fin H → ZMod L)) × (ZMod L × ZMod L) → ℝ := + fun q ↦ f (q.1.1, upd2 i j q.1.2 q.2.1 q.2.2) with hF + have hA := expect_sq_sub_expect_fiber_le_twistedShearTranslation + (ρ.prodCongr (Equiv.refl _)) (ρ'.prodCongr (Equiv.refl _)) F + have hL : 𝔼 q, (F q - 𝔼 v, F (q.1, v)) ^ 2 = 𝔼 p, (f p - G p) ^ 2 := by + rw [← expect_upd2 i j fun p ↦ (f p - G p) ^ 2] + refine expect_congr rfl fun q _ ↦ ?_ + rw [hGinv] + simp only [hF, hG, Fintype.expect_prod_type] + have hR (k : Fin 4) : 𝔼 q, (F (twistedShearTranslationMove (ρ.prodCongr (Equiv.refl _)) + (ρ'.prodCongr (Equiv.refl _)) L k q) - F q) ^ 2 = + 𝔼 p, (f (pairShearTranslationMove ρ ρ' i j k p) - f p) ^ 2 := by + rw [← expect_upd2 i j fun p ↦ (f (pairShearTranslationMove ρ ρ' i j k p) - f p) ^ 2] + refine expect_congr rfl fun q _ ↦ ?_ + obtain ⟨⟨y, w⟩, a, b⟩ := q + fin_cases k <;> + simp [hF, twistedShearTranslationMove, pairShearTranslationMove, shearFst_apply, + shearSnd_apply, upd2_apply_fst hij, update_upd2_fst hij, upd2] + rw [hL] at hA + refine hA.trans_eq ?_ + simp only [hR] + +/-- **All coordinates, from the moves of coordinate pairs**: if `σ i ≠ i` for every coordinate `i`, +the second moment of `f` about its average over the whole tuple is at most `512` times the sum over +`i` of the total squared change of `f` along the four moves of the pair `(i, σ i)`, where `ρ i j` +acts on `Y` with the shear `w ↦ w + w j • e i`. -/ +theorem expect_sq_sub_expect_le_pairShearTranslation {Y : Type} [Fintype Y] + (ρ : Fin H → Fin H → Equiv.Perm Y) (σ : Fin H → Fin H) (hσ : ∀ i, σ i ≠ i) + (f : Y × (Fin H → ZMod L) → ℝ) : + 𝔼 p, (f p - 𝔼 w, f (p.1, w)) ^ 2 ≤ + 512 * ∑ i, ∑ k, 𝔼 p, + (f (pairShearTranslationMove (ρ i (σ i)) (ρ (σ i) i) i (σ i) k p) - f p) ^ 2 := by + refine (Fintype.expect_sq_sub_expect_le_sum_expect_sq_sub_update f).trans ?_ + rw [mul_sum] + exact sum_le_sum fun i _ ↦ + expect_sq_sub_expect_update_le_pairShearTranslation _ _ (hσ i).symm f + +end Cslib.RotationMap diff --git a/Complexity/Foundations/Probability/EfronStein.lean b/Complexity/Foundations/Probability/EfronStein.lean new file mode 100644 index 000000000..05b114c4a --- /dev/null +++ b/Complexity/Foundations/Probability/EfronStein.lean @@ -0,0 +1,141 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Data.Finset.Expect +import Mathlib.Algebra.BigOperators.Fin +import Mathlib.Algebra.Order.BigOperators.Expect +import Mathlib.Data.Fin.Tuple.Basic + +/-! +# The Efron–Stein inequality for uniform averages + +For a function `f` of a spectator `y` and of a uniformly random tuple `w : Fin n → A`, the second +moment of `f` about its average over `w` is at most the sum, over the coordinates `i`, of the second +moments of `f` about its averages over the single coordinate `w i` +(`Fintype.expect_sq_sub_expect_le_sum_expect_sq_sub_update`): +`𝔼 (f - 𝔼_w f)² ≤ ∑ i, 𝔼 (f - 𝔼_{w i} f)²`. This is the Efron–Stein inequality for the uniform +product measure, with the spectator as an extra fixed coordinate. It reduces the distance of `f` +from the functions of `y` alone to its distances from the functions not depending on one coordinate +at a time. + +The proof is by induction on `n`: split `w = Fin.cons a r`, decompose orthogonally over the fibers +of `(y, a)`, apply the induction hypothesis with the spectator `(y, a)` to the part of average zero +on these fibers, and bound the fiber averages by Jensen's inequality. + +## Main results + +* `Fintype.expect_sq_sub_expect_le_sum_expect_sq_sub_update`: the Efron–Stein inequality. +* `Fintype.expect_sq_sub_expect_update_le`: the average over one coordinate is the best + approximation by functions not depending on it. +-/ + +public section + +open Finset Function +open scoped BigOperators + +namespace Fintype + +/-- The second moment about a constant is the second moment about the average plus the squared +distance of the average from the constant. -/ +private theorem expect_sub_sq_eq {R : Type*} [Fintype R] [Nonempty R] (X : R → ℝ) (c : ℝ) : + 𝔼 r, (X r - c) ^ 2 = 𝔼 r, (X r - 𝔼 s, X s) ^ 2 + (𝔼 s, X s - c) ^ 2 := by + set m := 𝔼 s, X s + have h : 𝔼 r, (X r - m) = 0 := by rw [expect_sub_distrib, Fintype.expect_const, sub_self] + calc 𝔼 r, (X r - c) ^ 2 = 𝔼 r, ((X r - m) ^ 2 + 2 * (m - c) * (X r - m) + (m - c) ^ 2) := + expect_congr rfl fun r _ ↦ by ring + _ = _ := by rw [expect_add_distrib, expect_add_distrib, ← mul_expect, h, mul_zero, add_zero, + Fintype.expect_const] + +/-- **The average over one coordinate is the best approximation** by functions not depending on +that coordinate: if `G` does not change when `w i` is resampled, then the second moment of `f` about +its average over `w i` is at most the second moment of `f - G`. -/ +theorem expect_sq_sub_expect_update_le {ι Y A : Type*} [Fintype ι] [DecidableEq ι] [Fintype Y] + [Fintype A] [Nonempty A] (i : ι) (f G : Y × (ι → A) → ℝ) + (hG : ∀ p c, G (p.1, update p.2 i c) = G p) : + 𝔼 p, (f p - 𝔼 a, f (p.1, update p.2 i a)) ^ 2 ≤ 𝔼 p, (f p - G p) ^ 2 := by + set R : Y × (ι → A) → ℝ := fun p ↦ 𝔼 a, f (p.1, update p.2 i a) with hR + -- The part of `f` of average zero over `w i` is orthogonal to the functions not depending on it. + have horth : 𝔼 p, (f p - R p) * (R p - G p) = 0 := by + rw [Fintype.expect_prod_type] + refine expect_eq_zero fun y _ ↦ ?_ + rw [← Fintype.expect_expect_update _ i] + refine expect_eq_zero fun w _ ↦ ?_ + have h2 (a : A) : G (y, update w i a) = G (y, w) := hG (y, w) a + simp only [hR, update_idem, h2] + rw [← expect_mul, expect_sub_distrib, Fintype.expect_const, sub_self, zero_mul] + calc 𝔼 p, (f p - R p) ^ 2 ≤ 𝔼 p, ((f p - R p) ^ 2 + 2 * ((f p - R p) * (R p - G p)) + + (R p - G p) ^ 2) := by + rw [expect_add_distrib, expect_add_distrib, ← mul_expect, horth, mul_zero, add_zero] + exact le_add_of_nonneg_right (expect_nonneg fun _ _ ↦ sq_nonneg _) + _ = 𝔼 p, (f p - G p) ^ 2 := expect_congr rfl fun p _ ↦ by ring + +universe u + +variable {A : Type u} [Fintype A] [Nonempty A] + +/-- **The Efron–Stein inequality** for a uniformly random tuple `w : Fin n → A` and a spectator +`y`: the second moment of `f` about its average over `w` is at most the sum over the coordinates +`i` of the second moments of `f` about its averages over `w i`. The spectator lives in the +universe of `A`, so that the induction can absorb coordinates into it. -/ +theorem expect_sq_sub_expect_le_sum_expect_sq_sub_update {n : ℕ} {Y : Type u} [Fintype Y] + (f : Y × (Fin n → A) → ℝ) : + 𝔼 p, (f p - 𝔼 w, f (p.1, w)) ^ 2 ≤ ∑ i, 𝔼 p, (f p - 𝔼 a, f (p.1, update p.2 i a)) ^ 2 := by + induction n generalizing Y with + | zero => + have h (p : Y × (Fin 0 → A)) : f p - 𝔼 w, f (p.1, w) = 0 := by + rw [Fintype.expect_unique, sub_eq_zero] + exact congrArg f (Prod.ext rfl (Subsingleton.elim _ _)) + simp only [h] + simp + | succ n ih => + -- Split the tuple into its head `a` and tail `r`. + have hsplit (G : Y × (Fin (n + 1) → A) → ℝ) : + 𝔼 p, G p = 𝔼 y, 𝔼 a, 𝔼 r : Fin n → A, G (y, Fin.cons a r) := by + rw [Fintype.expect_prod_type] + exact expect_congr rfl fun y _ ↦ Fin.expect_univ_cons fun w ↦ G (y, w) + set g : (Y × A) × (Fin n → A) → ℝ := fun q ↦ f (q.1.1, Fin.cons q.1.2 q.2) with hg + have hIH := ih g + have hsplit' (G : (Y × A) × (Fin n → A) → ℝ) : + 𝔼 q, G q = 𝔼 y, 𝔼 a, 𝔼 r, G ((y, a), r) := by + rw [Fintype.expect_prod_type, Fintype.expect_prod_type] + -- The average over the whole tuple, and over its tail. + set h : Y × A → ℝ := fun q ↦ 𝔼 r, g (q, r) with hh + have hM (y : Y) : 𝔼 w, f (y, w) = 𝔼 a, h (y, a) := Fin.expect_univ_cons fun w ↦ f (y, w) + -- Orthogonal decomposition over the fibers of `(y, a)`. + have hLHS : 𝔼 p, (f p - 𝔼 w, f (p.1, w)) ^ 2 = + 𝔼 q, (g q - 𝔼 r, g (q.1, r)) ^ 2 + 𝔼 y, 𝔼 a, (h (y, a) - 𝔼 a', h (y, a')) ^ 2 := by + rw [hsplit, hsplit', ← expect_add_distrib] + refine expect_congr rfl fun y _ ↦ ?_ + rw [← expect_add_distrib] + refine expect_congr rfl fun a _ ↦ ?_ + simp only [hM] + exact expect_sub_sq_eq (fun r ↦ g ((y, a), r)) _ + -- The tail coordinates, by the induction hypothesis. + have htail (i : Fin n) : 𝔼 q, (g q - 𝔼 b, g (q.1, update q.2 i b)) ^ 2 = + 𝔼 p, (f p - 𝔼 b, f (p.1, update p.2 i.succ b)) ^ 2 := by + rw [hsplit, hsplit'] + simp only [hg, Fin.cons_update] + -- The head coordinate, by Jensen's inequality. + have hhead : 𝔼 y, 𝔼 a, (h (y, a) - 𝔼 a', h (y, a')) ^ 2 ≤ + 𝔼 p, (f p - 𝔼 b, f (p.1, update p.2 0 b)) ^ 2 := by + rw [hsplit] + refine expect_le_expect fun y _ ↦ expect_le_expect fun a _ ↦ ?_ + have : h (y, a) - 𝔼 a', h (y, a') = + 𝔼 r, (f (y, Fin.cons a r) - 𝔼 b, f (y, update (Fin.cons a r) 0 b)) := by + simp only [hh, hg, Fin.update_cons_zero, expect_sub_distrib] + rw [expect_comm] + rw [this] + exact sq_expect_le_expect_sq _ _ + rw [hLHS, Fin.sum_univ_succ] + calc _ ≤ ∑ i : Fin n, 𝔼 q, (g q - 𝔼 b, g (q.1, update q.2 i b)) ^ 2 + + 𝔼 p, (f p - 𝔼 b, f (p.1, update p.2 0 b)) ^ 2 := add_le_add hIH hhead + _ = _ := by rw [add_comm]; simp only [htail] + +end Fintype diff --git a/ComplexityTests/PairShearTranslation.lean b/ComplexityTests/PairShearTranslation.lean new file mode 100644 index 000000000..cb28f0927 --- /dev/null +++ b/ComplexityTests/PairShearTranslation.lean @@ -0,0 +1,52 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +import Complexity.Foundations.Combinatorics.Expander.PairShearTranslation +import Complexity.Foundations.Probability.EfronStein + +/-! +# Shears and translations of coordinate pairs + +Concrete pair moves on `ZMod 2 × (Fin 3 → ZMod 5)`, an instance of the Efron–Stein inequality, and +a client of the pair bound: a function invariant under the moves of the pairs +`(i, i + 1)` of `Fin 3` depends only on the spectator, for every modulus `L` and every action on +the spectator. +-/ + +namespace ComplexityTests.PairShearTranslation + +open Cslib Cslib.RotationMap Finset Function +open scoped BigOperators + +-- The shear `w ↦ w + w 1 • e 0` acts on the spectator by `ρ`; the translation `w ↦ w + e 2` does +-- not. +example : pairShearTranslationMove (L := 5) (Equiv.addRight (1 : ZMod 2)) (Equiv.refl _) 0 1 0 + (0, ![1, 2, 3]) = (1, ![3, 2, 3]) := by decide +example : pairShearTranslationMove (L := 5) (Equiv.addRight (1 : ZMod 2)) (Equiv.refl _) 2 0 1 + (0, ![1, 2, 4]) = (0, ![0, 2, 4]) := by decide +example : pairShearTranslationMove (L := 5) (Equiv.addRight (1 : ZMod 2)) (Equiv.refl _) 1 2 3 + (0, ![1, 2, 4]) = (0, ![1, 2, 0]) := by decide + +/-- The Efron–Stein inequality instantiates with a trivial spectator and the alphabet `Bool`. -/ +example (f : Unit × (Fin 2 → Bool) → ℝ) : + 𝔼 p, (f p - 𝔼 w, f (p.1, w)) ^ 2 ≤ ∑ i, 𝔼 p, (f p - 𝔼 a, f (p.1, update p.2 i a)) ^ 2 := + Fintype.expect_sq_sub_expect_le_sum_expect_sq_sub_update f + +/-- **A client**: on `Y × (Fin 3 → ZMod L)`, a real function invariant under the moves of the +pairs `(i, i + 1)` depends only on the spectator, whatever the actions `ρ` on `Y`. -/ +example {Y : Type} [Fintype Y] (L : ℕ) [NeZero L] (ρ : Fin 3 → Fin 3 → Equiv.Perm Y) + (f : Y × (Fin 3 → ZMod L) → ℝ) + (hf : ∀ i j k p, f (pairShearTranslationMove (ρ i j) (ρ j i) i j k p) = f p) + (p : Y × (Fin 3 → ZMod L)) : + f p = 𝔼 w, f (p.1, w) := by + have h := expect_sq_sub_expect_le_pairShearTranslation ρ (fun i ↦ i + 1) (by decide) f + simp only [hf, sub_self, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, + expect_const_zero, sum_const_zero, mul_zero] at h + have h0 := (Fintype.expect_eq_zero_iff_of_nonneg fun q ↦ sq_nonneg + (f q - 𝔼 w, f (q.1, w))).1 (le_antisymm h (expect_nonneg fun _ _ ↦ sq_nonneg _)) + exact sub_eq_zero.1 (pow_eq_zero_iff two_ne_zero |>.1 (congrFun h0 p)) + +end ComplexityTests.PairShearTranslation From a547de38dc89ede2ccd896a86e6b71cdf36a8bf0 Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Fri, 30 Oct 2026 01:23:37 +0000 Subject: [PATCH 7/7] =?UTF-8?q?doc(Probability):=20cite=20Efron=E2=80=93St?= =?UTF-8?q?ein=20and=20Steele;=20numeric=20Efron=E2=80=93Stein=20test=20(#?= =?UTF-8?q?1682)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review fixes for #1699: - references.bib: EfronStein1981 (Ann. Statist. 9(3):586–596) and Steele1986 (Ann. Statist. 14(2):753–758), with DOIs; - EfronStein.lean cites both and gains a References section; - PairShearTranslation.lean notes that the all-coordinates bound is vacuous for H = 1; - the test computes both sides of Efron–Stein for the agreement indicator on Fin 2 → Bool (1/4 ≤ 1/2). Co-Authored-By: Claude Opus 5.5 --- .../Expander/PairShearTranslation.lean | 3 ++- .../Foundations/Probability/EfronStein.lean | 11 ++++++-- ComplexityTests/PairShearTranslation.lean | 26 ++++++++++++++----- references.bib | 22 ++++++++++++++++ 4 files changed, 53 insertions(+), 9 deletions(-) diff --git a/Complexity/Foundations/Combinatorics/Expander/PairShearTranslation.lean b/Complexity/Foundations/Combinatorics/Expander/PairShearTranslation.lean index 0ab4b088a..c438ae30f 100644 --- a/Complexity/Foundations/Combinatorics/Expander/PairShearTranslation.lean +++ b/Complexity/Foundations/Combinatorics/Expander/PairShearTranslation.lean @@ -22,7 +22,8 @@ where `ρ` is the action of the same elementary matrix on the frames. The second moment of `f` about its average over the whole tuple `w` is at most `512` times the sum, over the coordinates `i`, of the total squared change of `f` along the moves of a pair `(i, σ i)` -with `σ i ≠ i` (`expect_sq_sub_expect_le_pairShearTranslation`). The proof combines: +with `σ i ≠ i` (`expect_sq_sub_expect_le_pairShearTranslation`). Such a `σ` exists only when +`H ≠ 1`; for `H = 1` the hypothesis cannot hold, and the bound says nothing. The proof combines: * the Efron–Stein inequality (`Fintype.expect_sq_sub_expect_le_sum_expect_sq_sub_update`), which reduces the distance from the functions of `y` alone to the distances from the functions not diff --git a/Complexity/Foundations/Probability/EfronStein.lean b/Complexity/Foundations/Probability/EfronStein.lean index 05b114c4a..0db7e9bc0 100644 --- a/Complexity/Foundations/Probability/EfronStein.lean +++ b/Complexity/Foundations/Probability/EfronStein.lean @@ -19,8 +19,10 @@ For a function `f` of a spectator `y` and of a uniformly random tuple `w : Fin n moment of `f` about its average over `w` is at most the sum, over the coordinates `i`, of the second moments of `f` about its averages over the single coordinate `w i` (`Fintype.expect_sq_sub_expect_le_sum_expect_sq_sub_update`): -`𝔼 (f - 𝔼_w f)² ≤ ∑ i, 𝔼 (f - 𝔼_{w i} f)²`. This is the Efron–Stein inequality for the uniform -product measure, with the spectator as an extra fixed coordinate. It reduces the distance of `f` +`𝔼 (f - 𝔼_w f)² ≤ ∑ i, 𝔼 (f - 𝔼_{w i} f)²`. This is the Efron–Stein inequality +[Efron and Stein][EfronStein1981] in the general form for functions that need not be symmetric +[Steele][Steele1986], for the uniform product measure and with the spectator as an extra fixed +coordinate. It reduces the distance of `f` from the functions of `y` alone to its distances from the functions not depending on one coordinate at a time. @@ -33,6 +35,11 @@ on these fibers, and bound the fiber averages by Jensen's inequality. * `Fintype.expect_sq_sub_expect_le_sum_expect_sq_sub_update`: the Efron–Stein inequality. * `Fintype.expect_sq_sub_expect_update_le`: the average over one coordinate is the best approximation by functions not depending on it. + +## References + +* [B. Efron, C. Stein, *The Jackknife Estimate of Variance*][EfronStein1981] +* [J. M. Steele, *An Efron-Stein Inequality for Nonsymmetric Statistics*][Steele1986] -/ public section diff --git a/ComplexityTests/PairShearTranslation.lean b/ComplexityTests/PairShearTranslation.lean index cb28f0927..216bc9e72 100644 --- a/ComplexityTests/PairShearTranslation.lean +++ b/ComplexityTests/PairShearTranslation.lean @@ -10,8 +10,8 @@ import Complexity.Foundations.Probability.EfronStein /-! # Shears and translations of coordinate pairs -Concrete pair moves on `ZMod 2 × (Fin 3 → ZMod 5)`, an instance of the Efron–Stein inequality, and -a client of the pair bound: a function invariant under the moves of the pairs +Concrete pair moves on `ZMod 2 × (Fin 3 → ZMod 5)`, a concrete instance of the Efron–Stein +inequality, and a client of the pair bound: a function invariant under the moves of the pairs `(i, i + 1)` of `Fin 3` depends only on the spectator, for every modulus `L` and every action on the spectator. -/ @@ -30,10 +30,24 @@ example : pairShearTranslationMove (L := 5) (Equiv.addRight (1 : ZMod 2)) (Equiv example : pairShearTranslationMove (L := 5) (Equiv.addRight (1 : ZMod 2)) (Equiv.refl _) 1 2 3 (0, ![1, 2, 4]) = (0, ![1, 2, 0]) := by decide -/-- The Efron–Stein inequality instantiates with a trivial spectator and the alphabet `Bool`. -/ -example (f : Unit × (Fin 2 → Bool) → ℝ) : - 𝔼 p, (f p - 𝔼 w, f (p.1, w)) ^ 2 ≤ ∑ i, 𝔼 p, (f p - 𝔼 a, f (p.1, update p.2 i a)) ^ 2 := - Fintype.expect_sq_sub_expect_le_sum_expect_sq_sub_update f +/-- The indicator that the two coordinates of a uniform `w : Fin 2 → Bool` agree. -/ +noncomputable def eqInd (p : Unit × (Fin 2 → Bool)) : ℝ := if p.2 0 = p.2 1 then 1 else 0 + +/-- **Efron–Stein on a concrete function**: the second moment of `eqInd` about its average is +`1 / 4`, and the sum of the single-coordinate terms is `1 / 2`. -/ +example : 𝔼 p, (eqInd p - 𝔼 w, eqInd (p.1, w)) ^ 2 = 1 / 4 ∧ + ∑ i, 𝔼 p, (eqInd p - 𝔼 a, eqInd (p.1, update p.2 i a)) ^ 2 = 1 / 2 := by + constructor + · simp only [Fintype.expect_prod_type, Fin.expect_univ_cons, Fintype.expect_bool, + Fintype.expect_unique] + norm_num [eqInd] + · simp only [Fin.sum_univ_two, Fintype.expect_prod_type, Fin.expect_univ_cons, + Fintype.expect_bool, Fintype.expect_unique] + norm_num [eqInd, update_apply] + +example : 𝔼 p, (eqInd p - 𝔼 w, eqInd (p.1, w)) ^ 2 ≤ + ∑ i, 𝔼 p, (eqInd p - 𝔼 a, eqInd (p.1, update p.2 i a)) ^ 2 := + Fintype.expect_sq_sub_expect_le_sum_expect_sq_sub_update eqInd /-- **A client**: on `Y × (Fin 3 → ZMod L)`, a real function invariant under the moves of the pairs `(i, i + 1)` depends only on the spectator, whatever the actions `ρ` on `Y`. -/ diff --git a/references.bib b/references.bib index 7cae42ed4..213b20d08 100644 --- a/references.bib +++ b/references.bib @@ -1351,6 +1351,17 @@ @inproceedings{DunkelmanKellerShamir2012 doi = {10.1007/978-3-642-29011-4_21} } +@article{EfronStein1981, + author = {Efron, Bradley and Stein, Charles}, + title = {The Jackknife Estimate of Variance}, + journal = {The Annals of Statistics}, + volume = {9}, + number = {3}, + pages = {586--596}, + year = {1981}, + doi = {10.1214/aos/1176345462} +} + @article{EHKV1989, author = {Ehrenfeucht, Andrzej and Haussler, David and Kearns, Michael and Valiant, Leslie}, title = {A General Lower Bound on the Number of Examples Needed for Learning}, @@ -4198,6 +4209,17 @@ @inproceedings{StearnsHartmanisLewis1965 doi = {10.1109/FOCS.1965.11} } +@article{Steele1986, + author = {Steele, J. Michael}, + title = {An {Efron}-{Stein} Inequality for Nonsymmetric Statistics}, + journal = {The Annals of Statistics}, + volume = {14}, + number = {2}, + pages = {753--758}, + year = {1986}, + doi = {10.1214/aos/1176349952} +} + @article{Stockmeyer1976, author = {Stockmeyer, Larry J.}, title = {The Polynomial-Time Hierarchy},