DetLow: basic definitions

Up g j is the set of ones x of g with x j = true whose j-neighbour is also a one (the upper endpoints of the j-edges inside the ones of g); its cardinality is the number e_j of Section 3.3 of the paper. (With the identification true ↦ -1 of Defs.lean, the set Up_j of the paper consists of the other endpoints of the same edges; it is Dn g j of Count.lean, and it has the same cardinality.)

def AaronsonAmbainis.DetLow.Up {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : Finset (Ones g)

The upper endpoints of the j-edges inside the ones of g.

Equations

• AaronsonAmbainis.DetLow.Up g j = {x : AaronsonAmbainis.Ones g | ↑x j = true ∧ g (AaronsonAmbainis.flipSet ↑x {j}) = true}

theorem AaronsonAmbainis.DetLow.mem_Up {ι : Type} [Fintype ι] [DecidableEq ι] {g : Cube ι → Bool} {j : ι} {x : Ones g} : x ∈ Up g j ↔ ↑x j = true ∧ g (flipSet ↑x {j}) = true

@[simp]

theorem AaronsonAmbainis.DetLow.flipSet_singleton_self {ι : Type} [DecidableEq ι] (x : Cube ι) (j : ι) : flipSet x {j} j = !x j

theorem AaronsonAmbainis.DetLow.flipSet_singleton_of_ne {ι : Type} [DecidableEq ι] (x : Cube ι) {i j : ι} (h : i ≠ j) : flipSet x {j} i = x i

@[simp]

theorem AaronsonAmbainis.DetLow.flipSet_flipSet_singleton {ι : Type} [DecidableEq ι] (x : Cube ι) (j : ι) : flipSet (flipSet x {j}) {j} = x