Improve code: root multiplicity of a sum

Stream: new members

[Riccardo Brasca]

Hi all! As I mentioned in #Is there code for X? > A polynomial splits if it has enough roots I wanted to prove that the multiplicity of a root in a sum of two polynomials is at least the minimum of the multiplicities. I figured it by myself and I think it is something that should be added to mathlib (specifically to data.polynomial.ring_division). My code works, but I don't think its quality is very high, so before making a PR I would like to have some comments. Here it is (the last lemma is the important one):

import data.polynomial.ring_division

variables {R : Type*} [integral_domain R]

namespace polynomial

/-The multiplicity of a as root of (X - a)^n is n-/
lemma root_multiplicity_X_sub_C_pow (a : R) (n : ℕ) : root_multiplicity a ((X - C a)^n) = n :=
begin
induction n with n hn,
{ apply root_multiplicity_eq_zero,
  simp },
have hzero :=  (ne_zero_of_monic (monic_pow (monic_X_sub_C a) n.succ)),
rw pow_succ (X - C a) n at *,
rw [root_multiplicity_mul hzero, root_multiplicity_X_sub_C_self],
simp [hn],
exact nat.one_add n
end

/-If (X - a)^n divides a polynomial p then the multipicity of a as root of p is at least n-/
lemma multiplicity_ge_of_dvd (p : polynomial R) (a : R) (n : ℕ) :
p ≠ 0 → (X - C a)^n ∣ p → root_multiplicity a p ≥ n :=
begin
intros hzero h,
have div := exists_eq_mul_right_of_dvd h,
cases div with q hq,
rw hq at *,
rw root_multiplicity_mul hzero,
rw root_multiplicity_X_sub_C_pow,
exact nat.le.intro rfl
end

variables (p : polynomial R) (a : R) (n : ℕ)

lemma min_power_dvd_sum (n m : ℕ) (p q d : polynomial R) (hp : d^n ∣ p) (hq : d^m ∣ q) :
d^(min n m) ∣ p + q :=
begin
cases hp with p₁ hdivp,
cases hq with q₁ hdivq,
by_cases n ≤ m,
{ have ex : ∃ a : ℕ, m = n + a := le_iff_exists_add.mp h,
  cases ex with a ha,
  simp [h],
  rw [ha, pow_add d n a] at hdivq,
  rw [hdivp, hdivq],
  have factor : d ^ n * p₁ + d ^ n * d ^ a * q₁ = d ^ n * (p₁ + d ^ a * q₁) := by ring,
  rw factor,
  exact dvd.intro (p₁ + d ^ a * q₁) rfl },
/-I tried to avoid this part with wlog but I wasn't able to do it-/
{ have ex : ∃ a : ℕ, n = m + a := le_iff_exists_add.mp (le_of_not_ge h),
  cases ex with a ha,
  simp [le_of_not_ge h],
  rw [ha, pow_add d m a] at hdivp,
  rw [hdivq, hdivp],
  have factor : d ^ m * d ^ a * p₁ + d ^ m * q₁ = d ^ m * (q₁ + d ^ a * p₁) := by ring,
  rw factor,
  exact dvd.intro (q₁ + d ^ a * p₁) rfl }
end

/-The multiplicty of p+q is at leas the minimum of the multiplicities-/
lemma root_multiplicity_add (p q : polynomial R) (a : R) (n : ℕ) (hzero : p + q ≠ 0) :
root_multiplicity a (p + q) ≥
min (root_multiplicity a p) (root_multiplicity a q) :=
begin
apply multiplicity_ge_of_dvd (p+q) a (min (root_multiplicity a p) (root_multiplicity a q)) hzero,
have hdivp : (X - C a) ^ root_multiplicity a p ∣ p := pow_root_multiplicity_dvd  p a,
have hdivq : (X - C a) ^ root_multiplicity a q ∣ q := pow_root_multiplicity_dvd  q a,
exact min_power_dvd_sum (root_multiplicity a p) (root_multiplicity a q) p q (X - C a) hdivp hdivq
end

end polynomial

All comments are welcome! Thank you.

[Reid Barton]

min_power_dvd_sum doesn't have anything to do with polynomial and the proof can use docs#pow_dvd_pow rather than a case split.

[Yakov Pechersky]

Some thoughts about formatting, avoiding \ge and implicit args:

import data.polynomial.ring_division

variables {R : Type*} [integral_domain R]

namespace polynomial

/-The multiplicity of a as root of (X - a)^n is n-/
lemma root_multiplicity_X_sub_C_pow (a : R) (n : ℕ) : root_multiplicity a ((X - C a) ^ n) = n :=
begin
  induction n with n hn,
  { refine root_multiplicity_eq_zero _,
    simp only [eval_one, is_root.def, not_false_iff, one_ne_zero, pow_zero] },
  have hzero :=  (ne_zero_of_monic (monic_pow (monic_X_sub_C a) n.succ)),
  rw pow_succ (X - C a) n at hzero ⊢,
  simp only [root_multiplicity_mul hzero, root_multiplicity_X_sub_C_self, hn, nat.one_add]
end

/-If (X - a)^n divides a polynomial p then the multipicity of a as root of p is at least n-/
lemma multiplicity_of_dvd {p : polynomial R} {a : R} {n : ℕ}
  (hzero : p ≠ 0) (h : (X - C a) ^ n ∣ p) : n ≤ root_multiplicity a p :=
begin
  obtain ⟨q, hq⟩ := exists_eq_mul_right_of_dvd h,
  rw hq at hzero,
  simp only [hq, root_multiplicity_mul hzero, root_multiplicity_X_sub_C_pow,
             ge_iff_le, zero_le, le_add_iff_nonneg_right],
end

variables {p : polynomial R} {a : R} {n : ℕ}

lemma min_power_dvd_sum {n m : ℕ} {p q d : polynomial R} (hp : d ^ n ∣ p) (hq : d ^ m ∣ q) :
  d ^ (min n m) ∣ p + q :=
begin
  obtain ⟨p₁, hdivp⟩ := hp,
  obtain ⟨q₁, hdivq⟩ := hq,
  rw [hdivp, hdivq],
  sorry
end

/-The multiplicty of p+q is at leas the minimum of the multiplicities-/
lemma root_multiplicity_add {p q : polynomial R} (a : R) {n : ℕ} (hzero : p + q ≠ 0) :
  min (root_multiplicity a p) (root_multiplicity a q) ≤ root_multiplicity a (p + q) :=
begin
  refine multiplicity_of_dvd hzero _,
  have hdivp : (X - C a) ^ root_multiplicity a p ∣ p := pow_root_multiplicity_dvd p a,
  have hdivq : (X - C a) ^ root_multiplicity a q ∣ q := pow_root_multiplicity_dvd q a,
  exact min_power_dvd_sum hdivp hdivq
end

end polynomial

[Riccardo Brasca]

@Reid Barton @Yakov Pechersky thank you very much! I've modified min_power_dvd_sum to hold in an arbitrary commutative semiring and taken into account the other suggestions.

import data.polynomial.ring_division

variables {R : Type*} [comm_semiring R]

lemma min_power_dvd_sum {n m : ℕ} {p q d : R} (hp : d^n ∣ p) (hq : d^m ∣ q) :
d^(min n m) ∣ p + q :=
begin
by_cases n ≤ m,
{ simp [h],
  replace hq := dvd.trans (pow_dvd_pow d h) hq,
  exact dvd_add hp hq },
{ simp [le_of_not_ge h],
  replace hp := dvd.trans (pow_dvd_pow d (le_of_not_ge h)) hp,
  exact dvd_add hp hq,
 },
end

namespace polynomial

variable [integral_domain R]

/-The multiplicity of a as root of (X - a)^n is n-/
lemma root_multiplicity_X_sub_C_pow (a : R) (n : ℕ) : root_multiplicity a ((X - C a) ^ n) = n :=
begin
  induction n with n hn,
  { refine root_multiplicity_eq_zero _,
    simp only [eval_one, is_root.def, not_false_iff, one_ne_zero, pow_zero] },
  have hzero :=  (ne_zero_of_monic (monic_pow (monic_X_sub_C a) n.succ)),
  rw pow_succ (X - C a) n at hzero ⊢,
  simp only [root_multiplicity_mul hzero, root_multiplicity_X_sub_C_self, hn, nat.one_add]
end

/-If (X - a)^n divides a polynomial p then the multipicity of a as root of p is at least n-/
lemma multiplicity_of_dvd {p : polynomial R} {a : R} {n : ℕ}
  (hzero : p ≠ 0) (h : (X - C a) ^ n ∣ p) : n ≤ root_multiplicity a p :=
begin
  obtain ⟨q, hq⟩ := exists_eq_mul_right_of_dvd h,
  rw hq at hzero,
  simp only [hq, root_multiplicity_mul hzero, root_multiplicity_X_sub_C_pow,
             ge_iff_le, zero_le, le_add_iff_nonneg_right],
end

/-The multiplicty of p+q is at leas the minimum of the multiplicities-/
lemma root_multiplicity_add {p q : polynomial R} (a : R) (hzero : p + q ≠ 0) :
  min (root_multiplicity a p) (root_multiplicity a q) ≤ root_multiplicity a (p + q) :=
begin
  refine multiplicity_of_dvd hzero _,
  have hdivp : (X - C a) ^ root_multiplicity a p ∣ p := pow_root_multiplicity_dvd p a,
  have hdivq : (X - C a) ^ root_multiplicity a q ∣ q := pow_root_multiplicity_dvd q a,
  exact min_power_dvd_sum hdivp hdivq
end

end polynomial

It looks already much better!

[Aaron Anderson]

Would it help anything if we made multiplicity a valuation?

[Johan Commelin]

What do you mean with valuation?

[Johan Commelin]

mathlib only knows about multiplicative valuations atm...

[Aaron Anderson]

I mean that mathematically it looks like a monoidal, additive, valuation

[Aaron Anderson]

And I wonder if we would be helped by tweaking the definitions of multiplicity and/or valuation to be able to at least have a valuation that’s related to multiplicity

[Johan Commelin]

@Kevin Buzzard Do you think it's true that most valuations are actually additive?

[Kevin Buzzard]

I think that most of the time one simply doesn't care and there's a trivial dictionary which passes from one language to the other. But I've not had enough experience using them to know whether this is going to be a pain in practice. I'll get back to DVRs in a couple of weeks and might learn more

[Johan Commelin]

Well, at the moment that "trivial dictionary" doesn't exist in Lean

[Johan Commelin]

And if from a user perspective it is a lot better to work with additive valuations all the time, then maybe we should switch to that.

[Johan Commelin]

But I don't look forward to implementing add_group_with_top and linearly_ordered_add_comm_group_with_top