Zulip Chat Archive

Stream: maths

Topic: Proofs About Polynomial Degree Based on Derivative


Max Bobbin (Apr 08 2022 at 01:05):

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 (Apr 08 2022 at 01:07):

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

Max Bobbin (Apr 08 2022 at 01:10):

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 (Apr 08 2022 at 01:11):

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

Damiano Testa (Apr 08 2022 at 01:12):

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

Reid Barton (Apr 08 2022 at 01:12):

and the polynomial could be 0

Heather Macbeth (Apr 08 2022 at 01:12):

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

Damiano Testa (Apr 08 2022 at 01:14):

I would change the goal to an inequality.

Damiano Testa (Apr 08 2022 at 01:14):

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

Damiano Testa (Apr 08 2022 at 01:21):

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 (Apr 08 2022 at 01:49):

Damiano Testa
Just edited it, thank you!

Max Bobbin (Apr 08 2022 at 01:50):

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 (Apr 08 2022 at 02:17):

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 (Apr 08 2022 at 02:18):

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

Damiano Testa (Apr 08 2022 at 02:34):

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 (Apr 08 2022 at 04:13):

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 (Apr 08 2022 at 04:19):

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 (Apr 08 2022 at 04:34):

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 (Apr 08 2022 at 04:38):

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 (Apr 08 2022 at 04:41):

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 (Apr 08 2022 at 04:41):

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

Johan Commelin (Apr 08 2022 at 05:20):

@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 (Apr 08 2022 at 06:00):

...except if P = 0.

Eric Rodriguez (Apr 08 2022 at 08:21):

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 (Apr 08 2022 at 08:22):

Shall we de-duplicate this?

Eric Rodriguez (Apr 08 2022 at 08:22):

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 (Apr 08 2022 at 08:23):

This is possible as a constant product of endomorphisms.

Eric Rodriguez (Apr 08 2022 at 08:25):

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 (Apr 08 2022 at 08:26):

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

Eric Wieser (Apr 08 2022 at 11:35):

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

Eric Rodriguez (Apr 08 2022 at 13:56):

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

Eric Wieser (Apr 08 2022 at 15:03):

I think that would make things easier

Eric Wieser (Apr 08 2022 at 15:03):

Do we have a docs#linear_map.iterate lemma?

Eric Wieser (Apr 08 2022 at 15:03):

Ah, it's docs#linear_map.coe_pow

Eric Wieser (Apr 08 2022 at 15:04):

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

Eric Rodriguez (Apr 08 2022 at 16:21):

@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 (Apr 08 2022 at 16:28):

Not at all. Please go ahead.

Eric Rodriguez (Apr 08 2022 at 22:54):

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 (Apr 08 2022 at 22:56):

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 (Apr 08 2022 at 23:03):

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 (Apr 08 2022 at 23:08):

... and coe_mul, coe_add ...

Yaël Dillies (Apr 08 2022 at 23:09):

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 (Apr 08 2022 at 23:10):

simp [←foo] should already have that behavior

Yaël Dillies (Apr 08 2022 at 23:11):

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

Eric Rodriguez (Apr 08 2022 at 23:56):

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 (Apr 09 2022 at 06:27):

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 (Apr 09 2022 at 08:51):

Sorry I should have recorded how it happened.


Last updated: Dec 20 2023 at 11:08 UTC