The all-pairs inequality for one set F of free coordinates (allPairs_core)

Step 1 of the proof of Proposition 5.2 of the paper: the antipodal inequality (Theorem 4.3) applied to all subcubes with free coordinates F, added up:

∑ x, allPairsTerm g w lam F x ≤ ∑ j ∈ F, bdry g j / w j,

where allPairsTerm g w lam F x = (∑ j ∈ F, w j * lam x j * lam (x^F) j)⁻¹ if g x = true and g (x^F) = false, and 0 otherwise (the term T_F(x) of the paper).

The subcube through z with free coordinates F is parametrised by u ↦ glue F z u (u : Cube ι; the coordinates of u off F are dummies). The antipodal inequality is applied to u ↦ g (glue F z u) with the rows lam (glue F z u) restricted to F, for every z, and the results are added over all z; sum_sum_glue removes the multiplicity 2 ^ n.

noncomputable def AaronsonAmbainis.allPairsTerm {ι : Type u_1} [DecidableEq ι] (g : Cube ι → Bool) (w : ι → ℝ) (lam : Cube ι → ι → ℝ) (F : Finset ι) (x : Cube ι) : ℝ

The term T_F(x) of the paper: (∑ j ∈ F, w j * lam x j * lam (x^F) j)⁻¹ if g x = true and g (x^F) = false, and 0 otherwise.

Equations

• AaronsonAmbainis.allPairsTerm g w lam F x = if g x = true ∧ g (AaronsonAmbainis.flipSet x F) = false then (∑ j ∈ F, w j * lam x j * lam (AaronsonAmbainis.flipSet x F) j)⁻¹ else 0

theorem AaronsonAmbainis.isRow_glue {ι : Type u_1} [DecidableEq ι] {g : Cube ι → Bool} {lam : Cube ι → ι → ℝ} (hlam : ∀ (x : Cube ι), IsRow g x (lam x)) (F : Finset ι) (z u : Cube ι) : IsRow (fun (u : Cube ι) => g (glue F z u)) u fun (j : ι) => if j ∈ F then lam (glue F z u) j else 0

The restriction of a row to the free coordinates is a row of the restricted function.

theorem AaronsonAmbainis.sum_ite_ite_mem {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : Finset ι) (w a b : ι → ℝ) : (∑ j : ι, (w j * if j ∈ F then a j else 0) * if j ∈ F then b j else 0) = ∑ j ∈ F, w j * a j * b j

A sum of products of two restricted vectors is a sum over the restriction set.

theorem AaronsonAmbainis.zone_sum_glue {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (w : ι → ℝ) (lam : Cube ι → ι → ℝ) (F : Finset ι) (z : Cube ι) : ∑ u ∈ zone fun (u : Cube ι) => g (glue F z u), (∑ j : ι, (w j * if j ∈ F then lam (glue F z u) j else 0) * if j ∈ F then lam (glue F z (antipode u)) j else 0)⁻¹ = ∑ u : Cube ι, allPairsTerm g w lam F (glue F z u)

The left side of the antipodal inequality for the restricted function, in terms of allPairsTerm.

theorem AaronsonAmbainis.bdry_eq_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : ↑(bdry g j) = ∑ x : Cube ι, if g x = true ∧ g (flipSet x {j}) = false then 1 else 0

bdry as a real sum of indicators.

theorem AaronsonAmbainis.bdry_glue_of_not_mem {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) {F : Finset ι} {j : ι} (hj : j ∉ F) (z : Cube ι) : bdry (fun (u : Cube ι) => g (glue F z u)) j = 0

A coordinate that is not free has no bichromatic edge in the subcube.

theorem AaronsonAmbainis.sum_bdry_glue_of_mem {ι : Type u_1} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) {F : Finset ι} {j : ι} (hj : j ∈ F) : ∑ z : Cube ι, ↑(bdry (fun (u : Cube ι) => g (glue F z u)) j) = 2 ^ Fintype.card ι * ↑(bdry g j)

A free coordinate: the bichromatic j-edges of all subcubes with free coordinates F are the bichromatic j-edges of g, each 2 ^ n times.

theorem AaronsonAmbainis.allPairs_core (hAntipodal : AntipodalInequality) {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (w : ι → ℝ) (hw : ∀ (j : ι), 0 < w j) (lam : Cube ι → ι → ℝ) (hlam : ∀ (x : Cube ι), IsRow g x (lam x)) (F : Finset ι) : ∑ x : Cube ι, allPairsTerm g w lam F x ≤ ∑ j ∈ F, ↑(bdry g j) / w j

The inequality for one set F of free coordinates (Step 1 of the proof of Proposition 5.2 of the paper), from the antipodal inequality.