DetLow: the number of ones of g is 2 e_j + b_j(g)

This is a step of the proof of Lemma 3.6 of the paper. The ones of g split into the upper endpoints Up g j of the j-edges inside the ones, the lower endpoints Dn g j (in bijection with Up g j by flipping j), and the points Bd g j whose j-neighbour is a zero of g (there are bdry g j of them).

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

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

Equations

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

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

The ones of g whose j-neighbour is a zero of g.

Equations

• AaronsonAmbainis.DetLow.Bd g j = {x : AaronsonAmbainis.Ones g | g (AaronsonAmbainis.flipSet ↑x {j}) = false}

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

theorem AaronsonAmbainis.DetLow.mem_Bd {ι : Type} [Fintype ι] [DecidableEq ι] {g : Cube ι → Bool} {j : ι} {x : Ones g} : x ∈ Bd g j ↔ g (flipSet ↑x {j}) = false

theorem AaronsonAmbainis.DetLow.card_Dn {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : (Dn g j).card = (Up g j).card

theorem AaronsonAmbainis.DetLow.card_Bd {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : (Bd g j).card = bdry g j

theorem AaronsonAmbainis.DetLow.card_ones_eq {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : Fintype.card (Ones g) = 2 * (Up g j).card + bdry g j

The number of ones of g is 2 e_j + b_j(g) (proof of Lemma 3.6 of the paper).