DetLow: (1 - s_j^2)^(e_j) divides the determinant of the agreement matrix

This is Lemma 3.5 of the paper. Row operations: with P[x,y] = 1 if x j = true and y = x^j (and 0 otherwise), (1 + s_j P) (1 - s_j P) = 1 and (1 - s_j P) M = D N, where D is diagonal with entry 1 - s_j^2 at the rows x ∈ Up g j and 1 elsewhere. (In the proof of the paper the matrices P, D, N are called E, Λ, M~.)

theorem AaronsonAmbainis.DetLow.agMon_eq_mul_erase {ι : Type} [Fintype ι] [DecidableEq ι] (x z : Cube ι) (j : ι) : agMon x z = (if x j = z j then MvPolynomial.X j else 1) * ∏ i ∈ Finset.univ.erase j, if x i = z i then MvPolynomial.X i else 1

Splitting off the j-th factor of agMon.

theorem AaronsonAmbainis.DetLow.prod_erase_flipSet {ι : Type} [Fintype ι] [DecidableEq ι] (x z : Cube ι) (j : ι) : (∏ i ∈ Finset.univ.erase j, if flipSet x {j} i = z i then MvPolynomial.X i else 1) = ∏ i ∈ Finset.univ.erase j, if x i = z i then MvPolynomial.X i else 1

theorem AaronsonAmbainis.DetLow.agMon_of_eq {ι : Type} [Fintype ι] [DecidableEq ι] (x z : Cube ι) (j : ι) (h : x j = z j) : agMon x z = MvPolynomial.X j * agMon (flipSet x {j}) z

If x and z agree at j then M[x,z] = s_j * M[x^j,z].

theorem AaronsonAmbainis.DetLow.agMon_of_ne {ι : Type} [Fintype ι] [DecidableEq ι] (x z : Cube ι) (j : ι) (h : x j ≠ z j) : agMon (flipSet x {j}) z = MvPolynomial.X j * agMon x z

If x and z disagree at j then M[x^j,z] = s_j * M[x,z].

noncomputable def AaronsonAmbainis.DetLow.pairMat {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : Matrix (Ones g) (Ones g) (MvPolynomial ι ℤ)

P[x,y] = 1 if x j = true and y = x^j, and 0 otherwise.

Equations

• AaronsonAmbainis.DetLow.pairMat g j x y = if ↑x j = true ∧ ↑y = AaronsonAmbainis.flipSet ↑x {j} then 1 else 0

noncomputable def AaronsonAmbainis.DetLow.redMat {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : Matrix (Ones g) (Ones g) (MvPolynomial ι ℤ)

N[x,z] = 0 if x ∈ Up g j and z j = x j, and M[x,z] otherwise.

Equations

• AaronsonAmbainis.DetLow.redMat g j x z = if x ∈ AaronsonAmbainis.DetLow.Up g j ∧ ↑z j = ↑x j then 0 else AaronsonAmbainis.agMon ↑x ↑z

noncomputable def AaronsonAmbainis.DetLow.diagVec {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : Ones g → MvPolynomial ι ℤ

The diagonal of D: 1 - s_j^2 on Up g j, 1 elsewhere.

Equations

• AaronsonAmbainis.DetLow.diagVec g j x = if x ∈ AaronsonAmbainis.DetLow.Up g j then 1 - MvPolynomial.X j ^ 2 else 1

theorem AaronsonAmbainis.DetLow.pairMat_apply {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) (x y : Ones g) : pairMat g j x y = if ↑x j = true ∧ ↑y = flipSet ↑x {j} then 1 else 0

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

theorem AaronsonAmbainis.DetLow.pairMat_mul_pairMat {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : pairMat g j * pairMat g j = 0

theorem AaronsonAmbainis.DetLow.pairMat_mul_agMatrix {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) (x z : Ones g) : (pairMat g j * agMatrix g) x z = if x ∈ Up g j then agMon (flipSet ↑x {j}) ↑z else 0

theorem AaronsonAmbainis.DetLow.unipotent_mul {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : (1 + MvPolynomial.X j • pairMat g j) * (1 - MvPolynomial.X j • pairMat g j) = 1

theorem AaronsonAmbainis.DetLow.rowop_eq {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : (1 - MvPolynomial.X j • pairMat g j) * agMatrix g = Matrix.diagonal (diagVec g j) * redMat g j

theorem AaronsonAmbainis.DetLow.prod_diagVec {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : ∏ x : Ones g, diagVec g j x = (1 - MvPolynomial.X j ^ 2) ^ (Up g j).card

theorem AaronsonAmbainis.DetLow.det_factor {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : ∃ (R : MvPolynomial ι ℤ), (agMatrix g).det = (1 - MvPolynomial.X j ^ 2) ^ (Up g j).card * R

Lemma 3.5 of the paper: det M = (1 - s_j^2)^(e_j) * R for some polynomial R.