Interface for the proof of the determinant inequality

This file defines the lowest monomials of a polynomial (IsLowest, Section 3.2 of the paper) and the agreement matrix (agMatrix, Section 3.3), and splits the proof of DetInequality (Corollary 3.2) into two independent parts:

• LowestUnit — multiplying by a polynomial with constant coefficient 1 does not change the monomials of least total degree (Lemma 3.3);
• LowestBound — the determinant of the agreement matrix on the ones of g is nonzero, and each of its monomials of least total degree has exponent at most bdry g j in every variable j (Lemma 3.4 and Lemma 3.6).

The directory DetLow proves LowestUnit and LowestBound. The directory DetBij proves LowestUnit → LowestBound → DetInequality.

def AaronsonAmbainis.IsLowest {ι : Type} [Fintype ι] (q : MvPolynomial ι ℤ) (m : ι →₀ ℕ) : Prop

m is a monomial of q of least total degree.

Equations

• AaronsonAmbainis.IsLowest q m = (m ∈ q.support ∧ ∀ m' ∈ q.support, ∑ i : ι, m i ≤ ∑ i : ι, m' i)

theorem AaronsonAmbainis.exists_isLowest {ι : Type} [Fintype ι] (q : MvPolynomial ι ℤ) (hq : q ≠ 0) : ∃ (m : ι →₀ ℕ), IsLowest q m

A nonzero polynomial has a monomial of least total degree.

noncomputable def AaronsonAmbainis.agMon {ι : Type} [Fintype ι] (x z : Cube ι) : MvPolynomial ι ℤ

agMon x z = ∏_{i : x_i = z_i} s_i: the monomial of the agreement set of x and z.

Equations

• AaronsonAmbainis.agMon x z = ∏ i : ι, if x i = z i then MvPolynomial.X i else 1

@[reducible, inline]

abbrev AaronsonAmbainis.Ones {ι : Type} (g : Cube ι → Bool) : Type

The ones of g, as a type.

Equations

• AaronsonAmbainis.Ones g = { x : AaronsonAmbainis.Cube ι // g x = true }

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

The agreement matrix M[x,z] = s^{ag(x,z)} on the ones of g.

Equations

• AaronsonAmbainis.agMatrix g x z = AaronsonAmbainis.agMon ↑x ↑z

def AaronsonAmbainis.LowestUnit : Prop

Multiplying by a polynomial with constant coefficient 1 does not change the monomials of least total degree.

Equations

• One or more equations did not get rendered due to their size.

def AaronsonAmbainis.LowestBound : Prop

The determinant of the agreement matrix is nonzero, and each of its monomials of least total degree has exponent at most bdry g j in every variable j.

Equations

• One or more equations did not get rendered due to their size.