Interface for the proof of the row bound

The row bound of Agarwal and Ben-David (RowBound in Statements.lean) enters Chain.lean as a named hypothesis. This file states the links of the proof of the row bound of the paper (Section 6: cost at most π² d² for functions with values in [-1,1], where the bound of Agarwal and Ben-David gives π² d² / 2), which has no hypothesis:

• MarkovEndpoint — A. A. Markov's inequality at an endpoint of the interval [0,2] (Lemma 6.1);
• BlockInequality — the block inequality for a family of blocks in which every coordinate lies in at most N blocks (Lemma 6.4);
• PackingBound — the packing bound, for fractional packings (Lemma 6.5);
• CoverDuality — linear-programming duality between packings and rows (Proposition 6.7);
• RowBoundPM — the row bound (Theorem 6.8).

Chain: MarkovEndpoint → BlockInequality → PackingBound, then PackingBound → CoverDuality → RowBoundPM. The block inequality also gives SensitivityBound (Statements.lean), and RowBoundPM and SensitivityBound enter the main theorem (MainTheorem.lean).

def AaronsonAmbainis.MarkovEndpoint : Prop

Markov's inequality at an endpoint: a real polynomial of degree at most D which is bounded by 1 in absolute value on [0,2] has |p'(0)| ≤ D².

Equations

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

def AaronsonAmbainis.BlockInequality : Prop

The block inequality. f is bounded by 1 and has degree at most d; S b (b : β) is a finite family of blocks such that every coordinate lies in at most N blocks; m ≥ 1 satisfies N (1 - cos (π / m)) ≤ 2. Then ∑_b |f(x) - f(x^{S b})| ≤ 4 d² m².

Equations

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

def AaronsonAmbainis.PackingBound : Prop

The packing bound. f is bounded by 1 and has degree at most d. If κ ≥ 0 and ∑_{S ∋ i} κ_S ≤ 1 for every coordinate i, then ∑_S κ_S |f(x) - f(x^S)| ≤ π² d².

Equations

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

def AaronsonAmbainis.CoverDuality : Prop

Duality between packings and rows: if every fractional packing κ has ∑_S κ_S t_S ≤ K, then there is a vector a ≥ 0 of total mass at most K with t_S ≤ a(S) for every S. (The hypotheses 0 ≤ K and t ∅ ≤ 0 follow from the hypothesis on packings: take κ = 0, and take κ with κ_∅ arbitrarily large and κ_S = 0 for S ≠ ∅.)

Equations

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

def AaronsonAmbainis.RowBoundPM : Prop

The row bound (Theorem 6.8 of the paper): a function with values in [-1,1] and of degree at most d has, at every point, a row of cost at most π² d².

Equations

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