English
Let F be a field and d, k be natural numbers. The polynomial preHilbertPoly F d k is defined by (d!)^{-1} times the composition of ascPochhammer F d with X − C(k) + 1; this is the basic building block used to formulate Hilbert polynomials.
Русский
Пусть F — поле, а d, k — натуральные числа. Полином preHilbertPoly F d k задаётся как (d!)^{-1} умноженное на композицию ascPochhammer F d и X − C(k) + 1; это базовый строительный блок для определения полиномов Хилберта.
LaTeX
$$$\operatorname{preHilbertPoly}(F,d,k) = (d!)^{-1} \cdot \big(\operatorname{ascPochhammer}(F,d)\big) \circ \big(X - C(k) + 1\big)$$$
Lean4
/-- For any field `F` and natural numbers `d` and `k`, `Polynomial.preHilbertPoly F d k`
is defined as `(d.factorial : F)⁻¹ • ((ascPochhammer F d).comp (X - (C (k : F)) + 1))`.
This is the most basic form of Hilbert polynomials. `Polynomial.preHilbertPoly ℚ d 0`
is exactly the Hilbert polynomial of the polynomial ring `ℚ[X_0,...,X_d]` viewed as
a graded module over itself. In fact, `Polynomial.preHilbertPoly F d k` is the
same as `Polynomial.hilbertPoly ((X : F[X]) ^ k) (d + 1)` for any field `F` and
`d k : ℕ` (see the lemma `Polynomial.hilbertPoly_X_pow_succ`). See also the lemma
`Polynomial.preHilbertPoly_eq_choose_sub_add`, which states that if `CharZero F`,
then for any `d k n : ℕ` with `k ≤ n`, `(Polynomial.preHilbertPoly F d k).eval (n : F)`
equals `(n - k + d).choose d`.
-/
noncomputable def preHilbertPoly (d k : ℕ) : F[X] :=
(d.factorial : F)⁻¹ • ((ascPochhammer F d).comp (Polynomial.X - (C (k : F)) + 1))
