[Merged by Bors] - feat(RingTheory/Polynomial/Hilbert): Polynomial.exists_unique_hilbertPoly and Polynomial.hilbertPoly_mul_one_sub_pow_add

Mathlib/RingTheory/Polynomial/HilbertPoly.lean

@@ -5,6 +5,8 @@ Authors: Fangming Li, Jujian Zhang
 -/
 import Mathlib.Algebra.Polynomial.AlgebraMap
 import Mathlib.Algebra.Polynomial.Eval.SMul
+import Mathlib.Algebra.Polynomial.Roots
+import Mathlib.Order.Interval.Set.Infinite
 import Mathlib.RingTheory.Polynomial.Pochhammer
 import Mathlib.RingTheory.PowerSeries.WellKnown
 import Mathlib.Tactic.FieldSimp
@@ -17,9 +19,9 @@ given any `p : F[X]` and `d : ℕ`, there exists some `h : F[X]` such that for a
 `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.hilbertPoly 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
-`Polynomial.hilbertPoly (1 : F[X]) d` is the polynomial `(n + 1)···(n + d)/d!`. Note that
+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
+`Polynomial.hilbertPoly (1 : F[X]) (d + 1)` 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 `Polynomial.hilbertPoly` may take
 any `p : F[X]` and `d : ℕ` as its inputs, it is necessary for us to assume that `CharZero F`.
@@ -96,13 +98,15 @@ lemma hilbertPoly_X_pow_succ (d k : ℕ) :
     hilbertPoly ((X : F[X]) ^ k) (d + 1) = preHilbertPoly F d k := by
   delta hilbertPoly; simp
 
+variable [CharZero F]
+
 /--
 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
-    [CharZero F] {p : F[X]} (d : ℕ) {n : ℕ} (hn : p.natDegree < n) :
+    {p : F[X]} (d : ℕ) {n : ℕ} (hn : p.natDegree < n) :
     PowerSeries.coeff F n (p * (invOneSubPow F d)) = (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]
@@ -127,4 +131,60 @@ theorem coeff_mul_invOneSubPow_eq_hilbertPoly_eval
         rw [hx.2, zero_mul]
       · rw [add_comm, Nat.add_sub_assoc (h_le ⟨x, hx⟩), succ_eq_add_one, add_tsub_cancel_right]
 
+/--
+The polynomial satisfying the key property of `Polynomial.hilbertPoly p d` is unique. In other
+words, if `h : F[X]` and there exists some `N : ℕ` such that for any number `n : ℕ` bigger than
+`N` we have `PowerSeries.coeff F n (p * (invOneSubPow F d)) = h.eval (n : F)`, then `h` is exactly
+`Polynomial.hilbertPoly p d`.
+-/
+theorem exists_unique_hilbertPoly (p : F[X]) (d : ℕ) :
+    ∃! (h : F[X]), (∃ (N : ℕ), (∀ (n : ℕ) (_ : N < n),
+    PowerSeries.coeff F n (p * (invOneSubPow F d)) = h.eval (n : F))) := by
+  use hilbertPoly p d; constructor
+  · use p.natDegree
+    exact fun n hn => coeff_mul_invOneSubPow_eq_hilbertPoly_eval d hn
+  · rintro h ⟨N, hhN⟩
+    refine eq_of_infinite_eval_eq h (hilbertPoly p d) ?_
+    intro hfin
+    have hsub : Nat.cast '' Set.Ioi (N ⊔ p.natDegree) ⊆
+        { x | h.eval x = (p.hilbertPoly d).eval x } := by
+      intro x hx
+      simp only [Set.mem_image, Set.mem_Ioi, sup_lt_iff, Set.mem_setOf_eq] at hx ⊢
+      rcases hx with ⟨n, ⟨hn1, hn2⟩, hn3⟩
+      rw [← hn3, ← coeff_mul_invOneSubPow_eq_hilbertPoly_eval d hn2, hhN n hn1]
+    exact Set.Infinite.image (Set.injOn_of_injective Nat.cast_injective)
+      (Set.Ioi_infinite (N ⊔ p.natDegree)) (Set.Finite.subset hfin hsub)
+
+lemma hilbertPoly_mul_one_sub_succ (p : F[X]) (d : ℕ) :
+    hilbertPoly (p * (1 - X)) (d + 1) = hilbertPoly p d := by
+  have heq (n : Set.Ioi (p * (1 - X)).natDegree) :
+      (hilbertPoly (p * (1 - X)) (d + 1)).eval (n : F) = (hilbertPoly p d).eval (n : F) := by
+    by_cases hp : p = 0
+    · simp only [hp, zero_mul, hilbertPoly_zero_nat]
+    · have hlt : (p * (1 - X)).natDegree < (n : ℕ) := Set.mem_Ioi.1 n.2
+      rw [← coeff_mul_invOneSubPow_eq_hilbertPoly_eval _ hlt,
+        ← coeff_mul_invOneSubPow_eq_hilbertPoly_eval]
+      · apply PowerSeries.ext_iff.1 <| by simp only [coe_mul, mul_assoc, coe_sub, coe_one, coe_X,
+          ← one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val F d 1, pow_one]
+      · have hne : (1 : F[X]) - X ≠ 0 := fun h0 => by simpa only [coeff_sub, coeff_one_zero,
+          coeff_X_zero, sub_zero, coeff_zero, one_ne_zero] using ext_iff.1 h0 0
+        simp_rw [natDegree_mul hp hne] at hlt
+        exact lt_of_add_right_lt hlt
+  refine eq_of_infinite_eval_eq _ _ ?_
+  · intro hfin
+    have hsub : Nat.cast '' Set.Ioi (p * (1 - X)).natDegree ⊆
+        { x | ((p * (1 - X)).hilbertPoly (d + 1)).eval x = (p.hilbertPoly d).eval x } := by
+      intro x hx
+      rcases hx with ⟨n, hn1, hn2⟩
+      rw [← hn2]
+      exact heq ⟨n, hn1⟩
+    exact Set.Infinite.image (Set.injOn_of_injective cast_injective) (Set.Ioi_infinite _)
+      (Set.Finite.subset hfin hsub)
+
+lemma hilbertPoly_mul_one_sub_pow_add (p : F[X]) (d e : ℕ) :
+    hilbertPoly (p * (1 - X) ^ e) (d + e) = hilbertPoly p d := by
+  induction e with
+  | zero => simp
+  | succ e he => rw [pow_add, pow_one, ← mul_assoc, ← add_assoc, hilbertPoly_mul_one_sub_succ, he]
+
 end Polynomial

Mathlib/RingTheory/PowerSeries/WellKnown.lean

@@ -159,6 +159,20 @@ 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 :=
   (invOneSubPow S (d + 1)).val_inv
 
+theorem invOneSubPow_add (e : ℕ) :
+    invOneSubPow S (d + e) = invOneSubPow S d * invOneSubPow S e := by
+  simp_rw [invOneSubPow_eq_inv_one_sub_pow, pow_add]
+
+theorem one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val (e : ℕ) :
+    (1 - X) ^ e * (invOneSubPow S (d + e)).val = (invOneSubPow S d).val := by
+  rw [invOneSubPow_add, Units.val_mul, mul_comm, mul_assoc, ← invOneSubPow_inv_eq_one_sub_pow]
+  simp
+
+theorem one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow (e : ℕ) :
+    (1 - X) ^ (d + e) * (invOneSubPow S e).val = (1 - X) ^ d := by
+  rw [pow_add, mul_assoc, ← invOneSubPow_inv_eq_one_sub_pow S e]
+  simp
+
 end invOneSubPow
 
 section Field