The chain

This file chains the links of the proof of the paper: every theorem below is one implication, applied to theorems that precede it.

Boolean functions (directories DetLow, DetBij, TwoSided):

• detInequality — the determinant inequality (Corollary 3.2), in DetTheorem.lean;
• antipodal_of_det — the antipodal inequality (Theorem 4.3);
• allPairs_of_antipodal — the all-pairs inequality (Proposition 5.2);
• twoSided_of_allPairs — the two-sided inequality (Theorem 5.4).

Real functions with a row of cost at most K at every point (directories Level, Average):

• integratedAllPairs_of_allPairs — the integrated all-pairs inequality (Proposition 7.4);
• thirdMoment_of_integratedAllPairs — the third-moment inequality (Theorem 7.6);
• meanIncrement_of_thirdMoment — the bound for the mean absolute increments (Theorem 7.10);
• influence_of_meanIncrement — the bound for the influences (Theorem 8.3).

Bounded functions of degree at most d (directories Row, Pack, Dual):

• blockInequality — the block inequality (Lemma 6.4), in Row/Main.lean;
• sensitivity_of_block — the sensitivity bound at every point (Corollary 6.10);
• packingBound_of_block — the packing bound (Lemma 6.5);
• rowBoundPM_of_packing — the row bound (Theorem 6.8: rows of cost at most π² d²).

The theorems for bounded functions of degree at most d (MainTheorem.lean):

• mainTheorem_of_influence — the main theorem (Theorem 1.1);
• meanIncrementDegree_of_meanIncrement — the bound for the mean absolute increments (Corollary 7.11);
• mainTheoremImproved_of_influence — the main theorem with the constant that the row bound of Agarwal and Ben-David gives (Remark 8.4).

All theorems of this file except the last one have no hypothesis. The hypothesis of the last one, mainTheoremImproved_of_rowBound : RowBound → MainTheoremImproved, is RowBound, the row bound of Agarwal and Ben-David (Theorem 1.7 of arXiv:2410.19062), which is not proved in this project. The two-sided inequality is a result of the paper in its own right; the main theorem does not use it.

Boolean functions

theorem AaronsonAmbainis.antipodalInequality : AntipodalInequality

The antipodal inequality (the inequality of Theorem 4.3 of the paper), with no hypothesis.

theorem AaronsonAmbainis.allPairsInequality : AllPairsInequality

The all-pairs inequality (the inequality of Proposition 5.2 of the paper), with no hypothesis.

theorem AaronsonAmbainis.twoSidedInequality : TwoSidedInequality

The two-sided inequality (the inequality of Theorem 5.4 of the paper), with no hypothesis.

Real functions with a row at every point

theorem AaronsonAmbainis.integratedAllPairsInequality : IntegratedAllPairsInequality

The integrated all-pairs inequality (the inequality of Proposition 7.4 of the paper), with no hypothesis.

theorem AaronsonAmbainis.thirdMomentInequality : ThirdMomentInequality

The third-moment inequality (Theorem 7.6 of the paper), with no hypothesis.

theorem AaronsonAmbainis.meanIncrementBound : MeanIncrementBound

The bound for the mean absolute increments (Theorem 7.10 of the paper), with no hypothesis.

theorem AaronsonAmbainis.influenceBound : InfluenceBound

The bound for the influences (Theorem 8.3 of the paper), with no hypothesis.

Bounded functions of degree at most d

theorem AaronsonAmbainis.sensitivityBound : SensitivityBound

The sensitivity bound at every point (Corollary 6.10 of the paper), with no hypothesis.

theorem AaronsonAmbainis.packingBound : PackingBound

The packing bound (Lemma 6.5 of the paper), with no hypothesis.

theorem AaronsonAmbainis.rowBoundPM : RowBoundPM

The row bound (Theorem 6.8 of the paper: rows of cost at most π² d²), with no hypothesis.

The theorems for bounded functions of degree at most d

theorem AaronsonAmbainis.mainTheorem : MainTheorem

The main theorem (Theorem 1.1 of the paper), with no hypothesis.

theorem AaronsonAmbainis.meanIncrementDegreeBound : MeanIncrementDegreeBound

The bound for the mean absolute increments of a bounded function of degree at most d (Corollary 7.11 of the paper), with no hypothesis.

theorem AaronsonAmbainis.mainTheoremImproved_of_rowBound : RowBound → MainTheoremImproved

The row bound of Agarwal and Ben-David, which is a hypothesis here, implies the main theorem with the constant 3125 π^8 (Remark 8.4 of the paper).