Import the Aaronson–Ambainis influence conjecture formalization

LeanPool/AaronsonAmbainis.lean

@@ -0,0 +1,84 @@
+/-
+Copyright (c) 2026 David Turturean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Turturean
+-/
+
+module
+
+-- Adapted for Lean Pool’s module system and pinned Mathlib.
+
+public import LeanPool.AaronsonAmbainis.Main
+public import LeanPool.AaronsonAmbainis.Bridge.Instance
+public import LeanPool.AaronsonAmbainis.Bridge.Positivity
+public import LeanPool.AaronsonAmbainis.Bridge.PaperInequalities
+public import LeanPool.AaronsonAmbainis.Bridge.PaperTheorems
+public import LeanPool.AaronsonAmbainis.Row.HypothesisCheck
+public import LeanPool.AaronsonAmbainis.Dual.Sanity
+
+/-!
+# The Aaronson–Ambainis influence conjecture
+
+Source: url:https://github.com/physical-superintelligence/aaronson-ambainis/tree/2a6ceaef872ae993708950f951989134084b851a
+Authors: David Turturean
+Status: verified
+Main declarations: `AaronsonAmbainis.aaronson_ambainis`,
+  `AaronsonAmbainis.aaronson_ambainis_explicit`, `AaronsonAmbainis.aaronson_ambainis_pm`
+Tags: boolean-functions, influence, fractional-certificates
+MSC: 68Q12, 60C05, 05D40
+-/
+
+/-!
+## Upstream attribution
+
+Adapted for Lean Pool’s module system and pinned dependencies from upstream commit
+`2a6ceaef872ae993708950f951989134084b851a`.
+
+The Aaronson–Ambainis conjecture: paper and Lean 4 formalization
+
+Copyright 2026 David Turturean
+
+The Lean source code and the repository documentation are licensed under the
+Apache License, Version 2.0. See LICENSE for the full text.
+
+The upstream paper, "A proof of the Aaronson–Ambainis conjecture," is authored
+by David Turturean and remains copyright its author.
+
+The conjecture is due to Scott Aaronson and Andris Ambainis, "The need for
+structure in quantum speedups," Theory of Computing 10 (2014), 133-166
+(arXiv:0911.0996).
+
+The proof builds on ideas from the following works, which are credited in the
+paper together with the other sources:
+
+  David Reimer, "Proof of the van den Berg-Kesten conjecture," Combinatorics,
+  Probability and Computing 9 (2000), 27-32 (the Butterfly Lemma, which the
+  bijection theorem of the paper refines, and the passage from antipodal pairs
+  of subcubes to all pairs of points).
+
+  Jeff Kahn, Michael Saks and Clifford Smyth, "The dual BKR inequality and
+  Rudich's conjecture," Combinatorics, Probability and Computing 20 (2011),
+  257-266 (the proof of the dual inequality, which uses that passage and
+  certificates at a point and at its antipode).
+
+  Raghav Kulkarni and Avishay Tal, "On fractional block sensitivity," Chicago
+  Journal of Theoretical Computer Science 2016, Article 8 (the lemma on the
+  fractional certificates at two points with different values).
+
+  Shachar Lovett and Jiapeng Zhang, "Fractional certificates for bounded
+  functions," ITCS 2023 (the use of fractional certificates and of level sets).
+
+  Avantika Agarwal and Shalev Ben-David, "Oracle separations for the
+  quantum-classical polynomial hierarchy," arXiv:2410.19062; ITCS 2026 (the
+  bound for the fractional block sensitivity of bounded functions of low
+  degree, and the method of its proof).
+
+  Yuval Filmus, Hamed Hatami, Nathan Keller and Noam Lifshitz, "On the sum of
+  the L1 influences of bounded functions," Israel Journal of Mathematics 214
+  (2016), 167-192 (the bound for the sum of the absolute increments at a
+  point).
+
+The mathematical statements and Lean formalization were produced by AI models in a
+research harness developed by David Turturean at PSI. David Turturean reviewed the
+paper and is responsible for its correctness.
+-/

LeanPool/AaronsonAmbainis/AllPairsDefs.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2026 David Turturean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Turturean
+-/
+module
+
+-- Adapted for Lean Pool’s module system and pinned Mathlib.
+
+public import Mathlib.Algebra.BigOperators.Group.Finset.Defs
+public import Mathlib.Basic.Real.Basic
+public import Mathlib.Data.Fintype.Pi
+public import LeanPool.AaronsonAmbainis.Statements
+
+/-!
+# Interface for the proof of the two-sided inequality from the antipodal inequality
+
+`AllPairsInequality` is the all-pairs inequality (the inequality of Proposition 5.2 of the paper:
+the sum over all pairs of a one and a zero of `g`), multiplied by `2` so that `2^(n-1)` does not
+appear.
+
+It splits the proof of `AntipodalInequality → TwoSidedInequality` into two independent parts:
+
+* `AntipodalInequality → AllPairsInequality` — apply the antipodal inequality (Theorem 4.3) on
+  every subcube and add up (Section 5.1);
+* `AllPairsInequality → TwoSidedInequality` — the overlap lemma (Lemma 4.1) and the
+  Cauchy–Schwarz inequality (Section 5.2).
+
+The all-pairs inequality is also the starting point of the statements on real functions:
+applied to the level functions `1_{f > t}` of a real function `f` and integrated over the level
+`t`, it gives the integrated all-pairs inequality (`Level/Integrated.lean`).
+-/
+
+@[expose] public section
+
+namespace AaronsonAmbainis
+
+open Finset
+
+/-- The all-pairs inequality (the inequality of Proposition 5.2 of the paper, multiplied by `2`).
+For every Boolean `g`, all positive weights `w` and every row field `lam`:
+`2 · ∑_{x : g x = true} ∑_{y : g y = false} 1 / (∑_{j ∈ Δ(x,y)} w_j lam^x_j lam^y_j)
+  ≤ 2^n · ∑_j b_j(g) / w_j`. -/
+def AllPairsInequality : Prop :=
+  ∀ (ι : Type) [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (w : ι → ℝ), (∀ j, 0 < w j) →
+  ∀ (lam : Cube ι → ι → ℝ), (∀ x, IsRow g x (lam x)) →
+    2 * ∑ x ∈ univ.filter (fun x : Cube ι => g x = true),
+          ∑ y ∈ univ.filter (fun y : Cube ι => g y = false),
+            (∑ j ∈ diffSet x y, w j * lam x j * lam y j)⁻¹
+      ≤ 2 ^ Fintype.card ι * ∑ j, (bdry g j : ℝ) / w j
+
+end AaronsonAmbainis

LeanPool/AaronsonAmbainis/Average/Coordinate.lean

@@ -0,0 +1,193 @@
+/-
+Copyright (c) 2026 David Turturean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Turturean
+-/
+module
+
+-- Adapted for Lean Pool’s module system and pinned Mathlib.
+
+public import Mathlib.Algebra.BigOperators.Field
+public import Mathlib.Algebra.Order.Star.Real
+public import Mathlib.Tactic.Linarith
+public import Mathlib.Tactic.NormNum
+public import Mathlib.Tactic.Positivity
+public import Mathlib.Tactic.Ring
+public import LeanPool.AaronsonAmbainis.TwoSided.Basic
+
+/-!
+# Averaging a function over one coordinate
+
+For a coordinate `j` let `avg j f x = (f x + f (x^j)) / 2`. Then (Lemma 8.1 of the paper)
+
+* `variance_avg`         — `Var f = Var (avg j f) + Inf_j f` (`f = avg j f + (f - f ∘ flip_j)/2`,
+                           and the two parts are even and odd under the flip of `j`);
+* `inflR_avg_le`         — `Inf_k (avg j f) ≤ Inf_k f` for every `k`;
+* `meanAbsIncr_avg_le`   — `L_k (avg j f) ≤ L_k f` for every `k`;
+* `meanAbsIncr_avg_self` — `L_j (avg j f) = 0`;
+* `rows_avg`             — if `a x` is a row of `f` at `x` for every `x`, of cost at most `K`,
+                           then `(a x + a (x^j)) / 2` is a row of `avg j f` at `x`, of cost at
+                           most `K`.
+
+Here `L_k(f) = meanAbsIncr f k` is the mean absolute increment of `f` in the coordinate `k`.
+-/
+
+@[expose] public section
+
+namespace AaronsonAmbainis
+namespace Average
+
+open Finset
+
+section NoFintype
+
+variable {ι : Type*} [DecidableEq ι]
+
+/-- Flips commute. -/
+lemma flipSet_comm (x : Cube ι) (S T : Finset ι) :
+    flipSet (flipSet x S) T = flipSet (flipSet x T) S := by
+  funext i
+  by_cases hS : i ∈ S <;> by_cases hT : i ∈ T <;> simp [flipSet, hS, hT]
+
+end NoFintype
+
+variable {ι : Type} [Fintype ι] [DecidableEq ι]
+
+/-- Flipping the same coordinates in two points does not change the set where they differ. -/
+lemma diffSet_flip (x y : Cube ι) (S : Finset ι) :
+    diffSet (flipSet x S) (flipSet y S) = diffSet x y := by
+  ext i
+  rw [mem_diffSet, mem_diffSet, flipSet_apply, flipSet_apply]
+  by_cases hS : i ∈ S
+  · rw [ite_eq_left hS, ite_eq_left hS]
+    cases x i <;> cases y i <;> simp
+  · rw [ite_eq_right hS, ite_eq_right hS]
+
+/-- The flip of the coordinate `j` is a bijection of the cube. -/
+lemma sum_flip (j : ι) (F : Cube ι → ℝ) : ∑ x, F (flipSet x {j}) = ∑ x, F x := by
+  have hinv : Function.Involutive (fun x : Cube ι => flipSet x {j}) :=
+    fun x => flipSet_flipSet_self x {j}
+  exact Equiv.sum_comp hinv.toPerm F
+
+/-- The average of `f` over the coordinate `j`. -/
+noncomputable def avg (j : ι) (f : Cube ι → ℝ) : Cube ι → ℝ :=
+  fun x => (f x + f (flipSet x {j})) / 2
+
+omit [Fintype ι] in
+lemma avg_flip (j : ι) (f : Cube ι → ℝ) (x : Cube ι) : avg j f (flipSet x {j}) = avg j f x := by
+  unfold avg
+  rw [flipSet_flipSet_self]
+  ring
+
+theorem mean_avg (j : ι) (f : Cube ι → ℝ) : mean (avg j f) = mean f := by
+  unfold mean avg
+  congr 1
+  rw [← Finset.sum_div, Finset.sum_add_distrib, sum_flip j f]
+  ring
+
+/-- `Var f = Var (avg j f) + Inf_j f`. -/
+theorem variance_avg (j : ι) (f : Cube ι → ℝ) :
+    variance f = variance (avg j f) + inflR f j := by
+  have hm := mean_avg j f
+  have hre : ∑ x, (f (flipSet x {j}) - mean f) ^ 2 = ∑ x, (f x - mean f) ^ 2 :=
+    sum_flip j (fun x => (f x - mean f) ^ 2)
+  have hpt : ∀ x, (f x - mean f) ^ 2 + (f (flipSet x {j}) - mean f) ^ 2
+      = 2 * ((avg j f x - mean f) ^ 2 + ((f x - f (flipSet x {j})) / 2) ^ 2) := by
+    intro x
+    unfold avg
+    ring
+  have hsum : ∑ x, (f x - mean f) ^ 2 + ∑ x, (f (flipSet x {j}) - mean f) ^ 2
+      = 2 * (∑ x, (avg j f x - mean f) ^ 2 + ∑ x, ((f x - f (flipSet x {j})) / 2) ^ 2) := by
+    rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib, Finset.mul_sum]
+    exact Finset.sum_congr rfl (fun x _ => hpt x)
+  rw [hre] at hsum
+  have hkey : ∑ x, (f x - mean f) ^ 2
+      = ∑ x, (avg j f x - mean f) ^ 2 + ∑ x, ((f x - f (flipSet x {j})) / 2) ^ 2 := by
+    linarith
+  unfold variance inflR
+  rw [hm, ← add_div, hkey]
+
+/-- `Inf_k (avg j f) ≤ Inf_k f` for every `k`. -/
+theorem inflR_avg_le (j k : ι) (f : Cube ι → ℝ) : inflR (avg j f) k ≤ inflR f k := by
+  have hcomm : ∀ x : Cube ι, flipSet (flipSet x {k}) {j} = flipSet (flipSet x {j}) {k} :=
+    fun x => flipSet_comm x {k} {j}
+  have hpt : ∀ x, ((avg j f x - avg j f (flipSet x {k})) / 2) ^ 2
+      ≤ (((f x - f (flipSet x {k})) / 2) ^ 2
+        + ((f (flipSet x {j}) - f (flipSet (flipSet x {j}) {k})) / 2) ^ 2) / 2 := by
+    intro x
+    unfold avg
+    rw [hcomm x]
+    nlinarith [sq_nonneg ((f x - f (flipSet x {k}))
+      - (f (flipSet x {j}) - f (flipSet (flipSet x {j}) {k})))]
+  have hre : ∑ x, ((f (flipSet x {j}) - f (flipSet (flipSet x {j}) {k})) / 2) ^ 2
+      = ∑ x, ((f x - f (flipSet x {k})) / 2) ^ 2 :=
+    sum_flip j (fun x => ((f x - f (flipSet x {k})) / 2) ^ 2)
+  unfold inflR
+  apply div_le_div_of_nonneg_right _ (by positivity)
+  calc ∑ x, ((avg j f x - avg j f (flipSet x {k})) / 2) ^ 2
+      ≤ ∑ x, (((f x - f (flipSet x {k})) / 2) ^ 2
+          + ((f (flipSet x {j}) - f (flipSet (flipSet x {j}) {k})) / 2) ^ 2) / 2 :=
+        Finset.sum_le_sum (fun x _ => hpt x)
+    _ = ∑ x, ((f x - f (flipSet x {k})) / 2) ^ 2 := by
+        rw [← Finset.sum_div, Finset.sum_add_distrib, hre]
+        ring
+
+/-- `L_k (avg j f) ≤ L_k f` for every `k`. -/
+theorem meanAbsIncr_avg_le (j k : ι) (f : Cube ι → ℝ) :
+    meanAbsIncr (avg j f) k ≤ meanAbsIncr f k := by
+  have hcomm : ∀ x : Cube ι, flipSet (flipSet x {k}) {j} = flipSet (flipSet x {j}) {k} :=
+    fun x => flipSet_comm x {k} {j}
+  have hpt : ∀ x, |avg j f x - avg j f (flipSet x {k})|
+      ≤ (|f x - f (flipSet x {k})|
+        + |f (flipSet x {j}) - f (flipSet (flipSet x {j}) {k})|) / 2 := by
+    intro x
+    have e : avg j f x - avg j f (flipSet x {k})
+        = ((f x - f (flipSet x {k}))
+          + (f (flipSet x {j}) - f (flipSet (flipSet x {j}) {k}))) / 2 := by
+      unfold avg
+      rw [hcomm x]
+      ring
+    rw [e, abs_div, abs_two]
+    exact div_le_div_of_nonneg_right (abs_add_le _ _) (by norm_num)
+  have hre : ∑ x, |f (flipSet x {j}) - f (flipSet (flipSet x {j}) {k})|
+      = ∑ x, |f x - f (flipSet x {k})| :=
+    sum_flip j (fun x => |f x - f (flipSet x {k})|)
+  unfold meanAbsIncr
+  apply div_le_div_of_nonneg_right _ (by positivity)
+  calc ∑ x, |avg j f x - avg j f (flipSet x {k})|
+      ≤ ∑ x, (|f x - f (flipSet x {k})|
+          + |f (flipSet x {j}) - f (flipSet (flipSet x {j}) {k})|) / 2 :=
+        Finset.sum_le_sum (fun x _ => hpt x)
+    _ = ∑ x, |f x - f (flipSet x {k})| := by
+        rw [← Finset.sum_div, Finset.sum_add_distrib, hre]
+        ring
+
+/-- `L_j (avg j f) = 0`. -/
+theorem meanAbsIncr_avg_self (j : ι) (f : Cube ι → ℝ) : meanAbsIncr (avg j f) j = 0 := by
+  unfold meanAbsIncr
+  rw [Finset.sum_eq_zero (fun x _ => by rw [avg_flip, sub_self, abs_zero]), zero_div]
+
+/-- Rows of `f` give rows of `avg j f` of the same cost. -/
+theorem rows_avg (j : ι) {f : Cube ι → ℝ} {a : Cube ι → ι → ℝ} {K : ℝ}
+    (ha : ∀ x i, 0 ≤ a x i) (hsum : ∀ x, ∑ i, a x i ≤ K)
+    (hrow : ∀ x y, |f x - f y| ≤ ∑ i ∈ diffSet x y, a x i) :
+    (∀ x i, 0 ≤ (a x i + a (flipSet x {j}) i) / 2) ∧
+    (∀ x, ∑ i, (a x i + a (flipSet x {j}) i) / 2 ≤ K) ∧
+    ∀ x y, |avg j f x - avg j f y| ≤ ∑ i ∈ diffSet x y, (a x i + a (flipSet x {j}) i) / 2 := by
+  refine ⟨fun x i => div_nonneg (add_nonneg (ha x i) (ha _ i)) (by norm_num), fun x => ?_,
+    fun x y => ?_⟩
+  · rw [← Finset.sum_div, Finset.sum_add_distrib]
+    linarith [hsum x, hsum (flipSet x {j})]
+  · have h1 := hrow x y
+    have h2 := hrow (flipSet x {j}) (flipSet y {j})
+    rw [diffSet_flip] at h2
+    have e : avg j f x - avg j f y
+        = ((f x - f y) + (f (flipSet x {j}) - f (flipSet y {j}))) / 2 := by
+      unfold avg
+      ring
+    rw [e, abs_div, abs_two, ← Finset.sum_div, Finset.sum_add_distrib]
+    exact div_le_div_of_nonneg_right (le_trans (abs_add_le _ _) (add_le_add h1 h2))
+      (by norm_num)
+
+end Average
+end AaronsonAmbainis