English
The Hilbert polynomial of a polynomial p is defined as follows: it is the zero polynomial at degree 0, and for d ≥ 0, hilbertPoly(p)(d+1) equals the sum over i in the support of p of the coefficient p_i times preHilbertPoly F d i.
Русский
Гильбртов полином полинома p задаётся так: для степени 0 он равен нулю, а для d ≥ 0 выполняется hilbertPoly(p)(d+1) = сумма по i из поддержки p от p_i умножить на preHilbertPoly F d i.
LaTeX
$$$\text{hilbertPoly}(p)(0) = 0, \quad \text{hilbertPoly}(p)(d+1) = \sum_{i \in \mathrm{supp}(p)} p_i \; \text{preHilbertPoly}(F,d,i).$$$
Lean4
/-- `Polynomial.hilbertPoly p 0 = 0`; for any `d : ℕ`, `Polynomial.hilbertPoly p (d + 1)`
is defined as `∑ i ∈ p.support, (p.coeff i) • Polynomial.preHilbertPoly F d i`. If
`M` is a graded module whose Poincaré series can be written as `p(X)/(1 - X)ᵈ` for some
`p : ℚ[X]` with integer coefficients, then `Polynomial.hilbertPoly p d` is the Hilbert
polynomial of `M`. See also `Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval`,
which says that `PowerSeries.coeff F n (p * PowerSeries.invOneSubPow F d)` equals
`(Polynomial.hilbertPoly p d).eval (n : F)` for any large enough `n : ℕ`.
-/
noncomputable def hilbertPoly (p : F[X]) : (d : ℕ) → F[X]
| 0 => 0
| d + 1 => ∑ i ∈ p.support, (p.coeff i) • preHilbertPoly F d i
