DetLow: the determinant of the agreement matrix is nonzero

This is Lemma 3.4 of the paper. Evaluate every variable at the real number c = 2 ^ n (n = Fintype.card ι). The evaluated matrix has diagonal entries c ^ n and off-diagonal entries c ^ k with k + 1 ≤ n, and a row has fewer than 2 ^ n = c off-diagonal entries, so the matrix is strictly diagonally dominant and its determinant is nonzero (Gershgorin: det_ne_zero_of_sum_row_lt_diag).

noncomputable def AaronsonAmbainis.DetLow.evalAt {ι : Type} (c : ℝ) : MvPolynomial ι ℤ →+* ℝ

Evaluation of all variables at the real number c.

Equations

• AaronsonAmbainis.DetLow.evalAt c = MvPolynomial.eval₂Hom (Int.castRingHom ℝ) fun (x : ι) => c

def AaronsonAmbainis.DetLow.agCount {ι : Type} [Fintype ι] (x z : Cube ι) : ℕ

The number of coordinates in which x and z agree.

Equations

• AaronsonAmbainis.DetLow.agCount x z = {i : ι | x i = z i}.card

theorem AaronsonAmbainis.DetLow.evalAt_agMon {ι : Type} [Fintype ι] (c : ℝ) (x z : Cube ι) : (evalAt c) (agMon x z) = c ^ agCount x z

theorem AaronsonAmbainis.DetLow.agCount_self {ι : Type} [Fintype ι] (x : Cube ι) : agCount x x = Fintype.card ι

theorem AaronsonAmbainis.DetLow.agCount_lt {ι : Type} [Fintype ι] (x z : Cube ι) (h : x ≠ z) : agCount x z < Fintype.card ι

theorem AaronsonAmbainis.DetLow.evalMat_apply {ι : Type} [Fintype ι] [DecidableEq ι] (c : ℝ) (g : Cube ι → Bool) (x z : Ones g) : (evalAt c).mapMatrix (agMatrix g) x z = c ^ agCount ↑x ↑z

theorem AaronsonAmbainis.DetLow.card_erase_succ_le {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (x : Ones g) : (Finset.univ.erase x).card + 1 ≤ 2 ^ Fintype.card ι

A row of the ones of g has fewer than 2 ^ n off-diagonal entries.

theorem AaronsonAmbainis.DetLow.evalMat_dominant {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (c : ℝ) (hc : c = 2 ^ Fintype.card ι) (x : Ones g) : ∑ z ∈ Finset.univ.erase x, ‖(evalAt c).mapMatrix (agMatrix g) x z‖ < ‖(evalAt c).mapMatrix (agMatrix g) x x‖

The evaluated matrix is strictly diagonally dominant when c = 2 ^ n.

theorem AaronsonAmbainis.DetLow.agMatrix_det_ne_zero {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) : (agMatrix g).det ≠ 0

Lemma 3.4 of the paper: the determinant of the agreement matrix is nonzero.