The theorems for functions of bounded degree, from the links

A function f on the cube with |f| ≤ 1 and degree at most d has a row of cost at most π² d² at every point (RowBoundPM, Theorem 6.8 of the paper), and ∑_j |f(x) - f(x^j)| ≤ 4 d² at every point x (SensitivityBound, Corollary 6.10). With these two inputs:

• mainTheorem_of_influence : InfluenceBound → SensitivityBound → RowBoundPM → MainTheorem — the main theorem (Theorem 1.1 of the paper). The bound for the influences (Theorem 8.3) with K = π² d² and L(f) ≤ 4 d² reads 3 Var(f)^5 ≤ 3125 (4 d²)² (π² d²)^4 Inf_j(f)² = 50000 π^8 d^12 Inf_j(f)².
• meanIncrementDegree_of_meanIncrement : MeanIncrementBound → RowBoundPM → MeanIncrementDegreeBound — the bound for the mean absolute increments (Theorem 7.10) with K = π² d², which is Corollary 7.11 of the paper: Var(f)^3 ≤ 36 (π² d²)^4 L_j(f)² = 36 π^8 d^8 L_j(f)².
• mainTheoremImproved_of_influence : InfluenceBound → SensitivityBound → RowBound → MainTheoremImproved — the main theorem with the constant 3125 π^8 in place of 50000 π^8 (Remark 8.4 of the paper). Its hypothesis RowBound is the row bound of Agarwal and Ben-David (Theorem 1.7 of arXiv:2410.19062), which is not proved in this project; it gives rows of cost at most π² d² / 2 (rows_of_rowBound), and 3125 (4 d²)² (π² d² / 2)^4 = 3125 π^8 d^12.

theorem AaronsonAmbainis.mainTheorem_of_influence : InfluenceBound → SensitivityBound → RowBoundPM → MainTheorem

The main theorem (Theorem 1.1 of the paper) from the bound for the influences (Theorem 8.3), the sensitivity bound (Corollary 6.10) and the row bound (Theorem 6.8).

theorem AaronsonAmbainis.meanIncrementDegree_of_meanIncrement : MeanIncrementBound → RowBoundPM → MeanIncrementDegreeBound

The bound for the mean absolute increments of a bounded function of degree at most d (Corollary 7.11 of the paper), from the bound for functions with rows of cost at most K (Theorem 7.10) and the row bound (Theorem 6.8).

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

The row bound of Agarwal and Ben-David (the hypothesis RowBound) for a function f with values in [-1,1]: applied to (1 + f)/2, with the weights doubled, it gives rows of f of cost at most π² d² / 2.

theorem AaronsonAmbainis.mainTheoremImproved_of_influence : InfluenceBound → SensitivityBound → RowBound → MainTheoremImproved

The main theorem with the constant that the row bound of Agarwal and Ben-David gives (Remark 8.4 of the paper), from the bound for the influences, the sensitivity bound and the hypothesis RowBound.