[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,133 @@
+/-
+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 `RatFunc.Polynomial.hilbert p d`.
+
+For example, given `d : ℕ`, the power series expansion of `1/(1-X)ᵈ⁺¹` in `F[X]` is
+`Σₙ ((d + n).choose d)Xⁿ`, which equals `Σₙ ((n + 1)···(n + d)/d!)Xⁿ` and hence
+`RatFunc.Polynomial.hilbert (1 : F[X]) d` is the polynomial `(n + 1)···(n + d)/d!`. Note that if
+`d! = 0` in `F`, then the polynomial `(n + 1)···(n + d)/d!` no longer works, so we do not want the
+characteristic of `F` to be divisible by `d!`. As `RatFunc.Polynomial.hilbert` may take any
+`p : F[X]` and `d : ℕ` as its inputs, it is necessary for us to assume that `CharZero F`.
+
+## Main definitions
+
+* `RatFunc.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 `RatFunc.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 Polynomial PowerSeries
+
+variable (F : Type*) [Field F]
+
+namespace RatFunc
+
+namespace Polynomial
+
+/--
+For any field `F` and natural numbers `d` and `k`, `RatFunc.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. `RatFunc.Polynomial.preHilbert ℚ d 0`
+is exactly the Hilbert polynomial of the polynomial ring `ℚ[X_0,...,X_d]` viewed as
+a graded module over itself. In fact, `RatFunc.Polynomial.preHilbert F d k` is the
+same as `RatFunc.Polynomial.hilbert ((X : F[X]) ^ k) (d + 1)` for any field `F` and
+`d k : ℕ` (see the lemma `RatFunc.Polynomial.hilbert_X_pow_succ`). See also the lemma
+`RatFunc.Polynomial.preHilbert_eq_choose_sub_add`, which states that if `CharZero F`,
+then for any `d k n : ℕ` with `k ≤ n`, `(RatFunc.Polynomial.preHilbert F d k).eval (n : F)`
+equals `(n - k + d).choose d`.
+-/
+noncomputable def preHilbert (d k : ℕ) : F[X] :=
+  (d.factorial : F)⁻¹ • ((ascPochhammer F d).comp (Polynomial.X - (C (k : F)) + 1))
+
+lemma 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}
+
+/--
+`RatFunc.Polynomial.hilbert p 0 = 0`; for any `d : ℕ`, `RatFunc.Polynomial.hilbert p (d + 1)`
+is defined as `∑ i in p.support, (p.coeff i) • RatFunc.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 `RatFunc.Polynomial.hilbert p d` is the Hilbert
+polynomial of `M`. See also `RatFunc.Polynomial.coeff_mul_invOneSubPow_eq_hilbert_eval`,
+which says that `PowerSeries.coeff F n (p * (PowerSeries.invOneSubPow F d))` is equal to
+`(RatFunc.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_nat (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]
+
+lemma hilbert_poly_zero (p : F[X]) : hilbert p 0 = 0 := by
+  delta hilbert; simp
+
+variable (F) in
+lemma hilbert_X_pow_succ (d k : ℕ) :
+    hilbert ((X : F[X]) ^ k) (d + 1) = preHilbert F d k := by
+  delta hilbert; simp
+
+/--
+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 : ℕ`, `(RatFunc.Polynomial.hilbert p d).eval (n : F)` equals
+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]
+      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 (preHilbert F d ↑i) = (n + d - ↑i).choose d := by
+        rw [preHilbert_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]
+
+end Polynomial
+
+end RatFunc

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"],