Proofs About Polynomial Degree Based on Derivative

Stream: maths

[Max Bobbin]

I am trying to show that if P is a polynomial, and the nth derivative of P is a constant, then P is an nth degree polynomial. I began by using induction and proved the n=0 case, but I ran into trouble with the successor case. I was wondering if anyone has any insight or if my statement is actually incorrect and I am trying to prove something that isn't valid. I attached the statement of the code I wrote.

example
{R : Type u_2} [semiring R]
{n : ℕ}
(P : polynomial R)
(h1 : polynomial.iterated_deriv P n = C (↑n.factorial * P.leading_coeff))
:
P.nat_degree = n
:=

Edit: Changed symbol from X to P so its not confusing

[Leo Mayer]

Does mathlib have the fact that any two antiderivatives differ by a constant? That seems like it would be useful

[Max Bobbin]

I can look, that does sound useful. Mathlib has currently that if f.nat_deriv < n, then iterated_deriv f n = 0 and stuff like that, but they don't have the inverse. They have stuff depending on what f.nat_deriv is, but not something that proves f.nat_deriv

[Damiano Testa]

I would suggest using a symbol different from X for the polynomial, since that is also the symbol for the variable!

[Damiano Testa]

Also, as stated your result is false: the semiring could be trivial, its characteristic could be smaller than n,...

[Reid Barton]

and the polynomial could be 0

[Heather Macbeth]

Isn't there a classic problem here for $x^p$ with a ring of characteristic $p$?

[Damiano Testa]

I would change the goal to an inequality.

[Damiano Testa]

Then, docs#polynomial.nat_degree_derivative_le should help (I hope I guessed the right name!). EDIT: the link works now!

[Damiano Testa]

Incidentally, until a couple of days ago, the lemma used to have f.derivative.nat_degree ≤ f.nat_degree as its conclusion: you'll be probably the first to use it in its revamped form!

[Max Bobbin]

Damiano Testa
Just edited it, thank you!

[Max Bobbin]

Could you explain why this would be false? I find it confusing why the fact that if the nth derivative is constant, it doesn't entail that P is degree n. I understand that it wouldn't be true to say that if the nth derivative is zero, the degree is n-1, but it seems like it must be true if the nth derivative is a constant. Like the polynomial can't be zero if its nth derivative is a constant

[Damiano Testa]

Does this convince you?

example {R : Type*} [semiring R] {n : ℕ} [subsingleton R] (P : polynomial R)
  (h1 : polynomial.iterated_deriv P n = C (↑n.factorial * P.leading_coeff)) :
  P = 0 :=
subsingleton.elim P 0

[Damiano Testa]

Note that P = C ... means that P is constant, not that it is non-zero.

[Damiano Testa]

I think that this was Reid's example:

example {R : Type*} [semiring R] {n : ℕ} (n0 : n ≠ 0) :
  ∃ (f : polynomial R),
    f.iterated_deriv n = C (↑n.factorial * f.leading_coeff) ∧ f.nat_degree ≠ n :=
⟨0, by {simpa using n0.symm}⟩

[Max Bobbin]

Hmm, I will have to look this over more and understand it. Still new to Lean and doing math proofs so forgive me for my slow understanding, but thank you for all your help, I really appreciate it! :)

[Max Bobbin]

I think I understand what you're saying. I think my confusion lies in the fact that P being a constant does not entail it is non-zero. Follow-up question, would saying that P is non-zero then entail my above goal, or is there more to it than I am realizing?

[Damiano Testa]

There are still a number of things that could go wrong. For instance, if R is the field with two elements (or, more generally, is a ring of characteristic 2), then the second derivative of every polynomial is zero. This means that your assumption h1 is automatically satisfied in this case, when 2 ≤ n. Your example would therefore say that every polynomial has degree any natural number at least 2: you'll have a hard time convincing lean of this!

[Damiano Testa]

Heather's example can be interpreted as follows. Suppose that R is a field of characteristic p. The polynomial X ^ p + X has degree p. Its first derivative equals 1, which has degree 0, and satisfies h1 with n=1. Yet, the degree of X ^ p + X is not 1.

[Damiano Testa]

The main issue is that derivatives bring natural numbers in the exponents to multiply the terms of the polynomial. You need to have some control on whether these natural-numbers-converted-to-elements-of-R are zero or not. In general, they could be, or some product of them could be.

[Damiano Testa]

(or some product with the leading coefficient of P might)

[Johan Commelin]

@Max Bobbin You might just want to assume that you are working over a ring of characteristic 0 (maybe even a field) such as ℚ or ℝ. Then your intuition works.

[Damiano Testa]

...except if P = 0.

[Eric Rodriguez]

I will say, I have done a couple proofs relating to this stuff lately, and I didn't know docs#polynomial.iterated_deriv existed, and have been using its definition instead

[Eric Rodriguez]

Shall we de-duplicate this?

[Eric Rodriguez]

Also, I don't think hom_classes allow this, but it'd be nice for iterated homs to also be a member of the hom_class semi-automatically

[Yaël Dillies]

This is possible as a constant product of endomorphisms.

[Eric Rodriguez]

I recently made docs#polynomial.iterate_derivative_eq_zero, I think the proof for this statement shouldn't be too different to it

[Eric Rodriguez]

maybe using docs#nat.case_strong_induction_on instead of just strong induction

[Eric Wieser]

Note that for endomorphism ⇑(f^n) is usually better than ⇑f^[n] because it has a stronger type

[Eric Rodriguez]

so Eric, should we refactor all uses of docs#polynomial.iterated_deriv and the iterated derivative to use (f^n)?

[Eric Wieser]

I think that would make things easier

[Eric Wieser]

Do we have a docs#linear_map.iterate lemma?

[Eric Wieser]

Ah, it's docs#linear_map.coe_pow

[Eric Wieser]

Confusingly lots of lemmas about linear_map's pow use iterate in the name

[Eric Rodriguez]

@Jujian Zhang do you see any issues with this? You seem to have written iterated_deriv; just want to check before I embark and people think it's a bad idea

[Jujian Zhang]

Not at all. Please go ahead.

[Eric Rodriguez]

I am doing this now, and it's pretty annoying that the SNF for ↑(f^n) x is ↑f^[n] x. why did we do this?

[Yaël Dillies]

The motto was that you want to weaken the bundling as much as possible, notably because that might make different higher bundlings converge to the same weaker one.

[Eric Rodriguez]

but then you lose all the nice linear_map api, and if you really want this you can just stick pow_apply in there. i don't think it should be in the simpset by defualt

[Yaël Dillies]

... and coe_mul, coe_add ...

[Yaël Dillies]

It's perfectly acceptable to think that a rewrite might be desirable in the default simpset in a situation and not in the other. If only simp [←foo] was working, instead of having to do simp [-foo, ←foo]...

[Mario Carneiro]

simp [←foo] should already have that behavior

[Yaël Dillies]

Just yesterday I hit a case where it did not, when foo is already part of the simpset, of course.

[Eric Rodriguez]

anyways, I need to do other stuff, so if anyone wants to have a look this stuff is on branch#ericrbg/iterate_deriv. feel free to push/pull; I removed the parts of iterated_deriv.lean that already exist in the rest of the API

[Johan Commelin]

Yaël Dillies said:

Just yesterday I hit a case where it did not, when foo is already part of the simpset, of course.

Weird, I'm very sure I've done [← foo] for many foo in the default simpset and it just worked.

[Yaël Dillies]

Sorry I should have recorded how it happened.