feat(Expander): Efron–Stein and the coordinate-pair bound for shears and translations

Complexity.lean

@@ -2496,6 +2496,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
@@ -2801,6 +2802,7 @@ public import Complexity.Foundations.Probability.ConditionalProductMean
 public import Complexity.Foundations.Probability.CorrectionAtom
 public import Complexity.Foundations.Probability.DetectedHierarchy
 public import Complexity.Foundations.Probability.DetectedStage
+public import Complexity.Foundations.Probability.EfronStein
 public import Complexity.Foundations.Probability.EstimatorPrecision
 public import Complexity.Foundations.Probability.FineProductMean
 public import Complexity.Foundations.Probability.FourthRootHierarchyParams

Complexity/Foundations/Combinatorics/Expander/PairShearTranslation.lean

@@ -0,0 +1,168 @@
+/-
+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`). 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
+  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

Complexity/Foundations/Probability/EfronStein.lean

@@ -0,0 +1,148 @@
+/-
+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
+[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.
+
+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.
+
+## References
+
+* [B. Efron, C. Stein, *The Jackknife Estimate of Variance*][EfronStein1981]
+* [J. M. Steele, *An Efron-Stein Inequality for Nonsymmetric Statistics*][Steele1986]
+-/
+
+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