diff --git a/Complexity.lean b/Complexity.lean index f08f52b9d..23099724e 100644 --- a/Complexity.lean +++ b/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 diff --git a/Complexity/Foundations/Combinatorics/Expander/PairShearTranslation.lean b/Complexity/Foundations/Combinatorics/Expander/PairShearTranslation.lean new file mode 100644 index 000000000..c438ae30f --- /dev/null +++ b/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 diff --git a/Complexity/Foundations/Probability/EfronStein.lean b/Complexity/Foundations/Probability/EfronStein.lean new file mode 100644 index 000000000..0db7e9bc0 --- /dev/null +++ b/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 diff --git a/ComplexityTests/PairShearTranslation.lean b/ComplexityTests/PairShearTranslation.lean new file mode 100644 index 000000000..216bc9e72 --- /dev/null +++ b/ComplexityTests/PairShearTranslation.lean @@ -0,0 +1,66 @@ +/- +Copyright (c) 2026 Christian Reitwiessner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner +-/ + +import Complexity.Foundations.Combinatorics.Expander.PairShearTranslation +import Complexity.Foundations.Probability.EfronStein + +/-! +# Shears and translations of coordinate pairs + +Concrete pair moves on `ZMod 2 × (Fin 3 → ZMod 5)`, a concrete instance of the Efron–Stein +inequality, and a client of the pair bound: a function invariant under the moves of the pairs +`(i, i + 1)` of `Fin 3` depends only on the spectator, for every modulus `L` and every action on +the spectator. +-/ + +namespace ComplexityTests.PairShearTranslation + +open Cslib Cslib.RotationMap Finset Function +open scoped BigOperators + +-- The shear `w ↦ w + w 1 • e 0` acts on the spectator by `ρ`; the translation `w ↦ w + e 2` does +-- not. +example : pairShearTranslationMove (L := 5) (Equiv.addRight (1 : ZMod 2)) (Equiv.refl _) 0 1 0 + (0, ![1, 2, 3]) = (1, ![3, 2, 3]) := by decide +example : pairShearTranslationMove (L := 5) (Equiv.addRight (1 : ZMod 2)) (Equiv.refl _) 2 0 1 + (0, ![1, 2, 4]) = (0, ![0, 2, 4]) := by decide +example : pairShearTranslationMove (L := 5) (Equiv.addRight (1 : ZMod 2)) (Equiv.refl _) 1 2 3 + (0, ![1, 2, 4]) = (0, ![1, 2, 0]) := by decide + +/-- The indicator that the two coordinates of a uniform `w : Fin 2 → Bool` agree. -/ +noncomputable def eqInd (p : Unit × (Fin 2 → Bool)) : ℝ := if p.2 0 = p.2 1 then 1 else 0 + +/-- **Efron–Stein on a concrete function**: the second moment of `eqInd` about its average is +`1 / 4`, and the sum of the single-coordinate terms is `1 / 2`. -/ +example : 𝔼 p, (eqInd p - 𝔼 w, eqInd (p.1, w)) ^ 2 = 1 / 4 ∧ + ∑ i, 𝔼 p, (eqInd p - 𝔼 a, eqInd (p.1, update p.2 i a)) ^ 2 = 1 / 2 := by + constructor + · simp only [Fintype.expect_prod_type, Fin.expect_univ_cons, Fintype.expect_bool, + Fintype.expect_unique] + norm_num [eqInd] + · simp only [Fin.sum_univ_two, Fintype.expect_prod_type, Fin.expect_univ_cons, + Fintype.expect_bool, Fintype.expect_unique] + norm_num [eqInd, update_apply] + +example : 𝔼 p, (eqInd p - 𝔼 w, eqInd (p.1, w)) ^ 2 ≤ + ∑ i, 𝔼 p, (eqInd p - 𝔼 a, eqInd (p.1, update p.2 i a)) ^ 2 := + Fintype.expect_sq_sub_expect_le_sum_expect_sq_sub_update eqInd + +/-- **A client**: on `Y × (Fin 3 → ZMod L)`, a real function invariant under the moves of the +pairs `(i, i + 1)` depends only on the spectator, whatever the actions `ρ` on `Y`. -/ +example {Y : Type} [Fintype Y] (L : ℕ) [NeZero L] (ρ : Fin 3 → Fin 3 → Equiv.Perm Y) + (f : Y × (Fin 3 → ZMod L) → ℝ) + (hf : ∀ i j k p, f (pairShearTranslationMove (ρ i j) (ρ j i) i j k p) = f p) + (p : Y × (Fin 3 → ZMod L)) : + f p = 𝔼 w, f (p.1, w) := by + have h := expect_sq_sub_expect_le_pairShearTranslation ρ (fun i ↦ i + 1) (by decide) f + simp only [hf, sub_self, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, + expect_const_zero, sum_const_zero, mul_zero] at h + have h0 := (Fintype.expect_eq_zero_iff_of_nonneg fun q ↦ sq_nonneg + (f q - 𝔼 w, f (q.1, w))).1 (le_antisymm h (expect_nonneg fun _ _ ↦ sq_nonneg _)) + exact sub_eq_zero.1 (pow_eq_zero_iff two_ne_zero |>.1 (congrFun h0 p)) + +end ComplexityTests.PairShearTranslation diff --git a/references.bib b/references.bib index cc6369c43..e1f260685 100644 --- a/references.bib +++ b/references.bib @@ -1405,6 +1405,17 @@ @inproceedings{DunkelmanKellerShamir2012 doi = {10.1007/978-3-642-29011-4_21} } +@article{EfronStein1981, + author = {Efron, Bradley and Stein, Charles}, + title = {The Jackknife Estimate of Variance}, + journal = {The Annals of Statistics}, + volume = {9}, + number = {3}, + pages = {586--596}, + year = {1981}, + doi = {10.1214/aos/1176345462} +} + @article{EHKV1989, author = {Ehrenfeucht, Andrzej and Haussler, David and Kearns, Michael and Valiant, Leslie}, title = {A General Lower Bound on the Number of Examples Needed for Learning}, @@ -4367,6 +4378,17 @@ @inproceedings{StearnsHartmanisLewis1965 doi = {10.1109/FOCS.1965.11} } +@article{Steele1986, + author = {Steele, J. Michael}, + title = {An {Efron}-{Stein} Inequality for Nonsymmetric Statistics}, + journal = {The Annals of Statistics}, + volume = {14}, + number = {2}, + pages = {753--758}, + year = {1986}, + doi = {10.1214/aos/1176349952} +} + @article{Stockmeyer1976, author = {Stockmeyer, Larry J.}, title = {The Polynomial-Time Hierarchy},