RowBound and Theorem 1.7 of arXiv:2410.19062 as printed

Source: A. Agarwal and S. Ben-David, Oracle separations for the quantum-classical polynomial hierarchy, arXiv:2410.19062 (version 2), Theorem 1.7:

Let f : {0,1}^n → [0,1] be a real-valued function which can be expressed as a polynomial of degree at most d. Then there is an assignment of weights {c_{x,i}}_{x∈{0,1}^n, i∈[n]} to inputs x and positions i ∈ [n] such that for all x, y ∈ {0,1}^n, we have ∑_{i : x_i ≠ y_i} c_{x,i} ≥ |f(x) - f(y)| and ∑_{i=1}^n c_{x,i} ≤ (π²/4) d².

FbsDegPrinted transcribes this sentence with Mathlib notions only (no definition of Defs.lean is used) and in its weakest reading: only n ≥ 1, only d ≥ 1, no sign condition on the weights in the conclusion. FbsDegPrintedML is the same with the narrowest reading of the hypothesis (a multilinear polynomial in the 0/1 variables with no monomial of size > d).

Result: RowBound ↔ FbsDegPrinted ↔ FbsDegPrintedML. So the hypothesis RowBound asks for nothing beyond the printed theorem. Also: a RowBound weight system is automatically nonnegative (weights_nonneg_of_row).

def AaronsonAmbainis.Bridge.PrintedConcl {n : ℕ} (f : (Fin n → Bool) → ℝ) (d : ℕ) : Prop

The conclusion of the printed theorem for one function, written with Mathlib notions only.

Equations

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

def AaronsonAmbainis.Bridge.FbsDegPrinted : Prop

Theorem 1.7 of arXiv:2410.19062 as printed, for n ≥ 1 and d ≥ 1 ("can be expressed as a polynomial of degree at most d": some real polynomial of total degree ≤ d agrees with f on {0,1}^n).

Equations

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

def AaronsonAmbainis.Bridge.FbsDegPrintedML : Prop

Theorem 1.7 of arXiv:2410.19062 with the narrowest reading of the hypothesis: f is a multilinear polynomial in the 0/1 variables with no monomial of size > d.

Equations

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

theorem AaronsonAmbainis.Bridge.printedConcl_iff {n : ℕ} (f : Cube (Fin n) → ℝ) (d : ℕ) : PrintedConcl f d ↔ ∃ (c : Cube (Fin n) → Fin n → ℝ), (∀ (x y : Cube (Fin n)), |f x - f y| ≤ ∑ i ∈ diffSet x y, c x i) ∧ ∀ (x : Cube (Fin n)), ∑ i : Fin n, c x i ≤ Real.pi ^ 2 / 4 * ↑d ^ 2

The printed conclusion is literally the conclusion of RowBound.

theorem AaronsonAmbainis.Bridge.printedConcl_of_const {n : ℕ} {f : (Fin n → Bool) → ℝ} (h : ∀ (x y : Fin n → Bool), f x = f y) (d : ℕ) : PrintedConcl f d

For a constant function the conclusion holds with zero weights, for every d.

theorem AaronsonAmbainis.Bridge.rowBoundFin_of_restricted (h : ∀ (n d : ℕ), 1 ≤ n → 1 ≤ d → ∀ (f : Cube (Fin n) → ℝ), (∀ (x : Cube (Fin n)), 0 ≤ f x ∧ f x ≤ 1) → HasDegreeLE f d → PrintedConcl f d) : RowBoundFin

The cases n = 0 and d = 0 of RowBoundFin are trivially true, so the statement restricted to n ≥ 1, d ≥ 1 already gives RowBoundFin.

theorem AaronsonAmbainis.Bridge.rowBound_of_printed (h : FbsDegPrinted) : RowBound

The printed theorem implies the hypothesis RowBound.

theorem AaronsonAmbainis.Bridge.rowBound_of_printedML (h : FbsDegPrintedML) : RowBound

The printed theorem in its narrowest reading implies the hypothesis RowBound.

theorem AaronsonAmbainis.Bridge.printed_of_rowBound (h : RowBound) : FbsDegPrinted

Conversely RowBound gives the printed theorem (so it says neither more nor less).

theorem AaronsonAmbainis.Bridge.printedML_of_rowBound (h : RowBound) : FbsDegPrintedML

theorem AaronsonAmbainis.Bridge.rowBound_iff_printed : RowBound ↔ FbsDegPrinted

RowBound is equivalent to Theorem 1.7 of arXiv:2410.19062 as printed.

theorem AaronsonAmbainis.Bridge.rowBound_iff_printedML : RowBound ↔ FbsDegPrintedML

RowBound is equivalent to the printed theorem in its narrowest reading.

theorem AaronsonAmbainis.Bridge.weights_nonneg_of_row {ι : Type u_1} [Fintype ι] {f : Cube ι → ℝ} {c : Cube ι → ι → ℝ} (h : ∀ (x y : Cube ι), |f x - f y| ≤ ∑ i ∈ diffSet x y, c x i) (x : Cube ι) (i : ι) : 0 ≤ c x i

Weights satisfying the first condition of RowBound are nonnegative (take y = x^i).

theorem AaronsonAmbainis.Bridge.rowBound_nonneg (h : RowBound) (ι : Type) [Fintype ι] (d : ℕ) (f : Cube ι → ℝ) (hf : ∀ (x : Cube ι), 0 ≤ f x ∧ f x ≤ 1) (hdeg : HasDegreeLE f d) : ∃ (c : Cube ι → ι → ℝ), (∀ (x : Cube ι) (i : ι), 0 ≤ c x i) ∧ (∀ (x y : Cube ι), |f x - f y| ≤ ∑ i ∈ diffSet x y, c x i) ∧ ∀ (x : Cube ι), ∑ i : ι, c x i ≤ Real.pi ^ 2 / 4 * ↑d ^ 2

So RowBound implies its own strengthening with nonnegative weights.