feat(Expander): fourth-moment decay of the random walk from the spectral gap

Complexity.lean

@@ -2419,6 +2419,7 @@ public import Complexity.Foundations.Combinatorics.Expander.Connected
 public import Complexity.Foundations.Combinatorics.Expander.Contraction
 public import Complexity.Foundations.Combinatorics.Expander.Existence
 public import Complexity.Foundations.Combinatorics.Expander.Family
+public import Complexity.Foundations.Combinatorics.Expander.FourthMoment
 public import Complexity.Foundations.Combinatorics.Expander.Hitting
 public import Complexity.Foundations.Combinatorics.Expander.Hom
 public import Complexity.Foundations.Combinatorics.Expander.IteratedProd

Complexity/Foundations/Combinatorics/Expander/Basic.lean

@@ -59,6 +59,7 @@ below is proved from these characterizations. `λ(G) ≤ 1` always, and `G` is a
 * `Cslib.RotationMap.expect_walk`, `Cslib.RotationMap.expect_mul_walk_comm`,
   `Cslib.RotationMap.expect_walk_sq_le`: the walk operator preserves expectations, is
   self-adjoint and does not increase the second moment.
+* `Cslib.RotationMap.sq_walk_le`: Jensen's inequality for the walk.
 * `Cslib.RotationMap.spectralExpansion_le_iff`,
   `Cslib.RotationMap.abs_expect_mul_walk_le`,
   `Cslib.RotationMap.spectralExpansion_le_iff_abs_expect_mul_walk_le`,
@@ -261,6 +262,14 @@ theorem walk_pow_const [Nonempty D] (t : ℕ) (c : ℝ) : (G.walk ^ t) (fun _ 
   | zero => rfl
   | succ t ih => rw [pow_succ, Module.End.mul_apply, walk_const, ih]
 
+/-- **Jensen's inequality for the walk**: the square of an average of neighbors is at most the
+average of the squares. -/
+theorem sq_walk_le (f : V → ℝ) (v : V) : G.walk f v ^ 2 ≤ G.walk (fun w ↦ f w ^ 2) v := by
+  rcases isEmpty_or_nonempty D with hD | hD
+  · simp [walk_apply]
+  simpa [walk_apply] using
+    expect_mul_sq_le_sq_mul_sq univ (fun i ↦ f (G.neighbor v i)) fun _ ↦ 1
+
 variable [Fintype V]
 
 /-- The walk operator preserves expectations. -/
@@ -298,11 +307,7 @@ theorem expect_mul_walk_comm (f g : V → ℝ) :
 theorem expect_walk_sq_le (f : V → ℝ) : 𝔼 v, G.walk f v ^ 2 ≤ 𝔼 v, f v ^ 2 := by
   rcases isEmpty_or_nonempty D with hD | hD
   · simpa [walk_apply] using expect_nonneg fun v _ ↦ sq_nonneg (f v)
-  calc 𝔼 v, G.walk f v ^ 2 ≤ 𝔼 v, 𝔼 i, f (G.neighbor v i) ^ 2 := by
-        refine expect_le_expect fun v _ ↦ ?_
-        simpa [walk_apply] using
-          expect_mul_sq_le_sq_mul_sq univ (fun i ↦ f (G.neighbor v i)) fun _ ↦ 1
-    _ = 𝔼 v, f v ^ 2 := G.expect_expect_neighbor fun v ↦ f v ^ 2
+  exact (expect_le_expect fun v _ ↦ G.sq_walk_le f v).trans_eq (G.expect_walk fun v ↦ f v ^ 2)
 
 end Walk
 

Complexity/Foundations/Combinatorics/Expander/FourthMoment.lean

@@ -0,0 +1,213 @@
+/-
+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.Basic
+import Mathlib.Algebra.Order.BigOperators.Expect
+
+/-!
+# Fourth moments of the random walk
+
+The spectral expansion `λ(G)` controls second moments: a walk of length `t` multiplies
+`𝔼 f²` by at most `λ(G) ^ (2 t)` when `𝔼 f = 0`
+(`expect_walk_pow_sq_le_spectralExpansion_pow_mul`). This file derives the same kind of decay for
+fourth moments, with elementary arguments only.
+
+The walk averages over neighbors, so Jensen's inequality holds pointwise:
+`(G.walk f v) ^ 2 ≤ G.walk (f ^ 2) v` (`sq_walk_le`), and therefore the walk does not increase
+fourth moments (`expect_walk_pow_pow_four_le`). For the decay, write `g = W ^ s f`, where `W` is
+the walk operator. Then `(W ^ t g) ^ 4 ≤ (W ^ t (g ^ 2)) ^ 2` pointwise. The function `g ^ 2` is
+its mean `m = 𝔼 g²` plus a part of expectation zero. The walk multiplies the second moment of
+that part by `λ ^ (2 t)`. Hence
+
+`𝔼 (W ^ (s + t) f) ^ 4 ≤ m ^ 2 + λ ^ (2 t) 𝔼 g ^ 4 ≤ (λ ^ (4 s) + λ ^ (2 t)) 𝔼 f ^ 4`,
+
+using `m ≤ λ ^ (2 s) 𝔼 f²` and `(𝔼 f²)² ≤ 𝔼 f⁴` (`expect_walk_pow_add_pow_four_le`). With
+`s = t` the fourth moment decays like `2 λ ^ (2 t)` over `2 t` steps
+(`expect_walk_pow_two_mul_pow_four_le`). Up to constants, this is the `p = 4` case of the
+`Lᵖ` contraction of a Markov operator with a spectral gap. That contraction usually comes from
+the Riesz–Thorin interpolation theorem; here no interpolation is needed. The centred form
+(`expect_walk_pow_two_mul_sub_expect_pow_four_le`) applies to every function.
+
+The use of `Lᵖ` contraction of the walk (idea 8 in issue #474) comes from the OpenAI preprint
+on derandomizing logarithmic space [OpenAI2026LogSpace], where the `Lˢ` decay
+`‖K ^ d - Π‖_{s → s} ≤ 2 ^ (1 - 2 / s) (1 - γ) ^ (2 d / s)` appears in the proof of Lemma 6.2 and
+comes from the Riesz–Thorin theorem; the Jensen argument here is a different proof.
+
+## Main results
+
+* `Cslib.RotationMap.sq_walk_pow_le`: Jensen's inequality for walks of every length, from the
+  one-step `Cslib.RotationMap.sq_walk_le`.
+* `Cslib.RotationMap.expect_walk_pow_pow_four_le`: walks do not increase fourth moments.
+* `Cslib.RotationMap.expect_walk_pow_add_pow_four_le`: the fourth-moment decay
+  `𝔼 (W ^ (s + t) f) ^ 4 ≤ (λ ^ (4 s) + λ ^ (2 t)) 𝔼 f ^ 4` for `𝔼 f = 0`.
+* `Cslib.RotationMap.expect_walk_pow_two_mul_pow_four_le`,
+  `Cslib.RotationMap.expect_walk_pow_two_mul_sub_expect_pow_four_le`: over `2 t` steps the
+  fourth moment of the deviation from the mean shrinks by `2 λ ^ (2 t)`.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
+  proof of Lemma 6.2 (preprint, not peer reviewed)
+-/
+
+public section
+
+namespace Cslib.RotationMap
+
+open Finset
+open scoped BigOperators
+
+variable {V D : Type*} (G : RotationMap V D)
+
+section Pointwise
+
+variable [Fintype D]
+
+/-- The walk operator is monotone. -/
+theorem walk_mono {f g : V → ℝ} (h : ∀ v, f v ≤ g v) (v : V) : G.walk f v ≤ G.walk g v := by
+  simp only [walk_apply]
+  exact expect_le_expect fun i _ ↦ h _
+
+/-- **Jensen's inequality for walks of every length.** -/
+theorem sq_walk_pow_le (t : ℕ) (f : V → ℝ) (v : V) :
+    (G.walk ^ t) f v ^ 2 ≤ (G.walk ^ t) (fun w ↦ f w ^ 2) v := by
+  induction t generalizing v with
+  | zero => simp
+  | succ t ih =>
+    rw [show G.walk ^ (t + 1) = G.walk * G.walk ^ t from pow_succ' _ _, Module.End.mul_apply,
+      Module.End.mul_apply]
+    exact (G.sq_walk_le _ v).trans (G.walk_mono ih v)
+
+/-- **Jensen's inequality for fourth powers.** -/
+theorem pow_four_walk_pow_le (t : ℕ) (f : V → ℝ) (v : V) :
+    (G.walk ^ t) f v ^ 4 ≤ (G.walk ^ t) (fun w ↦ f w ^ 4) v := by
+  calc (G.walk ^ t) f v ^ 4 = ((G.walk ^ t) f v ^ 2) ^ 2 := by ring
+    _ ≤ ((G.walk ^ t) (fun w ↦ f w ^ 2) v) ^ 2 :=
+        pow_le_pow_left₀ (sq_nonneg _) (G.sq_walk_pow_le t f v) 2
+    _ ≤ (G.walk ^ t) (fun w ↦ (f w ^ 2) ^ 2) v := G.sq_walk_pow_le t _ v
+    _ = (G.walk ^ t) (fun w ↦ f w ^ 4) v := by
+        rw [show (fun w ↦ (f w ^ 2) ^ 2) = fun w ↦ f w ^ 4 from funext fun w ↦ by ring]
+
+end Pointwise
+
+section Moments
+
+variable [Fintype V] [Fintype D] [Nonempty D]
+
+/-- **Walks do not increase fourth moments.** -/
+theorem expect_walk_pow_pow_four_le (t : ℕ) (f : V → ℝ) :
+    𝔼 v, (G.walk ^ t) f v ^ 4 ≤ 𝔼 v, f v ^ 4 :=
+  (expect_le_expect fun v _ ↦ G.pow_four_walk_pow_le t f v).trans_eq
+    (G.expect_walk_pow t fun w ↦ f w ^ 4)
+
+/-- The square of the second moment is at most the fourth moment. -/
+private theorem sq_expect_sq_le_expect_pow_four (f : V → ℝ) :
+    (𝔼 v, f v ^ 2) ^ 2 ≤ 𝔼 v, f v ^ 4 := by
+  have h := expect_mul_sq_le_sq_mul_sq univ (fun v ↦ f v ^ 2) fun _ ↦ (1 : ℝ)
+  rcases isEmpty_or_nonempty V with hV | hV
+  · simp
+  simp only [mul_one, one_pow, Fintype.expect_const] at h
+  simpa only [← pow_mul] using h
+
+/-- **Fourth-moment decay of the random walk**: for `𝔼 f = 0`, a walk of length `s + t`
+multiplies the fourth moment by at most `λ(G) ^ (4 s) + λ(G) ^ (2 t)`. -/
+theorem expect_walk_pow_add_pow_four_le {f : V → ℝ} (hf : 𝔼 v, f v = 0) (s t : ℕ) :
+    𝔼 v, (G.walk ^ (s + t)) f v ^ 4 ≤
+      (G.spectralExpansion ^ (4 * s) + G.spectralExpansion ^ (2 * t)) * 𝔼 v, f v ^ 4 := by
+  rcases isEmpty_or_nonempty V with hV | hV
+  · simp
+  set g := (G.walk ^ s) f with hg
+  set q : V → ℝ := fun w ↦ g w ^ 2 with hq
+  set m := 𝔼 v, q v with hm
+  set h := (G.walk ^ t) fun w ↦ q w - m with hh
+  have hsplit : (G.walk ^ (s + t)) f = (G.walk ^ t) g := by
+    rw [add_comm, pow_add, Module.End.mul_apply]
+  -- The walk of `q` is its mean plus the walk of the part of expectation zero.
+  have hq_split (v : V) : (G.walk ^ t) q v = h v + m := by
+    have : q = (fun w ↦ q w - m) + fun _ ↦ m := by
+      funext w
+      simp
+    rw [this, map_add, Pi.add_apply, walk_pow_const, ← hh]
+  have hq0 : 𝔼 v, (q v - m) = 0 := by
+    rw [expect_sub_distrib, Fintype.expect_const, sub_self]
+  have hh0 : 𝔼 v, h v = 0 := G.expect_walk_pow_eq_zero hq0 t
+  -- Pointwise Jensen reduces the fourth moment to the second moment of the walk of `q`.
+  have h₁ : 𝔼 v, (G.walk ^ t) g v ^ 4 ≤ 𝔼 v, (h v + m) ^ 2 := by
+    refine expect_le_expect fun v _ ↦ ?_
+    rw [← hq_split]
+    calc (G.walk ^ t) g v ^ 4 = ((G.walk ^ t) g v ^ 2) ^ 2 := by ring
+      _ ≤ _ := pow_le_pow_left₀ (sq_nonneg _) (G.sq_walk_pow_le t g v) 2
+  have h₂ : 𝔼 v, (h v + m) ^ 2 = 𝔼 v, h v ^ 2 + m ^ 2 := by
+    simp only [add_sq, expect_add_distrib, ← expect_mul, ← mul_expect, hh0,
+      Fintype.expect_const]
+    ring
+  -- The part of expectation zero decays at rate `λ ^ (2 t)`.
+  have h₃ : 𝔼 v, h v ^ 2 ≤ G.spectralExpansion ^ (2 * t) * 𝔼 v, f v ^ 4 := by
+    refine (G.expect_walk_pow_sq_le_spectralExpansion_pow_mul hq0 t).trans
+      (mul_le_mul_of_nonneg_left ?_ (pow_nonneg G.spectralExpansion_nonneg _))
+    calc 𝔼 v, (q v - m) ^ 2 = 𝔼 v, q v ^ 2 - m ^ 2 := by
+          simp only [sub_sq, expect_sub_distrib, expect_add_distrib, ← expect_mul,
+            ← mul_expect, Fintype.expect_const, ← hm]
+          ring
+      _ ≤ 𝔼 v, q v ^ 2 := sub_le_self _ (sq_nonneg _)
+      _ = 𝔼 v, g v ^ 4 := by
+          congr 1
+          funext v
+          rw [hq]
+          ring
+      _ ≤ 𝔼 v, f v ^ 4 := G.expect_walk_pow_pow_four_le s f
+  -- The mean of `q` decays at rate `λ ^ (2 s)`.
+  have h₄ : m ^ 2 ≤ G.spectralExpansion ^ (4 * s) * 𝔼 v, f v ^ 4 := by
+    have hm0 : 0 ≤ m := expect_nonneg fun v _ ↦ sq_nonneg _
+    have hms : m ≤ G.spectralExpansion ^ (2 * s) * 𝔼 v, f v ^ 2 :=
+      G.expect_walk_pow_sq_le_spectralExpansion_pow_mul hf s
+    calc m ^ 2 ≤ (G.spectralExpansion ^ (2 * s) * 𝔼 v, f v ^ 2) ^ 2 :=
+          pow_le_pow_left₀ hm0 hms 2
+      _ = G.spectralExpansion ^ (4 * s) * (𝔼 v, f v ^ 2) ^ 2 := by ring
+      _ ≤ G.spectralExpansion ^ (4 * s) * 𝔼 v, f v ^ 4 := by
+          have := G.spectralExpansion_nonneg
+          gcongr
+          exact sq_expect_sq_le_expect_pow_four f
+  rw [hsplit]
+  linarith
+
+/-- **Fourth-moment decay over `2 t` steps**: for `𝔼 f = 0`, a walk of length `2 t` multiplies
+the fourth moment by at most `2 λ(G) ^ (2 t)`. -/
+theorem expect_walk_pow_two_mul_pow_four_le {f : V → ℝ} (hf : 𝔼 v, f v = 0) (t : ℕ) :
+    𝔼 v, (G.walk ^ (2 * t)) f v ^ 4 ≤ 2 * G.spectralExpansion ^ (2 * t) * 𝔼 v, f v ^ 4 := by
+  have h := G.expect_walk_pow_add_pow_four_le hf t t
+  have hl₀ := G.spectralExpansion_nonneg
+  have hl₁ := G.spectralExpansion_le_one
+  have hpow : G.spectralExpansion ^ (4 * t) ≤ G.spectralExpansion ^ (2 * t) :=
+    pow_le_pow_of_le_one hl₀ hl₁ (by omega)
+  have h4 : 0 ≤ 𝔼 v, f v ^ 4 := expect_nonneg fun v _ ↦ by positivity
+  rw [← two_mul t] at h
+  have := mul_le_mul_of_nonneg_right hpow h4
+  nlinarith
+
+/-- **Fourth-moment decay for every function**: over `2 t` steps, the fourth moment of the
+deviation from the mean shrinks by at least the factor `2 λ(G) ^ (2 t)`. -/
+theorem expect_walk_pow_two_mul_sub_expect_pow_four_le (f : V → ℝ) (t : ℕ) :
+    𝔼 v, ((G.walk ^ (2 * t)) f v - 𝔼 w, f w) ^ 4 ≤
+      2 * G.spectralExpansion ^ (2 * t) * 𝔼 v, (f v - 𝔼 w, f w) ^ 4 := by
+  rcases isEmpty_or_nonempty V with hV | hV
+  · simp
+  set c := 𝔼 w, f w
+  have hsub : (G.walk ^ (2 * t)) (fun w ↦ f w - c) = fun v ↦ (G.walk ^ (2 * t)) f v - c := by
+    have : (fun w ↦ f w - c) = f - fun _ ↦ c := rfl
+    rw [this, map_sub, walk_pow_const]
+    rfl
+  have hc : 𝔼 v, (f v - c) = 0 := by
+    rw [expect_sub_distrib, Fintype.expect_const, sub_self]
+  have := G.expect_walk_pow_two_mul_pow_four_le hc t
+  rwa [hsub] at this
+
+end Moments
+
+end Cslib.RotationMap

ComplexityTests/WalkFourthMoment.lean

@@ -0,0 +1,62 @@
+/-
+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.AffinePlane
+import Complexity.Foundations.Combinatorics.Expander.FourthMoment
+import Mathlib.Algebra.Field.ZMod
+
+/-!
+# Fourth moments of the random walk
+
+Jensen's inequality for the walk on a concrete function, where it is strict, and the
+fourth-moment decay on the affine-plane expander over `𝔽₅`: two steps shrink the fourth moment of
+every function of expectation zero by at least the factor `2 / 5`.
+-/
+
+namespace ComplexityTests.WalkFourthMoment
+
+open Cslib Cslib.RotationMap Finset
+open scoped BigOperators
+
+private instance : Fact (Nat.Prime 5) := ⟨Nat.prime_five⟩
+
+-- One step of the affine-plane walk on `𝔽₃ × 𝔽₃` from `(0, 0)` averages `f` over the line
+-- `{(c, 0)}`; for the indicator of `(1, 0)` this is `1 / 3`, and `(1 / 3) ^ 2 < 1 / 3`.
+example : (affinePlane (ZMod 3)).walk (fun p ↦ if p = (1, 0) then (1 : ℝ) else 0) (0, 0) ^ 2 ≤
+    (affinePlane (ZMod 3)).walk (fun p ↦ (if p = (1, 0) then (1 : ℝ) else 0) ^ 2) (0, 0) :=
+  sq_walk_le _ _ _
+
+private theorem walk_indicator :
+    (affinePlane (ZMod 3)).walk (fun p ↦ if p = (1, 0) then (1 : ℝ) else 0) (0, 0) = 1 / 3 := by
+  rw [walk_affinePlane, Fintype.expect_eq_sum_div_card]
+  simp [ZMod.card]
+
+-- Here Jensen's inequality is strict.
+example : (affinePlane (ZMod 3)).walk (fun p ↦ if p = (1, 0) then (1 : ℝ) else 0) (0, 0) ^ 2 <
+    (affinePlane (ZMod 3)).walk (fun p ↦ (if p = (1, 0) then (1 : ℝ) else 0) ^ 2) (0, 0) := by
+  have h : (fun p : ZMod 3 × ZMod 3 ↦ (if p = (1, 0) then (1 : ℝ) else 0) ^ 2) =
+      fun p ↦ if p = (1, 0) then (1 : ℝ) else 0 := funext fun p ↦ by split_ifs <;> norm_num
+  rw [h, walk_indicator]
+  norm_num
+
+-- Two steps of the affine-plane walk over `𝔽₅` shrink fourth moments by the factor `2 / 5`.
+example (f : ZMod 5 × ZMod 5 → ℝ) (hf : 𝔼 v, f v = 0) :
+    𝔼 v, ((affinePlane (ZMod 5)).walk ^ 2) f v ^ 4 ≤ 2 * (1 / 5) * 𝔼 v, f v ^ 4 := by
+  have h := (affinePlane (ZMod 5)).expect_walk_pow_two_mul_pow_four_le hf 1
+  have hl := spectralExpansion_affinePlane_le (ZMod 5)
+  have hl₀ := (affinePlane (ZMod 5)).spectralExpansion_nonneg
+  have hsq : (affinePlane (ZMod 5)).spectralExpansion ^ (2 * 1) ≤ 1 / 5 := by
+    calc _ ≤ Real.sqrt (1 / Fintype.card (ZMod 5)) ^ 2 := by
+          rw [mul_one]
+          exact pow_le_pow_left₀ hl₀ hl 2
+      _ = 1 / 5 := by
+          rw [Real.sq_sqrt (by positivity), ZMod.card]
+          norm_num
+  have h4 : 0 ≤ 𝔼 v, f v ^ 4 := expect_nonneg fun v _ ↦ by positivity
+  rw [mul_one] at h
+  nlinarith
+
+end ComplexityTests.WalkFourthMoment