[Merged by Bors] - feat(RingTheory/Polynomial/HilbertPoly): the definition and key property of Polynomial.hilbertPoly p d for p : F[X] and d : ℕ, where F is a field.

Mathlib.lean

@@ -4387,6 +4387,7 @@ import Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
 import Mathlib.RingTheory.Polynomial.GaussLemma
 import Mathlib.RingTheory.Polynomial.Hermite.Basic
 import Mathlib.RingTheory.Polynomial.Hermite.Gaussian
+import Mathlib.RingTheory.Polynomial.Hilbert
 import Mathlib.RingTheory.Polynomial.IntegralNormalization
 import Mathlib.RingTheory.Polynomial.IrreducibleRing
 import Mathlib.RingTheory.Polynomial.Nilpotent

Mathlib/Data/Nat/Factorial/BigOperators.lean

@@ -33,6 +33,10 @@ theorem prod_factorial_dvd_factorial_sum : (∏ i ∈ s, (f i)!) ∣ (∑ i ∈
   · rw [prod_cons, Finset.sum_cons]
     exact (mul_dvd_mul_left _ ih).trans (Nat.factorial_mul_factorial_dvd_factorial_add _ _)
 
+theorem ascFactorial_eq_prod_range (n : ℕ) : ∀ k, n.ascFactorial k = ∏ i ∈ range k, (n + i)
+  | 0 => rfl
+  | k + 1 => by rw [ascFactorial, prod_range_succ, mul_comm, ascFactorial_eq_prod_range n k]
+
 theorem descFactorial_eq_prod_range (n : ℕ) : ∀ k, n.descFactorial k = ∏ i ∈ range k, (n - i)
   | 0 => rfl
   | k + 1 => by rw [descFactorial, prod_range_succ, mul_comm, descFactorial_eq_prod_range n k]

Mathlib/RingTheory/Polynomial/Hilbert.lean

@@ -0,0 +1,105 @@
+/-
+Copyright (c) 2024 Fangming Li. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fangming Li, Jujian Zhang
+-/
+import Mathlib.Algebra.Polynomial.AlgebraMap
+import Mathlib.Algebra.Polynomial.Eval.SMul
+import Mathlib.RingTheory.Polynomial.Pochhammer
+import Mathlib.RingTheory.PowerSeries.WellKnown
+import Mathlib.Tactic.FieldSimp
+
+/-!
+# Hilbert polynomials
+
+In this file, we formalise the following statement: if `F` is a field with characteristic `0`, then
+given any `p : F[X]` and `d : ℕ`, there exists some `h : F[X]` such that for any large enough
+`n : ℕ`, `h(n)` is equal to the coefficient of `Xⁿ` in the power series expansion of `p/(1 - X)ᵈ`.
+This `h` is unique and is denoted as `Polynomial.hilbert p d`.
+
+## Main definitions
+
+* `Polynomial.hilbert p d`. Given a field `F`, a polynomial `p : F[X]` and a natural number `d`, if
+  `F` is of characteristic `0`, then `Polynomial.hilbert p d : F[X]` is the polynomial whose value
+  at `n` equals the coefficient of `Xⁿ` in the power series expansion of `p/(1 - X)ᵈ`.
+
+## TODO
+
+* Hilbert polynomials of finitely generated graded modules over Noetherian rings.
+-/
+
+open Nat PowerSeries
+
+variable (F : Type*) [Field F]
+
+namespace Polynomial
+
+/--
+For any field `F` and natrual numbers `d` and `k`, `Polynomial.preHilbert 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.preHilbert ℚ d 0` is exactly the Hilbert polynomial of
+the polynomial ring `ℚ[X_0,...,X_d]` viewed as a graded module over itself. See also the theorem
+`Polynomial.preHilbert_eq_choose_sub_add`, which states that if `CharZero F`, then for any
+`d k n : ℕ` with `k ≤ n`, `(Polynomial.preHilbert F d k).eval (n : F) = (n - k + d).choose d`.
+-/
+noncomputable def preHilbert (d k : ℕ) : F[X] :=
+  (d.factorial : F)⁻¹ • ((ascPochhammer F d).comp (X - (C (k : F)) + 1))
+
+theorem preHilbert_eq_choose_sub_add [CharZero F] (d k n : ℕ) (hkn : k ≤ n):
+    (preHilbert F d k).eval (n : F) = (n - k + d).choose d := by
+  have : ((d ! : ℕ) : F) ≠ 0 := by norm_cast; positivity
+  calc
+  _ = (↑d !)⁻¹ * eval (↑(n - k + 1)) (ascPochhammer F d) := by simp [cast_sub hkn, preHilbert]
+  _ = (n - k + d).choose d := by
+    rw [ascPochhammer_nat_eq_natCast_ascFactorial];
+    field_simp [ascFactorial_eq_factorial_mul_choose]
+
+variable {F}
+
+/--
+`Polynomial.hilbert p 0 = 0`; for any `d : ℕ`, `Polynomial.hilbert p (d + 1)` is
+defined as `∑ i in p.support, (p.coeff i) • Polynomial.preHilbert 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.hilbert p d` is the Hilbert
+polynomial of `M`. See also `Polynomial.coeff_mul_invOneSubPow_eq_hilbert_eval`,
+which says that `PowerSeries.coeff F n (p * (PowerSeries.invOneSubPow F d))` is
+equal to `(Polynomial.hilbert p d).eval (n : F)` for any large enough `n : ℕ`.
+-/
+noncomputable def hilbert (p : F[X]) : (d : ℕ) → F[X]
+  | 0 => 0
+  | d + 1 => ∑ i in p.support, (p.coeff i) • preHilbert F d i
+
+variable (F) in
+lemma hilbert_zero (d : ℕ) : hilbert (0 : F[X]) d = 0 := by
+  delta hilbert; induction d with
+  | zero => simp only
+  | succ d _ => simp only [coeff_zero, zero_smul, Finset.sum_const_zero]
+
+/--
+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.hilbert p d).eval (n : F)` is equal to the
+coefficient of `Xⁿ` in the power series expansion of `p/(1 - X)ᵈ`.
+-/
+theorem coeff_mul_invOneSubPow_eq_hilbert_eval
+    [CharZero F] (p : F[X]) (d n : ℕ) (hn : p.natDegree < n) :
+    PowerSeries.coeff F n (p * (invOneSubPow F d)) = (hilbert p d).eval (n : F) := by
+  delta hilbert; 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]
+      simp_rw [show (i : p.support) → eval ↑n (preHilbert F d ↑i) = (n + d - ↑i).choose d by
+        intro i; rw [preHilbert_eq_choose_sub_add _ _ _ _ <| le_trans (le_natDegree_of_ne_zero
+        <| mem_support_iff.1 i.2) (le_of_lt hn)]; rw [Nat.sub_add_comm];
+        exact le_trans (le_natDegree_of_ne_zero <| mem_support_iff.1 i.2) (le_of_lt hn)]
+      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]
+      exact Eq.symm <| Finset.sum_subset_zero_on_sdiff (fun s hs => Finset.mem_range_succ_iff.mpr
+        <| le_trans (le_natDegree_of_ne_zero <| mem_support_iff.1 hs) (le_of_lt hn)) (fun x hx => by
+        simp only [Finset.mem_sdiff, mem_support_iff, not_not] at hx; rw [hx.2, zero_mul])
+        (fun x hx => by rw [add_comm, Nat.add_sub_assoc <| le_trans (le_natDegree_of_ne_zero <|
+        mem_support_iff.1 hx) (le_of_lt hn), succ_eq_add_one, add_tsub_cancel_right])
+
+end Polynomial

Mathlib/RingTheory/Polynomial/Pochhammer.lean

@@ -155,10 +155,20 @@ theorem ascPochhammer_nat_eq_ascFactorial (n : ℕ) :
     rw [ascPochhammer_succ_right, eval_mul, ascPochhammer_nat_eq_ascFactorial n t, eval_add, eval_X,
       eval_natCast, Nat.cast_id, Nat.ascFactorial_succ, mul_comm]
 
+theorem ascPochhammer_nat_eq_natCast_ascFactorial (S : Type*) [Semiring S] (n k : ℕ) :
+    (ascPochhammer S k).eval (n : S) = n.ascFactorial k := by
+  norm_cast
+  rw [ascPochhammer_nat_eq_ascFactorial]
+
 theorem ascPochhammer_nat_eq_descFactorial (a b : ℕ) :
     (ascPochhammer ℕ b).eval a = (a + b - 1).descFactorial b := by
   rw [ascPochhammer_nat_eq_ascFactorial, Nat.add_descFactorial_eq_ascFactorial']
 
+theorem ascPochhammer_nat_eq_natCast_descFactorial (S : Type*) [Semiring S] (a b : ℕ) :
+    (ascPochhammer S b).eval (a : S) = (a + b - 1).descFactorial b := by
+  norm_cast
+  rw [ascPochhammer_nat_eq_descFactorial]
+
 @[simp]
 theorem ascPochhammer_natDegree (n : ℕ) [NoZeroDivisors S] [Nontrivial S] :
     (ascPochhammer S n).natDegree = n := by

Mathlib/RingTheory/PowerSeries/WellKnown.lean

@@ -152,10 +152,9 @@ theorem invOneSubPow_inv_eq_one_sub_pow :
   | zero => exact Eq.symm <| pow_zero _
   | succ d => rfl
 
-theorem invOneSubPow_inv_eq_one_of_eq_zero (h : d = 0) :
-    (invOneSubPow S d).inv = 1 := by
+theorem invOneSubPow_inv_zero_eq_one : (invOneSubPow S 0).inv = 1 := by
   delta invOneSubPow
-  simp only [h, Units.inv_eq_val_inv, inv_one, Units.val_one]
+  simp only [Units.inv_eq_val_inv, inv_one, Units.val_one]
 
 theorem mk_add_choose_mul_one_sub_pow_eq_one :
     (mk fun n ↦ Nat.choose (d + n) d : S⟦X⟧) * ((1 - X) ^ (d + 1)) = 1 :=

scripts/noshake.json

@@ -317,14 +317,15 @@
   "Mathlib.RingTheory.PowerSeries.Basic":
   ["Mathlib.Algebra.CharP.Defs", "Mathlib.Tactic.MoveAdd"],
   "Mathlib.RingTheory.PolynomialAlgebra": ["Mathlib.Data.Matrix.DMatrix"],
+  "Mathlib.RingTheory.Polynomial.Hilbert":
+  ["Mathlib.RingTheory.PowerSeries.WellKnown"],
   "Mathlib.RingTheory.MvPolynomial.Homogeneous":
   ["Mathlib.Algebra.DirectSum.Internal"],
   "Mathlib.RingTheory.KrullDimension.Basic":
   ["Mathlib.Algebra.MvPolynomial.CommRing", "Mathlib.Algebra.Polynomial.Basic"],
   "Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs":
   ["Mathlib.Tactic.Algebraize"],
-  "Mathlib.RingTheory.Finiteness.Defs":
-  ["Mathlib.Tactic.Algebraize"],
+  "Mathlib.RingTheory.Finiteness.Defs": ["Mathlib.Tactic.Algebraize"],
   "Mathlib.RingTheory.Binomial": ["Mathlib.Algebra.Order.Floor"],
   "Mathlib.RingTheory.Adjoin.Basic": ["Mathlib.LinearAlgebra.Finsupp.SumProd"],
   "Mathlib.RepresentationTheory.FdRep":
@@ -365,7 +366,6 @@
   "Mathlib.Deprecated.NatLemmas": ["Batteries.Data.Nat.Lemmas", "Batteries.WF"],
   "Mathlib.Deprecated.MinMax": ["Mathlib.Order.MinMax"],
   "Mathlib.Deprecated.ByteArray": ["Batteries.Data.ByteSubarray"],
-  "Mathlib.Data.ENat.Lattice": ["Mathlib.Algebra.Group.Action.Defs"],
   "Mathlib.Data.Vector.Basic": ["Mathlib.Control.Applicative"],
   "Mathlib.Data.Set.Image":
   ["Batteries.Tactic.Congr", "Mathlib.Data.Set.SymmDiff"],
@@ -387,6 +387,7 @@
   "Mathlib.Data.Int.Defs": ["Batteries.Data.Int.Order"],
   "Mathlib.Data.FunLike.Basic": ["Mathlib.Logic.Function.Basic"],
   "Mathlib.Data.Finset.Insert": ["Mathlib.Data.Finset.Attr"],
+  "Mathlib.Data.ENat.Lattice": ["Mathlib.Algebra.Group.Action.Defs"],
   "Mathlib.Data.ByteArray": ["Batteries.Data.ByteSubarray"],
   "Mathlib.Data.Bool.Basic": ["Batteries.Tactic.Init"],
   "Mathlib.Control.Traversable.Instances": ["Mathlib.Control.Applicative"],