DetBij / Identity: the matrices P, U, Q' and the identity P * M = U * Q'

A : Cube ι → Finset ι is a field of sets; the identity needs A x to be a 1-wing of g at every x with g x = true (this is the only use of the wing property).

The file proves the wing identity (Lemma 3.7 of the paper, wing_sum) and parts (i) and (ii) of Lemma 3.8 (Pmat_mul_agMatrix, constantCoeff_det_Pmat, constantCoeff_det_Umat). The matrix Q' (Qmat) is the matrix Q of the paper.

noncomputable def AaronsonAmbainis.DetBij.Pmat {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (A : Cube ι → Finset ι) : Matrix (Ones g) (Ones g) (MvPolynomial ι ℤ)

P[x,w] = ∏_{i ∈ Δ(x,w)} (-s_i) if Δ(x,w) ⊆ A x, and 0 otherwise.

Equations

• AaronsonAmbainis.DetBij.Pmat g A x w = if AaronsonAmbainis.diffSet ↑x ↑w ⊆ A ↑x then ∏ i ∈ AaronsonAmbainis.diffSet ↑x ↑w, -MvPolynomial.X i else 0

noncomputable def AaronsonAmbainis.DetBij.Umat {ι : Type} [Fintype ι] (g : Cube ι → Bool) (A : Cube ι → Finset ι) : Matrix (Ones g) (Ones g) (MvPolynomial ι ℤ)

U is diagonal with entry ∏_{i ∈ A x} (1 - s_i^2) at x.

Equations

• AaronsonAmbainis.DetBij.Umat g A = Matrix.diagonal fun (x : AaronsonAmbainis.Ones g) => ∏ i ∈ A ↑x, (1 - MvPolynomial.X i ^ 2)

noncomputable def AaronsonAmbainis.DetBij.Qmat {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (A : Cube ι → Finset ι) : Matrix (Ones g) (Ones g) (MvPolynomial ι ℤ)

Q'[x,z] = M[x,z] if the agreement set of x and z is disjoint from A x, else 0.

Equations

• AaronsonAmbainis.DetBij.Qmat g A x z = if Disjoint (AaronsonAmbainis.DetBij.agSet ↑x ↑z) (A ↑x) then AaronsonAmbainis.agMon ↑x ↑z else 0

theorem AaronsonAmbainis.DetBij.Pmat_apply {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (A : Cube ι → Finset ι) (x w : Ones g) : Pmat g A x w = if diffSet ↑x ↑w ⊆ A ↑x then ∏ i ∈ diffSet ↑x ↑w, -MvPolynomial.X i else 0

theorem AaronsonAmbainis.DetBij.Qmat_apply {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (A : Cube ι → Finset ι) (x z : Ones g) : Qmat g A x z = if Disjoint (agSet ↑x ↑z) (A ↑x) then agMon ↑x ↑z else 0

theorem AaronsonAmbainis.DetBij.agMatrix_apply {ι : Type} [Fintype ι] (g : Cube ι → Bool) (x z : Ones g) : agMatrix g x z = agMon ↑x ↑z

The wing identity, coordinate by coordinate

noncomputable def AaronsonAmbainis.DetBij.fAg {ι : Type} (x z : Cube ι) (i : ι) : MvPolynomial ι ℤ

The factor of agMon x z at coordinate i.

Equations

• AaronsonAmbainis.DetBij.fAg x z i = if x i = z i then MvPolynomial.X i else 1

noncomputable def AaronsonAmbainis.DetBij.gAg {ι : Type} (x z : Cube ι) (i : ι) : MvPolynomial ι ℤ

The factor at coordinate i of agMon x' z, where x' is x flipped at i.

Equations

• AaronsonAmbainis.DetBij.gAg x z i = if x i = z i then 1 else MvPolynomial.X i

theorem AaronsonAmbainis.DetBij.agMon_eq_prod {ι : Type} [Fintype ι] (x z : Cube ι) : agMon x z = ∏ i : ι, fAg x z i

theorem AaronsonAmbainis.DetBij.fAg_flipSet_of_mem {ι : Type} [DecidableEq ι] (x z : Cube ι) {S : Finset ι} {i : ι} (hi : i ∈ S) : fAg (flipSet x S) z i = gAg x z i

theorem AaronsonAmbainis.DetBij.fAg_flipSet_of_notMem {ι : Type} [DecidableEq ι] (x z : Cube ι) {S : Finset ι} {i : ι} (hi : i ∉ S) : fAg (flipSet x S) z i = fAg x z i

theorem AaronsonAmbainis.DetBij.neg_X_mul_gAg_add_fAg {ι : Type} (x z : Cube ι) (i : ι) : -MvPolynomial.X i * gAg x z i + fAg x z i = if x i = z i then 0 else 1 - MvPolynomial.X i ^ 2

A coordinate of the wing contributes 0 if x_i = z_i and 1 - s_i^2 otherwise.

theorem AaronsonAmbainis.DetBij.wing_term {ι : Type} [Fintype ι] [DecidableEq ι] (x z : Cube ι) {A S : Finset ι} (hSA : S ⊆ A) : (∏ i ∈ S, -MvPolynomial.X i) * agMon (flipSet x S) z = ((∏ i ∈ S, -MvPolynomial.X i * gAg x z i) * ∏ i ∈ A \ S, fAg x z i) * ∏ i ∈ Aᶜ, fAg x z i

One term of the wing sum, split into the coordinates in S, in A \ S and outside A.

theorem AaronsonAmbainis.DetBij.wing_sum {ι : Type} [Fintype ι] [DecidableEq ι] (x z : Cube ι) (A : Finset ι) : ∑ S ∈ A.powerset, (∏ i ∈ S, -MvPolynomial.X i) * agMon (flipSet x S) z = (∏ i ∈ A, (1 - MvPolynomial.X i ^ 2)) * if Disjoint (agSet x z) A then agMon x z else 0

The wing identity (Lemma 3.7 of the paper), for an arbitrary set A and points x, z of the cube.

The matrix identity

theorem AaronsonAmbainis.DetBij.Pmat_mul_agMatrix {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (A : Cube ι → Finset ι) (hA : ∀ (x : Ones g), IsWing g (↑x) (A ↑x)) : Pmat g A * agMatrix g = Umat g A * Qmat g A

P * M = U * Q' (Lemma 3.8 (i) of the paper), using the wing property.

Constant coefficients of det P and det U

theorem AaronsonAmbainis.DetBij.constantCoeff_Pmat {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (A : Cube ι → Finset ι) (x w : Ones g) : MvPolynomial.constantCoeff (Pmat g A x w) = if x = w then 1 else 0

theorem AaronsonAmbainis.DetBij.constantCoeff_det_Pmat {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (A : Cube ι → Finset ι) : MvPolynomial.constantCoeff (Pmat g A).det = 1

theorem AaronsonAmbainis.DetBij.constantCoeff_det_Umat {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (A : Cube ι → Finset ι) : MvPolynomial.constantCoeff (Umat g A).det = 1