DetBij / Basic: cube lemmas and the agreement monomial

Elementary facts on flipSet, diffSet, antipode, the agreement set agSet, and the exponent vector agExp of the agreement monomial agMon.

def AaronsonAmbainis.DetBij.agSet {ι : Type} [Fintype ι] (x z : Cube ι) : Finset ι

The agreement set of x and z (written ag(x,z) in the paper).

Equations

• AaronsonAmbainis.DetBij.agSet x z = {i : ι | x i = z i}

theorem AaronsonAmbainis.DetBij.mem_agSet {ι : Type} [Fintype ι] {x z : Cube ι} {i : ι} : i ∈ agSet x z ↔ x i = z i

theorem AaronsonAmbainis.DetBij.mem_diffSet {ι : Type} [Fintype ι] {x z : Cube ι} {i : ι} : i ∈ diffSet x z ↔ x i ≠ z i

theorem AaronsonAmbainis.DetBij.flipSet_apply {ι : Type} [DecidableEq ι] (x : Cube ι) (S : Finset ι) (i : ι) : flipSet x S i = if i ∈ S then !x i else x i

theorem AaronsonAmbainis.DetBij.flipSet_empty {ι : Type} [DecidableEq ι] (x : Cube ι) : flipSet x ∅ = x

theorem AaronsonAmbainis.DetBij.diffSet_flipSet {ι : Type} [Fintype ι] [DecidableEq ι] (x : Cube ι) (S : Finset ι) : diffSet x (flipSet x S) = S

A point w with diffSet x w = S is flipSet x S: first half.

theorem AaronsonAmbainis.DetBij.flipSet_diffSet {ι : Type} [Fintype ι] [DecidableEq ι] (x w : Cube ι) : flipSet x (diffSet x w) = w

A point w with diffSet x w = S is flipSet x S: second half.

theorem AaronsonAmbainis.DetBij.diffSet_eq_empty_iff {ι : Type} [Fintype ι] {x w : Cube ι} : diffSet x w = ∅ ↔ x = w

theorem AaronsonAmbainis.DetBij.flipSet_antipode_agSet {ι : Type} [Fintype ι] [DecidableEq ι] (u z : Cube ι) : flipSet (antipode u) (agSet u z) = z

z is the antipode of u flipped on the agreement set of u and z.

noncomputable def AaronsonAmbainis.DetBij.agExp {ι : Type} [Fintype ι] (x z : Cube ι) : ι →₀ ℕ

The exponent vector of agMon x z: the indicator of the agreement set.

Equations

• AaronsonAmbainis.DetBij.agExp x z = ∑ i : ι, if x i = z i then Finsupp.single i 1 else 0

theorem AaronsonAmbainis.DetBij.agExp_apply {ι : Type} [Fintype ι] (x z : Cube ι) (j : ι) : (agExp x z) j = if x j = z j then 1 else 0

theorem AaronsonAmbainis.DetBij.agMon_eq_monomial {ι : Type} [Fintype ι] (x z : Cube ι) : agMon x z = (MvPolynomial.monomial (agExp x z)) 1

agMon x z is the monomial with exponent vector agExp x z and coefficient 1.