Elementary determinant bounds

The archimedean Gram determinant estimate is the one used in CCDN §3.3. The row-factor divisibility lemma isolates a basic arithmetic input to determinant lower bounds; it does not assert the much stronger local multiplicity estimates of CCDN §2.

theorem CCDN.prod_row_factors_dvd_det {R : Type u_1} [CommRing R] {s : ℕ} (A : Matrix (Fin s) (Fin s) R) (d : Fin s → R) (h : ∀ (i j : Fin s), d i ∣ A i j) : ∏ i : Fin s, d i ∣ A.det

If row i is divisible by d i, the product of the row factors divides the determinant.

theorem CCDN.evaluation_gram_det_le {n N s M : ℕ} (mon : Fin N → Fin n →₀ ℕ) (points : Fin s → Fin n → ℤ) {B : ℝ} (hB : 1 ≤ B) (hpoints : ∀ (i : Fin s), InBox (points i) B) (hdeg : ∀ (j : Fin N), Finsupp.degree (mon j) ≤ M) : have A := (evaluationMatrix mon points).map Int.cast; |(A * A.transpose).det| ≤ ↑s.factorial * (↑N * (B ^ M) ^ 2) ^ s

Archimedean Gram determinant bound: if A is the real evaluation matrix of N monomials of degree at most M at s integer points in the box of radius B ≥ 1, then |det (A Aᵀ)| ≤ s! · (N · B ^ (2 M)) ^ s.