The main theorem and the conjecture as printed

Source.

S. Aaronson and A. Ambainis, The need for structure in quantum speedups, arXiv:0911.0996, Conjecture 6 (Conjecture 1.7 of the journal version, Theory of Computing 10 (2014), 133–166):

Let p : R^N → R be a polynomial of degree d. Suppose that 0 ≤ p(X) ≤ 1 for all X ∈ {0,1}^N, and E_X[(p(X) − E[p])²] ≥ ε. Then there exists an i such that Inf_i[p] ≥ (ε/d)^{O(1)}, where Inf_i[p] := E_X[(p(X) − p(X^i))²].

The conjecture, and its form on the cube {1,-1}^n (problem_statement.md), are transcribed without the definitions of Defs.lean: Ex, flipBit, ev01, evPM spell out the expectation, the bit flip and the evaluation of a polynomial on the two cubes. evPM sends true to -1, as Defs.lean does; the statement ExplicitBoundPM of Conjecture.lean sends true to 1 (evPMt, in the last section).

MainBound C is a bound of the kind of the main theorem with a constant C: 3 Var(f)^5 ≤ C d^12 Inf_j(f)². So MainTheorem is MainBound (50000 π^8) and MainTheoremImproved is MainBound (3125 π^8). Every such bound is carried over to polynomials:

• pm_of_mainBound — on the cube {1,-1}^n, for |p| ≤ 1: 3 ε^5 ≤ C d^12 Inf_i(p)²;
• zo_of_mainBound — on the cube {0,1}^N, for 0 ≤ p ≤ 1 (the bound is applied to 1 − 2p, whose variance is 4 Var[p]): 3072 ε^5 ≤ C d^12 Inf_i[p]².

The bounds are then put in the form in which the paper prints them, with the power 5/2 written as ε² √ε (sqrt_form_iff). From MainTheorem:

• pm_sq_of_mainTheorem, pm_sqrt_of_mainTheorem — 3 ε^5 ≤ 50000 π^8 d^12 Inf_i(p)², that is, Inf_i(p) ≥ (√15 / (500 π^4)) ε^{5/2} / d^6;
• zo_sq_of_mainTheorem, zo_sqrt_of_mainTheorem — 192 ε^5 ≤ 3125 π^8 d^12 Inf_i[p]², that is, Inf_i[p] ≥ (8 √15 / (125 π^4)) ε^{5/2} / d^6;
• zo_pow_of_mainTheorem — Inf_i[p] ≥ (ε/d)^7, the conjecture as printed (ratio_pow_le).

From MainTheoremImproved:

• zo_sq_of_mainTheoremImproved, zo_sqrt_of_mainTheoremImproved — 3072 ε^5 ≤ 3125 π^8 d^12 Inf_i[p]², that is, Inf_i[p] ≥ (32 √15 / (125 π^4)) ε^{5/2} / d^6.

In these theorems MainTheorem and MainTheoremImproved are hypotheses; Chain.lean proves the first with no hypothesis and the second from the hypothesis RowBound.

The last section treats the real power ε^{5/2} and the bit encoding of ExplicitBoundPM, as Conjecture.lean writes the power and the encoding: ε ^ ((5 : ℝ) / 2) equals ε² √ε (rpow_five_halves), and pmt_sq_of_mainTheorem, pmt_sqrt_of_mainTheorem are the bounds on the cube {-1,1}^n with true ↦ 1 and false ↦ -1 (evPMt), obtained from pm_sq_of_mainTheorem and pm_sqrt_of_mainTheorem by negating every bit.

noncomputable def AaronsonAmbainis.Bridge.Ex {N : ℕ} (F : (Fin N → Bool) → ℝ) : ℝ

Uniform expectation over {0,1}^N, spelled out.

Equations

• AaronsonAmbainis.Bridge.Ex F = (∑ X : Fin N → Bool, F X) / 2 ^ N

def AaronsonAmbainis.Bridge.flipBit {N : ℕ} (X : Fin N → Bool) (i : Fin N) : Fin N → Bool

X with the i-th bit flipped, spelled out (X^i in the sources).

Equations

• AaronsonAmbainis.Bridge.flipBit X i = Function.update X i !X i

noncomputable def AaronsonAmbainis.Bridge.ev01 {N : ℕ} (p : MvPolynomial (Fin N) ℝ) (X : Fin N → Bool) : ℝ

The value of the polynomial p at the 0/1 point X ∈ {0,1}^N.

Equations

• AaronsonAmbainis.Bridge.ev01 p X = (MvPolynomial.eval fun (i : Fin N) => if X i = true then 1 else 0) p

noncomputable def AaronsonAmbainis.Bridge.evPM {N : ℕ} (p : MvPolynomial (Fin N) ℝ) (X : Fin N → Bool) : ℝ

The value of the polynomial p at the ±1 point attached to X (true ↦ −1).

Equations

• AaronsonAmbainis.Bridge.evPM p X = (MvPolynomial.eval fun (i : Fin N) => if X i = true then -1 else 1) p

mean, variance, inflR, flipSet of Defs.lean are the spelled-out notions

theorem AaronsonAmbainis.Bridge.mean_eq_Ex {N : ℕ} (F : Cube (Fin N) → ℝ) : mean F = Ex F

theorem AaronsonAmbainis.Bridge.flipSet_singleton_eq_flipBit {N : ℕ} (X : Cube (Fin N)) (i : Fin N) : flipSet X {i} = flipBit X i

theorem AaronsonAmbainis.Bridge.variance_eq_Ex {N : ℕ} (F : Cube (Fin N) → ℝ) : variance F = Ex fun (X : Fin N → Bool) => (F X - Ex F) ^ 2

theorem AaronsonAmbainis.Bridge.inflR_eq_Ex {N : ℕ} (F : Cube (Fin N) → ℝ) (i : Fin N) : inflR F i = Ex fun (X : Fin N → Bool) => ((F X - F (flipBit X i)) / 2) ^ 2

theorem AaronsonAmbainis.Bridge.Ex_nonneg {N : ℕ} {F : (Fin N → Bool) → ℝ} (hF : ∀ (X : Fin N → Bool), 0 ≤ F X) : 0 ≤ Ex F

Bounds of the kind of the main theorem, for polynomials

def AaronsonAmbainis.Bridge.MainBound (C : ℝ) : Prop

A bound of the kind of the main theorem, with the constant C: every f on the cube with |f| ≤ 1, degree at most d and positive variance has a coordinate j with 3 Var(f)^5 ≤ C d^12 Inf_j(f)². MainTheorem is MainBound (50000 * π^8), and MainTheoremImproved is MainBound (3125 * π^8).

Equations

• One or more equations did not get rendered due to their size.

theorem AaronsonAmbainis.Bridge.mainBound_of_mainTheorem (h : MainTheorem) : MainBound (50000 * Real.pi ^ 8)

theorem AaronsonAmbainis.Bridge.mainBound_of_mainTheoremImproved (h : MainTheoremImproved) : MainBound (3125 * Real.pi ^ 8)

theorem AaronsonAmbainis.Bridge.zero_one_of_mainBound {C : ℝ} (h : MainBound C) {ι : Type} [Fintype ι] [DecidableEq ι] (d : ℕ) (P : Cube ι → ℝ) (hrange : ∀ (X : Cube ι), 0 ≤ P X ∧ P X ≤ 1) (hdeg : HasDegreeLE P d) (hpos : 0 < variance P) : ∃ (i : ι), 3072 * variance P ^ 5 ≤ C * ↑d ^ 12 * ((∑ X : Cube ι, (P X - P (flipSet X {i})) ^ 2) / 2 ^ Fintype.card ι) ^ 2

A bound of the kind of the main theorem, translated to [0,1]-valued functions P (apply it to 1 − 2P), with the unnormalised L2 influence E[(P(X) − P(X^i))²] of Aaronson–Ambainis on the right: 3072 Var[P]^5 ≤ C d^12 Inf_i[P]².

theorem AaronsonAmbainis.Bridge.zo_of_mainBound {C : ℝ} (h : MainBound C) (N d : ℕ) (p : MvPolynomial (Fin N) ℝ) (hp : p.totalDegree ≤ d) (hrange : ∀ (X : Fin N → Bool), 0 ≤ ev01 p X ∧ ev01 p X ≤ 1) (ε : ℝ) (hε : 0 < ε) (hvar : (Ex fun (X : Fin N → Bool) => (ev01 p X - Ex (ev01 p)) ^ 2) ≥ ε) : ∃ (i : Fin N), 3072 * ε ^ 5 ≤ C * ↑d ^ 12 * (Ex fun (X : Fin N → Bool) => (ev01 p X - ev01 p (flipBit X i)) ^ 2) ^ 2

A bound of the kind of the main theorem for polynomials on the cube {0,1}^N with values in [0,1]: 3072 ε^5 ≤ C d^12 Inf_i[p]².

theorem AaronsonAmbainis.Bridge.pm_of_mainBound {C : ℝ} (h : MainBound C) (n d : ℕ) (p : MvPolynomial (Fin n) ℝ) (hp : p.totalDegree ≤ d) (hbd : ∀ (X : Fin n → Bool), |evPM p X| ≤ 1) (ε : ℝ) (hε : 0 < ε) (hvar : (Ex fun (X : Fin n → Bool) => (evPM p X - Ex (evPM p)) ^ 2) ≥ ε) : ∃ (i : Fin n), 3 * ε ^ 5 ≤ C * ↑d ^ 12 * (Ex fun (X : Fin n → Bool) => ((evPM p X - evPM p (flipBit X i)) / 2) ^ 2) ^ 2

A bound of the kind of the main theorem for polynomials on the cube {1,-1}^n which are bounded by 1: 3 ε^5 ≤ C d^12 Inf_i(p)².

theorem AaronsonAmbainis.Bridge.zo_hyps_force (N d : ℕ) (p : MvPolynomial (Fin N) ℝ) (hp : p.totalDegree ≤ d) (hrange : ∀ (X : Fin N → Bool), 0 ≤ ev01 p X ∧ ev01 p X ≤ 1) (ε : ℝ) (hε : 0 < ε) (hvar : (Ex fun (X : Fin N → Bool) => (ev01 p X - Ex (ev01 p)) ^ 2) ≥ ε) : 1 ≤ ↑d ∧ ε ≤ 1 / 4

Under the hypotheses of the statements on the cube {0,1}^N: d ≥ 1 and ε ≤ 1/4.

theorem AaronsonAmbainis.Bridge.pm_hyps_force (n d : ℕ) (p : MvPolynomial (Fin n) ℝ) (hp : p.totalDegree ≤ d) (ε : ℝ) (hε : 0 < ε) (hvar : (Ex fun (X : Fin n → Bool) => (evPM p X - Ex (evPM p)) ^ 2) ≥ ε) : 1 ≤ ↑d

Under the hypotheses of the statement on the cube {1,-1}^n, in the encoding of evPM: d ≥ 1.

The arithmetic of the printed forms

theorem AaronsonAmbainis.Bridge.sqrt_form_iff {c₁ c₂ k m ε D I : ℝ} (hc₁ : 0 ≤ c₁) (hc₂ : 0 < c₂) (hm : 0 < m) (hkm : 15 * c₁ ^ 2 * m = k * c₂ ^ 2) (hε : 0 ≤ ε) (hD : 0 < D) (hI : 0 ≤ I) : c₁ * √15 / (c₂ * Real.pi ^ 4) * (ε ^ 2 * √ε) / D ^ 6 ≤ I ↔ k * ε ^ 5 ≤ m * Real.pi ^ 8 * D ^ 12 * I ^ 2

A bound without square roots and its printed form: if ε, I, c₁ ≥ 0, D, c₂, m > 0 and 15 c₁² m = k c₂², then I ≥ (c₁ √15 / (c₂ π^4)) ε^{5/2} / D^6 if and only if k ε^5 ≤ m π^8 D^12 I². The power ε^{5/2} is written ε² √ε.

theorem AaronsonAmbainis.Bridge.ratio_pow_le {ε D I : ℝ} (hε : 0 < ε) (hε4 : ε ≤ 1 / 4) (hD : 1 ≤ D) (hI : 0 ≤ I) (h : 192 * ε ^ 5 ≤ 3125 * Real.pi ^ 8 * D ^ 12 * I ^ 2) : (ε / D) ^ 7 ≤ I

If 192 ε^5 ≤ 3125 π^8 D^12 I² with 0 < ε ≤ 1/4, D ≥ 1 and I ≥ 0, then (ε/D)^7 ≤ I: indeed 3125 π^8 ε^9 ≤ 192 for ε ≤ 1/4, and D^12 ≤ D^14.

The form on the cube {1,-1}^n, from MainTheorem

theorem AaronsonAmbainis.Bridge.pm_sq_of_mainTheorem (h : MainTheorem) (n d : ℕ) (p : MvPolynomial (Fin n) ℝ) (hp : p.totalDegree ≤ d) (hbd : ∀ (X : Fin n → Bool), |evPM p X| ≤ 1) (ε : ℝ) (hε : 0 < ε) (hvar : (Ex fun (X : Fin n → Bool) => (evPM p X - Ex (evPM p)) ^ 2) ≥ ε) : ∃ (i : Fin n), 3 * ε ^ 5 ≤ 50000 * Real.pi ^ 8 * ↑d ^ 12 * (Ex fun (X : Fin n → Bool) => ((evPM p X - evPM p (flipBit X i)) / 2) ^ 2) ^ 2

3 ε^5 ≤ 50000 π^8 d^12 Inf_i(p)², from MainTheorem.

theorem AaronsonAmbainis.Bridge.pm_sqrt_of_mainTheorem (h : MainTheorem) (n d : ℕ) (p : MvPolynomial (Fin n) ℝ) (hp : p.totalDegree ≤ d) (hbd : ∀ (X : Fin n → Bool), |evPM p X| ≤ 1) (ε : ℝ) (hε : 0 < ε) (hvar : (Ex fun (X : Fin n → Bool) => (evPM p X - Ex (evPM p)) ^ 2) ≥ ε) : ∃ (i : Fin n), (Ex fun (X : Fin n → Bool) => ((evPM p X - evPM p (flipBit X i)) / 2) ^ 2) ≥ √15 / (500 * Real.pi ^ 4) * (ε ^ 2 * √ε) / ↑d ^ 6

Inf_i(p) ≥ (√15 / (500 π^4)) ε^{5/2} / d^6, from MainTheorem.

The conjecture, from MainTheorem

theorem AaronsonAmbainis.Bridge.zo_sq_of_mainTheorem (h : MainTheorem) (N d : ℕ) (p : MvPolynomial (Fin N) ℝ) (hp : p.totalDegree ≤ d) (hrange : ∀ (X : Fin N → Bool), 0 ≤ ev01 p X ∧ ev01 p X ≤ 1) (ε : ℝ) (hε : 0 < ε) (hvar : (Ex fun (X : Fin N → Bool) => (ev01 p X - Ex (ev01 p)) ^ 2) ≥ ε) : ∃ (i : Fin N), 192 * ε ^ 5 ≤ 3125 * Real.pi ^ 8 * ↑d ^ 12 * (Ex fun (X : Fin N → Bool) => (ev01 p X - ev01 p (flipBit X i)) ^ 2) ^ 2

192 ε^5 ≤ 3125 π^8 d^12 Inf_i[p]², from MainTheorem.

theorem AaronsonAmbainis.Bridge.zo_sqrt_of_mainTheorem (h : MainTheorem) (N d : ℕ) (p : MvPolynomial (Fin N) ℝ) (hp : p.totalDegree ≤ d) (hrange : ∀ (X : Fin N → Bool), 0 ≤ ev01 p X ∧ ev01 p X ≤ 1) (ε : ℝ) (hε : 0 < ε) (hvar : (Ex fun (X : Fin N → Bool) => (ev01 p X - Ex (ev01 p)) ^ 2) ≥ ε) : ∃ (i : Fin N), (Ex fun (X : Fin N → Bool) => (ev01 p X - ev01 p (flipBit X i)) ^ 2) ≥ 8 * √15 / (125 * Real.pi ^ 4) * (ε ^ 2 * √ε) / ↑d ^ 6

Inf_i[p] ≥ (8 √15 / (125 π^4)) ε^{5/2} / d^6, from MainTheorem.

theorem AaronsonAmbainis.Bridge.zo_pow_of_mainTheorem (h : MainTheorem) (N d : ℕ) (p : MvPolynomial (Fin N) ℝ) (hp : p.totalDegree ≤ d) (hrange : ∀ (X : Fin N → Bool), 0 ≤ ev01 p X ∧ ev01 p X ≤ 1) (ε : ℝ) (hε : 0 < ε) (hvar : (Ex fun (X : Fin N → Bool) => (ev01 p X - Ex (ev01 p)) ^ 2) ≥ ε) : ∃ (i : Fin N), (Ex fun (X : Fin N → Bool) => (ev01 p X - ev01 p (flipBit X i)) ^ 2) ≥ (ε / ↑d) ^ 7

Inf_i[p] ≥ (ε/d)^7, from MainTheorem.

The conjecture with the constant of MainTheoremImproved

theorem AaronsonAmbainis.Bridge.zo_sq_of_mainTheoremImproved (h : MainTheoremImproved) (N d : ℕ) (p : MvPolynomial (Fin N) ℝ) (hp : p.totalDegree ≤ d) (hrange : ∀ (X : Fin N → Bool), 0 ≤ ev01 p X ∧ ev01 p X ≤ 1) (ε : ℝ) (hε : 0 < ε) (hvar : (Ex fun (X : Fin N → Bool) => (ev01 p X - Ex (ev01 p)) ^ 2) ≥ ε) : ∃ (i : Fin N), 3072 * ε ^ 5 ≤ 3125 * Real.pi ^ 8 * ↑d ^ 12 * (Ex fun (X : Fin N → Bool) => (ev01 p X - ev01 p (flipBit X i)) ^ 2) ^ 2

3072 ε^5 ≤ 3125 π^8 d^12 Inf_i[p]², from MainTheoremImproved.

theorem AaronsonAmbainis.Bridge.zo_sqrt_of_mainTheoremImproved (h : MainTheoremImproved) (N d : ℕ) (p : MvPolynomial (Fin N) ℝ) (hp : p.totalDegree ≤ d) (hrange : ∀ (X : Fin N → Bool), 0 ≤ ev01 p X ∧ ev01 p X ≤ 1) (ε : ℝ) (hε : 0 < ε) (hvar : (Ex fun (X : Fin N → Bool) => (ev01 p X - Ex (ev01 p)) ^ 2) ≥ ε) : ∃ (i : Fin N), (Ex fun (X : Fin N → Bool) => (ev01 p X - ev01 p (flipBit X i)) ^ 2) ≥ 32 * √15 / (125 * Real.pi ^ 4) * (ε ^ 2 * √ε) / ↑d ^ 6

Inf_i[p] ≥ (32 √15 / (125 π^4)) ε^{5/2} / d^6, from MainTheoremImproved.

The power 5/2 and the encoding of ExplicitBoundPM

Conjecture.lean writes the power ε^{5/2} as the real power ε ^ ((5 : ℝ) / 2), and ε ^ ((5 : ℝ) / 2) = ε² √ε for ε ≥ 0 (rpow_five_halves). The statement ExplicitBoundPM of Conjecture.lean, on the cube {-1,1}^n, encodes the bit true as 1 and the bit false as -1 (evPMt), while evPM, like Defs.lean, sends true to -1. Negating every bit (negBits) is a bijection of the cube: evPMt p X = evPM p (negBits X), and negBits commutes with the bit flips, so evPMt p and evPM p have the same expectation, the same variance and the same influences.

theorem AaronsonAmbainis.Bridge.rpow_five_halves {ε : ℝ} (hε : 0 ≤ ε) : ε ^ (5 / 2) = ε ^ 2 * √ε

The real power ε^{5/2} is ε² √ε.

noncomputable def AaronsonAmbainis.Bridge.evPMt {N : ℕ} (p : MvPolynomial (Fin N) ℝ) (X : Fin N → Bool) : ℝ

The value of the polynomial p at the ±1 point attached to X with true ↦ 1 and false ↦ -1, the encoding of ExplicitBoundPM.

Equations

• AaronsonAmbainis.Bridge.evPMt p X = (MvPolynomial.eval fun (i : Fin N) => if X i = true then 1 else -1) p

def AaronsonAmbainis.Bridge.negBits {N : ℕ} (X : Fin N → Bool) : Fin N → Bool

Every bit of X negated.

Equations

• AaronsonAmbainis.Bridge.negBits X i = !X i

theorem AaronsonAmbainis.Bridge.negBits_negBits {N : ℕ} (X : Fin N → Bool) : negBits (negBits X) = X

def AaronsonAmbainis.Bridge.negBitsEquiv (N : ℕ) : (Fin N → Bool) ≃ (Fin N → Bool)

Negating every bit, as a bijection of the cube.

Equations

• AaronsonAmbainis.Bridge.negBitsEquiv N = { toFun := AaronsonAmbainis.Bridge.negBits, invFun := AaronsonAmbainis.Bridge.negBits, left_inv := ⋯, right_inv := ⋯ }

theorem AaronsonAmbainis.Bridge.Ex_comp_negBits {N : ℕ} (F : (Fin N → Bool) → ℝ) : (Ex fun (X : Fin N → Bool) => F (negBits X)) = Ex F

theorem AaronsonAmbainis.Bridge.negBits_flipBit {N : ℕ} (X : Fin N → Bool) (i : Fin N) : negBits (flipBit X i) = flipBit (negBits X) i

theorem AaronsonAmbainis.Bridge.evPMt_eq {N : ℕ} (p : MvPolynomial (Fin N) ℝ) (X : Fin N → Bool) : evPMt p X = evPM p (negBits X)

theorem AaronsonAmbainis.Bridge.evPMt_bound_iff {N : ℕ} (p : MvPolynomial (Fin N) ℝ) : (∀ (X : Fin N → Bool), |evPMt p X| ≤ 1) ↔ ∀ (X : Fin N → Bool), |evPM p X| ≤ 1

theorem AaronsonAmbainis.Bridge.Ex_evPMt {N : ℕ} (p : MvPolynomial (Fin N) ℝ) : Ex (evPMt p) = Ex (evPM p)

theorem AaronsonAmbainis.Bridge.variance_evPMt {N : ℕ} (p : MvPolynomial (Fin N) ℝ) : (Ex fun (X : Fin N → Bool) => (evPMt p X - Ex (evPMt p)) ^ 2) = Ex fun (X : Fin N → Bool) => (evPM p X - Ex (evPM p)) ^ 2

theorem AaronsonAmbainis.Bridge.infl_evPMt {N : ℕ} (p : MvPolynomial (Fin N) ℝ) (i : Fin N) : (Ex fun (X : Fin N → Bool) => ((evPMt p X - evPMt p (flipBit X i)) / 2) ^ 2) = Ex fun (X : Fin N → Bool) => ((evPM p X - evPM p (flipBit X i)) / 2) ^ 2

theorem AaronsonAmbainis.Bridge.pmt_sq_of_mainTheorem (h : MainTheorem) (n d : ℕ) (p : MvPolynomial (Fin n) ℝ) (hp : p.totalDegree ≤ d) (hbd : ∀ (X : Fin n → Bool), |evPMt p X| ≤ 1) (ε : ℝ) (hε : 0 < ε) (hvar : (Ex fun (X : Fin n → Bool) => (evPMt p X - Ex (evPMt p)) ^ 2) ≥ ε) : ∃ (i : Fin n), 3 * ε ^ 5 ≤ 50000 * Real.pi ^ 8 * ↑d ^ 12 * (Ex fun (X : Fin n → Bool) => ((evPMt p X - evPMt p (flipBit X i)) / 2) ^ 2) ^ 2

3 ε^5 ≤ 50000 π^8 d^12 Inf_i(p)² on {-1,1}^n with true ↦ 1, from MainTheorem.

theorem AaronsonAmbainis.Bridge.pmt_sqrt_of_mainTheorem (h : MainTheorem) (n d : ℕ) (p : MvPolynomial (Fin n) ℝ) (hp : p.totalDegree ≤ d) (hbd : ∀ (X : Fin n → Bool), |evPMt p X| ≤ 1) (ε : ℝ) (hε : 0 < ε) (hvar : (Ex fun (X : Fin n → Bool) => (evPMt p X - Ex (evPMt p)) ^ 2) ≥ ε) : ∃ (i : Fin n), (Ex fun (X : Fin n → Bool) => ((evPMt p X - evPMt p (flipBit X i)) / 2) ^ 2) ≥ √15 / (500 * Real.pi ^ 4) * (ε ^ 2 * √ε) / ↑d ^ 6

Inf_i(p) ≥ (√15 / (500 π^4)) ε^{5/2} / d^6 on {-1,1}^n with true ↦ 1, from MainTheorem, with the power 5/2 written ε² √ε.