## Stream: new members

### Topic: contribution: induction on polynomial degree

#### Way Yan Win (Dec 07 2021 at 05:42):

Hi, it seems that (strong) induction on polynomial.nat_degree isn't supported yet, so as a first contribution to mathlib I'd like to add that. Here is the code I have, inspired by their analogues nat.strong_induction_on and nat.case_strong_induction_on:

import data.polynomial.degree.definitions

variables {R : Type*} [semiring R]

lemma polynomial_nat_degree_strong_induction_on {P : polynomial R → Prop}
(p : polynomial R)
(h : ∀ (p : polynomial R) (n : ℕ),
(∀ (m : ℕ), m < n →
(∀ (p' : polynomial R), p'.nat_degree = m → P p')) →
p.nat_degree = n → P p) :
P p :=
begin
generalize hd : p.nat_degree = d,
revert hd p,
apply nat.strong_induction_on d, clear d,
intros n h' p,
exact h p n h',
end

lemma polynomial_nat_degree_case_strong_induction_on {P : polynomial R → Prop}
(p : polynomial R)
(hz : ∀ (p : polynomial R), p.nat_degree = 0 → P p)
(hi : ∀ (p : polynomial R) (n : ℕ),
(∀ (m : ℕ), m ≤ n →
(∀ (p' : polynomial R), p'.nat_degree = m → P p')) →
p.nat_degree = n.succ → P p) :
P p :=
begin
generalize hd : p.nat_degree = d,
revert hd p,
apply nat.case_strong_induction_on d, clear d,
{ exact hz },
{ intros n h p, exact hi p n h }
end


If it is ok, can I have write access to the mathlib repository? My username is greysome.

#### Eric Wieser (Dec 07 2021 at 07:58):

I'd argue that strong induction on nat_degree is supported, and the spelling is pretty much what you have there. I don't think it makes much sense to duplicate nat strong_induction for every nat-valued property of other types.

#### Eric Wieser (Dec 07 2021 at 08:00):

Does induction h : p.nat_degree using nat.strong_induction_on do what you need?

#### Way Yan Win (Dec 07 2021 at 08:35):

ohh, I didn't know that was possible. thanks!

#### Way Yan Win (Dec 07 2021 at 08:41):

hmm wait actually there is a difference, because in the induction hypothesis there is an additional quantifier (namely, if for all m < n the property holds for all polynomials of degree m, then the property holds for all polynomials of degree n)

#### Way Yan Win (Dec 07 2021 at 08:44):

I think induction h : p.nat_degree using nat.strong_induction_on with i hi generalizing p would be correct

#### Eric Wieser (Dec 07 2021 at 08:55):

Ah, I forgot that it didn't generalize that automatically

#### Eric Wieser (Dec 07 2021 at 09:20):

If it is ok, can I have write access to the mathlib repository? My username is greysome.

I've sent an invite; even though I think the lemmas above are redundant, you're certainly welcome to contribute other things to mathlib

#### Yaël Dillies (Dec 07 2021 at 09:54):

This induction is a bit dull, but there are many inductions on the polynomials that we don't have. For example, p P -> p Q -> p (P * Q) and p (X - a)^n

#### Eric Rodriguez (Dec 07 2021 at 09:57):

That also needs p y for y in the base field or some similar condition

#### Eric Wieser (Dec 07 2021 at 10:23):

A variant of docs#polynomial.rec_on_horner for mv_polynomial might be nice too

#### Way Yan Win (Dec 09 2021 at 08:18):

Since we're already on this topic, there are some other results on polynomials that I've needed, which are oddly missing:

variables {R : Type*} [semiring R]
theorem nat_degree_pow_le (p : polynomial R) (n : ℕ) : (p ^ n).nat_degree ≤ n * p.nat_degree := sorry
theorem coeff_pow_degree_mul_degree (p : polynomial R) (n : ℕ) : (p ^ n).coeff (n * p.nat_degree) = p.leading_coeff ^ n := sorry


This seems like a reasonable contribution since there's already nat_degree_mul_le and coeff_mul_degree_add_degree

#### Yaël Dillies (Dec 09 2021 at 08:27):

And maybe do the constant coeff version as well?

#### Eric Wieser (Dec 09 2021 at 08:34):

Note we already have docs#polynomial.nat_degree_pow and docs#polynomial.nat_degree_pow'; the new pow lemma should reference those and maybe go somewhere near them

#### Way Yan Win (Dec 09 2021 at 08:38):

Yaël Dillies said:

And maybe do the constant coeff version as well?

Which specific result is that?

#### Way Yan Win (Dec 09 2021 at 08:39):

Eric Wieser said:

Note we already have docs#polynomial.nat_degree_pow and docs#polynomial.nat_degree_pow'; the new pow lemma should reference those and maybe go somewhere near them

Ah ok I'll try that

#### Eric Wieser (Dec 09 2021 at 08:43):

If you're looking for more contributions, we should probably have the degree variant of that nat.degree lemma

#### Way Yan Win (Dec 09 2021 at 10:39):

Right now I'm trying to copy the proof for nat_degree_mul_le in nat_degree_pow_le:

import data.polynomial.degree.definitions
open polynomial

variables {R : Type*} [semiring R]

lemma nat_degree_pow_le {p : polynomial R} {n : ℕ} : nat_degree (p ^ n) ≤ n * nat_degree p :=
begin
apply nat_degree_le_of_degree_le,
apply le_trans (degree_pow_le p n),
rw [nsmul_eq_mul, with_bot.coe_mul],
sorry
end


So I'm stuck at showing that ↑n * p.degree ≤ ↑n * ↑p.nat_degree. The other proof continued with refine add_le_add _ _, but the corresponding refine mul_le_mul_left' _ _ doesn't work. I suspect it's because with_bot.ordered_add_comm_monoid has been established but not with_bot.ordered_comm_monoid. Hopefully I'm on the right track with this?

#### Eric Wieser (Dec 09 2021 at 10:54):

Is it easier to prove the degree_pow_le version first?

#### Eric Wieser (Dec 09 2021 at 10:55):

Then do case analysis on whether p = 0 to handle the \bot and nat cases?

#### Ruben Van de Velde (Dec 09 2021 at 10:57):

Yeah, I don't think getting to a goal like p.degree ≤ ↑(p.nat_degree) is going to help you

#### Kevin Buzzard (Dec 09 2021 at 10:58):

Maybe direct induction on n is far less painful?

#### Ruben Van de Velde (Dec 09 2021 at 10:59):

rw [nat.cast_with_bot, degree_eq_nat_degree hp] will help though, after the case split

#### Eric Wieser (Dec 09 2021 at 11:04):

This is a mess, but works:

lemma nat_degree_pow_le {p : polynomial R} {n : ℕ} : nat_degree (p ^ n) ≤ n * nat_degree p :=
begin
by_cases hn : n = 0,
{ rw hn, simp },
by_cases hpn : p ^ n = 0,
{ rw hpn, simp },
have hp : p ≠ 0,
{ rintro rfl,
apply hpn,
simp [hn], },
rw [←with_bot.coe_le_coe, with_bot.coe_mul],
rw [←degree_eq_nat_degree hpn, ←degree_eq_nat_degree hp],
convert degree_pow_le _ _,
simp,
end


#### Ruben Van de Velde (Dec 09 2021 at 11:04):

Six lines with either approach:

import data.polynomial.degree

open polynomial

variables {R : Type*} [semiring R]
lemma nat_degree_pow_le {p : polynomial R} {n : ℕ} : nat_degree (p ^ n) ≤ n * nat_degree p :=
begin
obtain rfl|hp := eq_or_ne p 0,
{ obtain rfl|hn := eq_or_ne n 0; simp [*] },
apply nat_degree_le_of_degree_le,
apply le_trans (degree_pow_le p n),
rw [nsmul_eq_mul, with_bot.coe_mul, nat.cast_with_bot, degree_eq_nat_degree hp],
exact le_rfl,
end

lemma nat_degree_pow_le' {p : polynomial R} {n : ℕ} : nat_degree (p ^ n) ≤ n * nat_degree p :=
begin
induction n with n ih,
{ simp },
{ rw [pow_succ],
apply le_trans nat_degree_mul_le,
end


#### Eric Wieser (Dec 09 2021 at 11:05):

I think proving it in terms of the degree version is nicer than using induction

#### Kevin Buzzard (Dec 09 2021 at 11:06):

despite the fact that the induction proof has fewer characters, is more primitive, and probably compiles more quickly? ;-)

#### Eric Wieser (Dec 09 2021 at 11:07):

Yes, because the one proved from degree gives a template for "how to prove things about nat_degree from things about degree" that you can blindly repeat

#### Eric Wieser (Dec 09 2021 at 11:07):

Of course, it would also be good to make the proof less messy.

#### Way Yan Win (Dec 09 2021 at 11:36):

Thanks, I'll try the above approaches then. I was initially worried that the proof will look different from the existing proofs, but I guess it's good to have something working at least

Last updated: Dec 20 2023 at 11:08 UTC