From da700d59ab9cc380f07740dd401e10d94dc182df Mon Sep 17 00:00:00 2001 From: Christian Reitwiessner Date: Thu, 29 Oct 2026 23:17:17 +0000 Subject: [PATCH 1/3] =?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/3] =?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/3] 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