Coefficient and determinant bounds for the integer closed-form matrix.

def CCDN.BivariateCoefficientBound (f : Polynomial (Polynomial ℤ)) (H : ℝ) : Prop

Every coefficient of the integer bivariate polynomial f has absolute value at most H.

Equations

• CCDN.BivariateCoefficientBound f H = ∀ (i j : ℕ), |↑((f.coeff i).coeff j)| ≤ H

theorem CCDN.coeff_monomial_mul_at {R : Type u_1} [CommRing R] (f : Polynomial R) (a : R) (n k : ℕ) : ((Polynomial.monomial n) a * f).coeff k = if n ≤ k then a * f.coeff (k - n) else 0

The k-th coefficient of monomial n a * f is a * f.coeff (k - n) if n ≤ k and zero otherwise.

theorem CCDN.bivariateCoefficientBound_monomial_mul {f : Polynomial (Polynomial ℤ)} {H : ℝ} (hH : 0 ≤ H) (hf : BivariateCoefficientBound f H) (a : ℤ) (m n : ℕ) : BivariateCoefficientBound ((Polynomial.monomial m) ((Polynomial.monomial n) a) * f) (|↑a| * H)

Multiplying an integer bivariate polynomial with coefficients bounded by H ≥ 0 by a monomial with coefficient a gives coefficients bounded by |a| * H.

theorem CCDN.bivariateCoefficientBound_mono {f : Polynomial (Polynomial ℤ)} {H K : ℝ} (hf : BivariateCoefficientBound f H) (h : H ≤ K) : BivariateCoefficientBound f K

A coefficient bound H for f implies every larger coefficient bound K.

theorem CCDN.closedFormPair_single_inl {R : Type u_1} [CommRing R] (d : ℕ) (i : BivariateGrid d) : (closedFormPair R d) (Pi.single (Sum.inl i) 1) = ((Polynomial.monomial ↑i.1) ((Polynomial.monomial ↑i.2) 1), 0)

The standard basis vector of the first block decodes to the pair (monomial, 0) with the corresponding grid monomial.

theorem CCDN.closedFormPair_single_inr {R : Type u_1} [CommRing R] (d : ℕ) (i : BivariateGrid d) : (closedFormPair R d) (Pi.single (Sum.inr i) 1) = (0, (Polynomial.monomial ↑i.1) ((Polynomial.monomial ↑i.2) 1))

The standard basis vector of the second block decodes to the pair (0, monomial) with the corresponding grid monomial.

theorem CCDN.closedForm_integer_minor_bound (d r : ℕ) (f : Polynomial (Polynomial ℤ)) (H : ℝ) (hH : 0 ≤ H) (hf : BivariateCoefficientBound f H) (houter : f.natDegree ≤ d) (hinner : ∀ (i : ℕ), (f.coeff i).natDegree ≤ d) (a : Fin r → ℕ × ℕ) (c : Fin r → ClosedFormColumns d) : |↑((closedFormCoefficientMatrix d f).submatrix a c).det| ≤ ↑r.factorial * (2 * ↑d * H) ^ r

Expansion of a selected determinant gives a coefficient-controlled integer witness bound, uniformly over all choices of rows and columns.