## Stream: new members

### Topic: Improve code: root multiplicity of a sum

#### Riccardo Brasca (Oct 05 2020 at 14:21):

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],
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 (Oct 05 2020 at 14:36):

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 (Oct 05 2020 at 14:53):

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,
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 (Oct 05 2020 at 15:10):

@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,
{ simp [le_of_not_ge h],
replace hp := dvd.trans (pow_dvd_pow d (le_of_not_ge h)) hp,
},
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,
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


#### Aaron Anderson (Oct 06 2020 at 05:05):

Would it help anything if we made multiplicity a valuation?

#### Johan Commelin (Oct 06 2020 at 05:41):

What do you mean with valuation?

#### Johan Commelin (Oct 06 2020 at 05:41):

mathlib only knows about multiplicative valuations atm...

#### Aaron Anderson (Oct 08 2020 at 05:45):

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

#### Aaron Anderson (Oct 08 2020 at 05:46):

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 (Oct 08 2020 at 06:20):

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

#### Kevin Buzzard (Oct 08 2020 at 06:28):

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 (Oct 08 2020 at 06:39):

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

#### Johan Commelin (Oct 08 2020 at 06:39):

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 (Oct 08 2020 at 06:40):

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

Last updated: May 13 2021 at 17:42 UTC