possible improvements to `Polynomial.rootMultiplicity`

Stream: general

[Jz Pan]

I propose certain improvements to Polynomial.rootMultiplicity, let's make a list:

• Polynomial.rootMultiplicity should be closely related to Polynomial.trailingDegree, namely p.rootMultiplicity t = (aeval (X + C t) p).natTrailingDegree
• Therefore rootMultiplicity_mul should have stronger version similar to le_natTrailingDegree_mul, natTrailingDegree_mul'.

[Jz Pan]

Secondly,

• rootMultiplicity_sub_one_le_derivative_rootMultiplicity should have a stronger version which doesn't requiring characteristic zero, but only requiring derivative not zero (let's discuss it later after I finish its proof).

[Jz Pan]

• rootMultiplicity_X_sub_C_pow should not need [IsDomain R] (but still need [Nontrivial R]); I believe that there are other lemmas which should not need that either.

[Jz Pan]

This is my attempt:

import Mathlib.Data.Polynomial.RingDivision
import Mathlib.Data.Polynomial.Derivative

open scoped Classical Polynomial

noncomputable section

namespace Polynomial

variable {R : Type*} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ}

variable (t)

lemma rootMultiplicity_eq_rootMultiplicity :
    p.rootMultiplicity t = (aeval (X + C t) p).rootMultiplicity 0 := by
  have hdvd : ∀ n : ℕ, (X - C t) ^ n ∣ p ↔ (X - C 0) ^ n ∣ aeval (X + C t) p := by
    refine fun n ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩
    · replace h := (aeval (X + C t)).map_dvd h
      simpa only [AlgHom.toRingHom_eq_coe, map_pow, map_sub, RingHom.coe_coe, aeval_X, aeval_C,
        ← C_eq_algebraMap, add_sub_cancel, map_zero, sub_zero] using h
    · replace h := (aeval (X - C t)).map_dvd h
      simpa only [AlgHom.toRingHom_eq_coe, map_zero, sub_zero, map_pow, RingHom.coe_coe,
        aeval_X, ← AlgHom.comp_apply, ← aeval_algHom, map_add, aeval_C, ← C_eq_algebraMap,
        sub_add_cancel, aeval_X_left, AlgHom.coe_id, id_eq] using h
  by_cases h : p = 0
  · simp only [h, map_zero, dite_true, rootMultiplicity_zero]
  have h' : aeval (X + C t) p ≠ 0 := fun h' ↦ h <| by
    apply_fun aeval (X - C t) at h'
    rwa [map_zero, ← AlgHom.comp_apply, ← aeval_algHom, map_add, aeval_X, aeval_C,
      ← C_eq_algebraMap, sub_add_cancel, aeval_X_left, AlgHom.coe_id, id_eq] at h'
  rw [rootMultiplicity_eq_nat_find_of_nonzero h, rootMultiplicity_eq_nat_find_of_nonzero h']
  letI : DecidablePred fun n : ℕ => ¬(X - C t) ^ (n + 1) ∣ p := fun n ↦
    @Not.decidable _ (decidableDvdMonic p ((monic_X_sub_C t).pow (n + 1)))
  letI : DecidablePred fun n : ℕ => ¬(X - C 0) ^ (n + 1) ∣ aeval (X + C t) p := fun n ↦
    @Not.decidable _ (decidableDvdMonic (aeval (X + C t) p) ((monic_X_sub_C 0).pow (n + 1)))
  set m := Nat.find (multiplicity_X_sub_C_finite 0 h') with ← hm; clear_value m
  rw [Nat.find_eq_iff] at hm ⊢
  obtain ⟨hm, hm2⟩ := hm
  refine ⟨?_, fun n hn ↦ ?_⟩
  · rwa [hdvd]
  · simpa only [hdvd] using hm2 n hn

lemma rootMultiplicity_zero_eq_natTrailingDegree :
    p.rootMultiplicity 0 = p.natTrailingDegree := by
  by_cases h : p = 0
  · simp only [h, rootMultiplicity_zero, natTrailingDegree_zero]
  rw [rootMultiplicity_eq_nat_find_of_nonzero h]
  letI : DecidablePred fun n : ℕ => ¬(X - C 0) ^ (n + 1) ∣ p := fun n ↦
    @Not.decidable _ (decidableDvdMonic p ((monic_X_sub_C 0).pow (n + 1)))
  set m := Nat.find (multiplicity_X_sub_C_finite 0 h) with ← hm; clear_value m
  rw [Nat.find_eq_iff] at hm
  obtain ⟨hm, hm2⟩ := hm
  by_cases hm0 : m = 0
  · simp only [map_zero, sub_zero, hm0, zero_add, pow_one, X_dvd_iff] at hm
    linarith only [hm0, natTrailingDegree_le_of_ne_zero hm]
  replace hm0 : m - 1 + 1 = m := Nat.sub_add_cancel <| Nat.pos_of_ne_zero hm0
  replace hm2 := hm2 (m - 1) <| Nat.le_of_eq <| hm0
  simp only [map_zero, sub_zero, hm0, not_not, X_pow_dvd_iff] at hm hm2
  replace hm : p.coeff m ≠ 0 := fun h ↦ hm <| fun d hd ↦ by
    by_cases hd' : d < m
    · exact hm2 d hd'
    rwa [Nat.eq_of_lt_succ_of_not_lt hd hd']
  exact le_antisymm (le_natTrailingDegree h hm2) (natTrailingDegree_le_of_ne_zero hm)

lemma rootMultiplicity_eq_natTrailingDegree :
    p.rootMultiplicity t = (aeval (X + C t) p).natTrailingDegree := by
  rw [rootMultiplicity_eq_rootMultiplicity, rootMultiplicity_zero_eq_natTrailingDegree]

lemma rootMultiplicity_mul_X_sub_C_pow' (h : p ≠ 0) :
    (p * (X - C t) ^ n).rootMultiplicity t = p.rootMultiplicity t + n := by
  have h' : aeval (X + C t) p ≠ 0 := fun h' ↦ h <| by
    apply_fun aeval (X - C t) at h'
    rwa [map_zero, ← AlgHom.comp_apply, ← aeval_algHom, map_add, aeval_X, aeval_C,
      ← C_eq_algebraMap, sub_add_cancel, aeval_X_left, AlgHom.coe_id, id_eq] at h'
  simp only [rootMultiplicity_eq_natTrailingDegree, map_mul, map_pow, map_sub, aeval_X,
    aeval_C, ← C_eq_algebraMap, add_sub_cancel, natTrailingDegree_mul_X_pow h']

lemma rootMultiplicity_mul_X_sub_C_pow'' (h : p * (X - C t) ^ n ≠ 0) :
    (p * (X - C t) ^ n).rootMultiplicity t = p.rootMultiplicity t + n :=
  rootMultiplicity_mul_X_sub_C_pow' t (left_ne_zero_of_mul h)

lemma rootMultiplicity_X_sub_C_pow' [Nontrivial R] :
    ((X - C t) ^ n).rootMultiplicity t = n := by
  have := rootMultiplicity_mul_X_sub_C_pow' t (n := n) <| RingHom.map_one_ne_zero C
  rwa [rootMultiplicity_C, map_one, one_mul, zero_add] at this

lemma rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero
    (hnezero : derivative p ≠ 0) :
    p.rootMultiplicity t - 1 ≤ (derivative p).rootMultiplicity t := by
  have hp := divByMonic_mul_pow_rootMultiplicity_eq p t
  set m := p.rootMultiplicity t
  set g := p /ₘ (X - C t) ^ m
  have : derivative p = derivative g * (X - C t) ^ m + g * (C (m : R)) * (X - C t) ^ (m - 1) := by
    rw [← hp, derivative_mul, derivative_pow, map_sub, derivative_X, derivative_C, sub_zero, mul_one, mul_assoc]
  by_cases h1 : derivative g * (X - C t) ^ m = 0
  · rw [h1, zero_add] at this
    have := this.symm ▸ rootMultiplicity_mul_X_sub_C_pow'' t (this ▸ hnezero)
    rw [this]
    exact Nat.le_add_left (m - 1) _
  by_cases h2 : g * (C (m : R)) * (X - C t) ^ (m - 1) = 0
  · rw [h2, add_zero] at this
    have := this.symm ▸ rootMultiplicity_mul_X_sub_C_pow'' t (this ▸ hnezero)
    rw [this]
    exact m.sub_le 1 |>.trans <| Nat.le_add_left m _
  have := this.symm ▸ rootMultiplicity_add t (this ▸ hnezero)
  refine le_min ?_ ?_ |>.trans this
  · rw [rootMultiplicity_mul_X_sub_C_pow'' t h1]
    exact m.sub_le 1 |>.trans <| Nat.le_add_left m _
  · rw [rootMultiplicity_mul_X_sub_C_pow'' t h2]
    exact Nat.le_add_left (m - 1) _

variable {t}

lemma isRoot_iterate_derivative_of_lt_rootMultiplicity
    (hn : n < p.rootMultiplicity t) : (derivative^[n] p).IsRoot t := by
  revert p
  induction' n with n ih
  · intro p h
    exact rootMultiplicity_pos'.1 h |>.2
  · intro p h
    rw [Function.iterate_succ, Function.comp_apply]
    by_cases hzero : derivative p = 0
    · rw [hzero, iterate_derivative_zero, IsRoot.def, eval_zero]
    exact ih <| Nat.lt_of_lt_of_le (Nat.lt_pred_of_succ_lt h)
      (rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero t hzero)

end Polynomial

[Jz Pan]

Jz Pan said:

• Therefore rootMultiplicity_mul should have stronger version similar to le_natTrailingDegree_mul, natTrailingDegree_mul'.

However, the condition is very hard to describe :sweat_smile:. So far the only useful one is rootMultiplicity_mul_X_sub_C_pow''.

[Jz Pan]

I opened a draft pull request #8563. Comments welcome.