English
For CharZero field F, and p ∈ F[X], d ∈ ℕ, for all n with n > p.natDegree, the coefficient equality holds between p*invOneSubPow F d and h.eval n for h = hilbertPoly p d.
Русский
Для поля F характерности ноль и полинома p, для всех больших n коэффициенты связаны с hilbertPoly.
LaTeX
$$theorem coeff_mul_invOneSubPow_eq_hilbertPoly_eval {p : Polynomial F} (d : Nat) {n : Nat} (hn : p.natDegree < n) :
(p * invOneSubPow F d : F⟦X⟧).coeff n = (hilbertPoly p d).eval (n : F)$$
Lean4
/-- The key property of Hilbert polynomials. If `F` is a field with characteristic `0`, `p : F[X]` and
`d : ℕ`, then for any large enough `n : ℕ`, `(Polynomial.hilbertPoly p d).eval (n : F)` equals the
coefficient of `Xⁿ` in the power series expansion of `p/(1 - X)ᵈ`.
-/
theorem coeff_mul_invOneSubPow_eq_hilbertPoly_eval {p : F[X]} (d : ℕ) {n : ℕ} (hn : p.natDegree < n) :
(p * invOneSubPow F d : F⟦X⟧).coeff n = (hilbertPoly p d).eval (n : F) := by delta hilbertPoly;
induction d with
| zero =>
simp only [invOneSubPow_zero, Units.val_one, mul_one, coeff_coe, eval_zero]
exact coeff_eq_zero_of_natDegree_lt hn
| succ d hd =>
simp only [eval_finset_sum, eval_smul, smul_eq_mul]
rw [← Finset.sum_coe_sort]
have h_le (i : p.support) : (i : ℕ) ≤ n := le_trans (le_natDegree_of_ne_zero <| mem_support_iff.1 i.2) hn.le
have h (i : p.support) : eval ↑n (preHilbertPoly F d ↑i) = (n + d - ↑i).choose d := by
rw [preHilbertPoly_eq_choose_sub_add _ _ (h_le i), Nat.sub_add_comm (h_le i)]
simp_rw [h]
rw [Finset.sum_coe_sort _ (fun x => (p.coeff ↑x) * (_ + d - ↑x).choose _), PowerSeries.coeff_mul,
Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk,
invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos _ _ (zero_lt_succ d)]
simp only [coeff_coe, coeff_mk]
symm
refine Finset.sum_subset_zero_on_sdiff (fun s hs ↦ ?_) (fun x hx ↦ ?_) (fun x hx ↦ ?_)
· rw [Finset.mem_range_succ_iff]
exact h_le ⟨s, hs⟩
· simp only [Finset.mem_sdiff, mem_support_iff, not_not] at hx
rw [hx.2, zero_mul]
· rw [add_comm, Nat.add_sub_assoc (h_le ⟨x, hx⟩), succ_eq_add_one, add_tsub_cancel_right]
