The antipodal inequality from the determinant inequality (antipodal_of_det)

The pointwise step (Lemma 4.2 of the paper) and the proof of the antipodal inequality (Theorem 4.3) from the determinant inequality (Corollary 3.2).

With ℓ j = 1 / w j, x = lam u, y = lam (antipode u), S = ∑ j, w j * x j * y j and D = S⁻¹ (Lean: 0⁻¹ = 0), the wing at u is wingSet w x y: empty if S = 0, and {j : ℓ j < D * y j} otherwise. (By the overlap lemma, Lemma 4.1 of the paper, S > 0 on the zone; the case S = 0 is treated directly here, so that the overlap lemma is not needed in this file.)

theorem AaronsonAmbainis.wing_of_row {ι : Type u_1} [Fintype ι] [DecidableEq ι] {g : Cube ι → Bool} {u : Cube ι} {x y w : ι → ℝ} (hu : g u = true) (hw : ∀ (j : ι), 0 < w j) (hx : IsRow g u x) (hy : ∀ (j : ι), 0 ≤ y j) (hpos : 0 < ∑ j : ι, w j * x j * y j) : IsWing g u {j : ι | (w j)⁻¹ < (∑ j : ι, w j * x j * y j)⁻¹ * y j}

Steps 1 and 2 of the proof of Lemma 4.2 of the paper: if x is a row at u, g u = true and S = ∑ j, w j * x j * y j > 0, then {j : 1 / w j < S⁻¹ * y j} is a 1-wing at u.

theorem AaronsonAmbainis.lower_of_row {ι : Type u_1} [DecidableEq ι] {g : Cube ι → Bool} {u' : Cube ι} {y ℓ : ι → ℝ} {D : ℝ} (hD : 0 ≤ D) (hy : IsRow g u' y) (hu' : g u' = false) (G : Finset ι) (hG : ∀ j ∈ G, D * y j ≤ ℓ j) (hgG : g (flipSet u' G) = true) : D ≤ ∑ j ∈ G, ℓ j

Step 3 of the proof of Lemma 4.2 of the paper: if y is a row at u', g u' = false, g (u'^G) = true and D * y j ≤ ℓ j on G, then D ≤ ℓ(G).

noncomputable def AaronsonAmbainis.wingSet {ι : Type u_1} [Fintype ι] (w x y : ι → ℝ) : Finset ι

The wing used at a point with rows x (at the point) and y (at its antipode).

Equations

• AaronsonAmbainis.wingSet w x y = if ∑ j : ι, w j * x j * y j = 0 then ∅ else {j : ι | (w j)⁻¹ < (∑ j : ι, w j * x j * y j)⁻¹ * y j}

theorem AaronsonAmbainis.wingSet_isWing {ι : Type u_1} [Fintype ι] [DecidableEq ι] {g : Cube ι → Bool} {u : Cube ι} {x y w : ι → ℝ} (hu : g u = true) (hw : ∀ (j : ι), 0 < w j) (hx : IsRow g u x) (hy : ∀ (j : ι), 0 ≤ y j) : IsWing g u (wingSet w x y)

theorem AaronsonAmbainis.wingSet_lower {ι : Type u_1} [Fintype ι] [DecidableEq ι] {g : Cube ι → Bool} {u' : Cube ι} {x y w : ι → ℝ} (hw : ∀ (j : ι), 0 < w j) (hx : ∀ (j : ι), 0 ≤ x j) (hy : IsRow g u' y) (hu' : g u' = false) (G : Finset ι) (hG : Disjoint G (wingSet w x y)) (hgG : g (flipSet u' G) = true) : (∑ j : ι, w j * x j * y j)⁻¹ ≤ ∑ j ∈ G, (w j)⁻¹

theorem AaronsonAmbainis.antipodal_of_det : DetInequality → AntipodalInequality

The antipodal inequality (the inequality of Theorem 4.3 of the paper) from the determinant inequality (Corollary 3.2).