DetBij / Main: LowestUnit → LowestBound → DetInequality

The determinant inequality (Corollary 3.2 of the paper) from the two interface propositions of AaronsonAmbainis.DetDefs, through the bijection theorem in the form of Perm.lean. The argument is the proof of Corollary 3.2 from Theorem 3.1 in the paper.

def AaronsonAmbainis.DetBij.extWing {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (A : Cube ι → Finset ι) (x : Cube ι) : Finset ι

The wings extended to all points: A x on zone g, the empty set elsewhere.

Equations

• AaronsonAmbainis.DetBij.extWing g A x = if x ∈ AaronsonAmbainis.zone g then A x else ∅

theorem AaronsonAmbainis.DetBij.extWing_of_mem {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (A : Cube ι → Finset ι) {x : Cube ι} (hx : x ∈ zone g) : extWing g A x = A x

theorem AaronsonAmbainis.DetBij.extWing_of_notMem {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (A : Cube ι → Finset ι) {x : Cube ι} (hx : x ∉ zone g) : extWing g A x = ∅

theorem AaronsonAmbainis.DetBij.isWing_extWing {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (A : Cube ι → Finset ι) (hA : ∀ u ∈ zone g, IsWing g u (A u)) (x : Ones g) : IsWing g (↑x) (extWing g A ↑x)

The extended wings are 1-wings at every one of g (the empty set is a 1-wing).

theorem AaronsonAmbainis.DetBij.det_inequality_of_perm {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (ℓ : ι → ℝ) (hℓ : ∀ (j : ι), 0 < ℓ j) (A : Cube ι → Finset ι) (d : Cube ι → ℝ) (hd : ∀ u ∈ zone g, ∀ (G : Finset ι), Disjoint G (A u) → g (flipSet (antipode u) G) = true → d u ≤ ∑ j ∈ G, ℓ j) (σ : Equiv.Perm (Ones g)) (hσ : ∀ (x : Ones g), Disjoint (agSet ↑(σ x) ↑x) (extWing g A ↑(σ x))) (hcard : ∀ (j : ι), {x : Ones g | ↑(σ x) j = ↑x j}.card ≤ bdry g j) : ∑ u ∈ zone g, d u ≤ ∑ j : ι, ℓ j * ↑(bdry g j)

The weighted inequality for one instance, from a permutation as in exists_perm.

theorem AaronsonAmbainis.DetBij.detInequality_of_lowest : LowestUnit → LowestBound → DetInequality

The determinant inequality (Corollary 3.2 of the paper) from LowestUnit and LowestBound.