Zulip Chat Archive

Stream: new members

Topic: Improve code: root multiplicity of a sum


view this post on Zulip 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],
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.

view this post on Zulip 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.

view this post on Zulip 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,
             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

view this post on Zulip 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,
  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!

view this post on Zulip Aaron Anderson (Oct 06 2020 at 05:05):

Would it help anything if we made multiplicity a valuation?

view this post on Zulip Johan Commelin (Oct 06 2020 at 05:41):

What do you mean with valuation?

view this post on Zulip Johan Commelin (Oct 06 2020 at 05:41):

mathlib only knows about multiplicative valuations atm...

view this post on Zulip Aaron Anderson (Oct 08 2020 at 05:45):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 08 2020 at 06:20):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 08 2020 at 06:39):

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

view this post on Zulip 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.

view this post on Zulip 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