# Zulip Chat Archive

## 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,
apply le_trans (add_le_add_left ih _),
rw [nat.succ_mul, add_comm] },
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