The homogeneous Hilbert count bounds evaluation-matrix ranks. The deficit includes every degree-allowed multiple of the defining equation.

noncomputable def CCDN.homogeneousCoefficientMap (K : Type u_1) [Field K] (n M : ℕ) : MvPolynomial (Fin (n + 1)) K →ₗ[K] Fin ((n + M).choose M) → K

The K-linear map sending a polynomial in n + 1 variables to its vector of coefficients at the degree-M monomials, enumerated by homogeneousMonomials n M.

Equations

• CCDN.homogeneousCoefficientMap K n M = LinearMap.pi fun (j : Fin ((n + M).choose M)) => MvPolynomial.lcoeff K (CCDN.homogeneousMonomials n M j)

noncomputable def CCDN.homogeneousEvaluationMatrix (K : Type u_1) [Field K] (n M : ℕ) {t : ℕ} (points : Fin t → Fin (n + 1) → K) : Matrix (Fin t) (Fin ((n + M).choose M)) K

The matrix of values of the degree-M monomials in n + 1 variables at the points points i: its (i, j) entry is the j-th monomial of homogeneousMonomials n M evaluated at points i.

Equations

• CCDN.homogeneousEvaluationMatrix K n M points i j = (CCDN.homogeneousMonomials n M j).prod fun (k : Fin (n + 1)) (e : ℕ) => points i k ^ e

theorem CCDN.homogeneous_evaluation_mulVec {K : Type u_1} [Field K] {n M t : ℕ} (f : MvPolynomial (Fin (n + 1)) K) (hf : f.IsHomogeneous M) (points : Fin t → Fin (n + 1) → K) (i : Fin t) : (homogeneousEvaluationMatrix K n M points).mulVec ((homogeneousCoefficientMap K n M) f) i = (MvPolynomial.eval (points i)) f

For a homogeneous polynomial f of degree M, multiplying the homogeneous evaluation matrix by the coefficient vector of f gives the vector of values of f at the points.

theorem CCDN.homogeneousEvaluationMatrix_intCast {n M t : ℕ} (points : Fin t → Fin (n + 1) → ℤ) : (homogeneousEvaluationMatrix ℚ n M fun (i : Fin t) (j : Fin (n + 1)) => ↑(points i j)) = (evaluationMatrix (homogeneousMonomials n M) points).map Int.cast

The homogeneous evaluation matrix of integer points, computed over ℚ, is the cast of the integer evaluation matrix of the degree-M monomials.

theorem CCDN.integer_homogeneous_rows_hilbert_bound {n d M t : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hdM : d ≤ M) (points : Fin t → Fin (n + 1) → ℤ) (hzero : ∀ (i : Fin t), (MvPolynomial.eval (points i)) f = 0) (hli : LinearIndependent ℚ ((evaluationMatrix (homogeneousMonomials n M) points).map Int.cast).row) : t + (n + (M - d)).choose (M - d) ≤ (n + M).choose M

For t integer zeros of a nonzero homogeneous integer polynomial f of degree d ≤ M whose degree-M evaluation rows are linearly independent over ℚ, the count t plus the dimension (n + (M - d)).choose (M - d) of the degree-M multiples of f is at most the number (n + M).choose M of degree-M monomials in n + 1 variables.