The all-pairs inequality from the antipodal inequality (allPairs_of_antipodal)

Step 2 of the proof of Proposition 5.2 of the paper (all sets of free coordinates).

allPairs_core (file AllPairsCore.lean) is the sum of the antipodal inequality over all subcubes with a fixed set F of free coordinates. Here the inequalities allPairs_core are added over all F:

• left side: for fixed x, F ↦ x^F is a bijection from sets of coordinates to points, with inverse y ↦ diffSet x y (sum_allPairsTerm);
• right side: each coordinate lies in exactly half of all sets (two_mul_sum_finset_sum).

def AaronsonAmbainis.flipEquiv {ι : Type u_1} [Fintype ι] [DecidableEq ι] (x : Cube ι) : Finset ι ≃ Cube ι

For fixed x, F ↦ x^F is a bijection from sets of coordinates to points.

Equations

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

theorem AaronsonAmbainis.sum_allPairsTerm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (w : ι → ℝ) (lam : Cube ι → ι → ℝ) (x : Cube ι) : ∑ F : Finset ι, allPairsTerm g w lam F x = ∑ y : Cube ι, if g x = true ∧ g y = false then (∑ j ∈ diffSet x y, w j * lam x j * lam y j)⁻¹ else 0

The terms of x in all the inequalities allPairs_core are the terms of the pairs (x, y).

theorem AaronsonAmbainis.two_mul_sum_finset_sum {ι : Type u_1} [Fintype ι] (β : ι → ℝ) : 2 * ∑ F : Finset ι, ∑ j ∈ F, β j = 2 ^ Fintype.card ι * ∑ j : ι, β j

Each coordinate lies in exactly half of all sets.

theorem AaronsonAmbainis.allPairs_of_antipodal : AntipodalInequality → AllPairsInequality

The all-pairs inequality (the inequality of Proposition 5.2 of the paper, multiplied by 2) from the antipodal inequality (Theorem 4.3).