polynomial degree

Stream: new members

[Damiano Testa]

Dear All,

more struggles... I am trying to prove something analogous to the code below, but I can't. Also in the specific example below, I am unable to find a proof of the fact that the nat_degree of a non-zero polynomial equals the maximum of the support. What am I doing wrong? How can I prove this? I always have problems accessing the xx-part of option xx.

Thank you!

import tactic
import data.polynomial.degree.basic

open polynomial

lemma defs {R : Type*} [semiring R] {f : polynomial R} {h : f.support.nonempty} : nat_degree f = f.support.max' h :=
begin
  sorry,
end

#exit

[Kevin Buzzard]

Hey, you ask good questions now, and in a good way. You could ask this in #maths. The question seems not to be one about polynomials at all -- this looks like something which could/should be in the finsupp API, and there's a lot to get your head around with finsupps.

[Kevin Buzzard]

I would have thought that f \ne 0 was the canonical way to say that f was non-zero, rather than f.support.nonempty.

[Johan Commelin]

Kevin Buzzard said:

Hey, you ask good questions now, and in a good way. You could ask this in #maths. The question seems not to be one about polynomials at all -- this looks like something which could/should be in the finsupp API, and there's a lot to get your head around with finsupps.

Mwah... nat_degree is not really something about finsupps, is it?

[Damiano Testa]

Kevin Buzzard said:

Hey, you ask good questions now, and in a good way. You could ask this in #maths. The question seems not to be one about polynomials at all -- this looks like something which could/should be in the finsupp API, and there's a lot to get your head around with finsupps.

Thank you! I am glad that some progress can be detected from the outside!

To be honest, I try to avoid finsets as much as possible, since I do not really understand them. This is why I thought that this was an issue with polynomials. I am happy to see a solution using finsupp, though!

[Kevin Buzzard]

No but degree is, and degree equals nat_degree if f isn't zero

[Damiano Testa]

Kevin Buzzard said:

I would have thought that f \ne 0 was the canonical way to say that f was non-zero, rather than f.support.nonempty.

I am happy with either: I have a proof of the equivalence of f \neq 0 and f.support.nonempty!

[Damiano Testa]

Kevin Buzzard said:

No but degree is, and degree equals nat_degree if f isn't zero

Exactly! As much as I try to steer away from degree, nat_degreee is defined in terms of degree and that makes things very hard for me.

[Kevin Buzzard]

Right. The point I'm making is that if you want to state a bunch of lemmas and you switch between the two notions in the statements of the lemmas then you'll forever have to be rewriting the equivalence when you're trying to use your lemmas

[Kevin Buzzard]

I'm sorry the API isn't there, this shouldn't be too hard. Just sorry it and move on, and I'll fix it when I get to a computer?

[Kevin Buzzard]

You just need some result of the form finset.sup = finset.max which is surely there

[Damiano Testa]

Kevin Buzzard said:

I'm sorry the API isn't there, this shouldn't be too hard. Just sorry it and move on, and I'll fix it when I get to a computer?

Ok, thank you! I am curious to see how to fix it, since this might teach me how to deal with options!

[Johan Commelin]

lemma defs {f : polynomial R} (h : f.support.nonempty) :
  f.nat_degree = f.support.max' h :=
begin
  apply le_antisymm,
  { apply finset.le_max',
    rw finsupp.mem_support_iff,
    show f.leading_coeff ≠ 0,
    rw [ne.def, polynomial.leading_coeff_eq_zero],
    rwa [finset.nonempty_iff_ne_empty, ne.def, finsupp.support_eq_empty] at h, },
  { apply polynomial.le_nat_degree_of_ne_zero,
    have := finset.max'_mem _ h,
    rwa finsupp.mem_support_iff at this, }
end

[Kevin Buzzard]

The idea is that users like us shouldn't have to worrying about this sort of thing at all

[Damiano Testa]

@Johan Commelin thanks! I'll use your code right now!

[Kevin Buzzard]

Because it should just all be there

[Johan Commelin]

Kevin, do we have a notion of degree for finsupps?

[Damiano Testa]

Ok, I am slowly understanding the difference between things that I should worry about and things that I should not!

[Johan Commelin]

I'm not really aware of it

[Kevin Buzzard]

But actually the reason we discover holes in the library like this is because people are actually using the library

[Kevin Buzzard]

I was filling in holes in the with_bot library yesterday.

[Kevin Buzzard]

Degree is just defined to be some max

[Kevin Buzzard]

Or some sup

[Damiano Testa]

Yes, and to work with at_infty I was trying to work with with_top and trailing_degrees, but it got ugly...

[Kevin Buzzard]

One should imagine the API you want and then find it or complain that it's not there :-)

[Mario Carneiro]

:point_up: This. It is actually really valuable to spec out the API when you find it missing. This is the hard part of library building - the proofs are usually all trival

[Mario Carneiro]

Especially, once you find an individual proof going not as smoothly as you would hope, rather than making a huge proof anyway you should step back and ask yourself what theorem you would like to have found in the library, and write its statement precisely. Then PR it

[Damiano Testa]

Mario Carneiro said:

Especially, once you find an individual proof going not as smoothly as you would hope, rather than making a huge proof anyway you should step back and ask yourself what theorem you would like to have found in the library, and write its statement precisely. Then PR it

Ok, so one thing that would be very valuable for me, at the moment, would be to have all the statements about degree, nat_degree, leading_coeff,... (in data.polynomial.degree.basic) available also for trailing_degree, nat_trailing_degree, trailing_coeff,...

[Mario Carneiro]

write them down

[Damiano Testa]

I have started this, and got quite a bit into it, but could not reprove everything

[Mario Carneiro]

don't worry about that

[Mario Carneiro]

just statements

[Damiano Testa]

ok, writing them down (and almost proving them) was a simple matter of using the right sed. with a couple of exceptions!

[Mario Carneiro]

if you post them here people can probably prove them in a few minutes and then bam you've got a PR

[Damiano Testa]

ok, I will get to it!

[Mario Carneiro]

the important part is to identify those pain points and what statements would avoid them

[Damiano Testa]

Ok, I have converted the statements in data.polynomial.degree.basic to their upside down. The proofs that just went through with mechanical twitching are not commented. The proofs that do not work are commented. Should I simply make a gist and post the link here?

[Damiano Testa]

I am not necessarily interested in all these lemmas. What I do care about is that the trailing coefficient of a product of polynomials is the product of the trailing coefficients (at least when the product of the trailing coefficients is non-zero).

[Johan Commelin]

Even better than a gist, would be to push it to a branch of mathlib

[Johan Commelin]

Do you already have write access to mathlib branches on github?

[Damiano Testa]

I am not sure: besides being new to Lean, I am also new to github...

[Damiano Testa]

I feel like I am constantly wasting everybody's time with my not being able to do basic stuf...

[Johan Commelin]

https://github.com/leanprover-community/mathlib/invitations

[Damiano Testa]

I accepted!

[Damiano Testa]

(I assume that this was what I was supposed to do! Ahaha)

[Johan Commelin]

So, did you write those lemmas in a file inside mathlib?

[Damiano Testa]

I wrote them inside a project that I created. Does that count?

[Johan Commelin]

Hmm, not really

[Johan Commelin]

No worries

[Damiano Testa]

Ok

[Damiano Testa]

I can copy the file elsewhere, of course

[Kevin Buzzard]

Damiano Testa said:

I feel like I am constantly wasting everybody's time with my not being able to do basic stuf...

For me this was a really important part of the learning process. I bombarded Mario with questions about all 1st year undergrad material (algebra, analysis, ...) and MSc level algebra

[Johan Commelin]

In that case, just save the file, commit, and push it to your project

[Johan Commelin]

Are you hosting the project on github?

[Damiano Testa]

Johan Commelin said:

Are you hosting the project on github?

I like to think that I am, but I am worried to moving it to github, since I fear that I might copy the empty project in github to my computer, instead of uploading the files on my computer to github...

[Johan Commelin]

https://www.youtube.com/watch?v=Bnc8w9lxe8A&list=PLlF-CfQhukNnxF1S22cNGKyfOrd380NUv&index=7&t=0s
This might be an interesting video to watch, if you have some spare minutes.

[Damiano Testa]

I push the github button on VSC every once in a while, though

[Damiano Testa]

Johan Commelin said:

https://www.youtube.com/watch?v=Bnc8w9lxe8A&list=PLlF-CfQhukNnxF1S22cNGKyfOrd380NUv&index=7&t=0s
This might be an interesting video to watch, if you have some spare minutes.

I will watch later, thanks!

[Damiano Testa]

While I watch the video and digest it, here is the gist

https://gist.github.com/adomani/a87231b5c4e8eb815a0575b026e7ce52

[Damiano Testa]

(there may be mistakes in some of the statements, since reversing all the le signs is not as easy to do!)

[Damiano Testa]

I am watching the video and I have added and committed a file.

[Damiano Testa]

Still continuing with problems involving degrees, minima and infima: do you know how to prove the lemma below? Thanks!

import tactic
import data.polynomial.degree.basic

open polynomial

lemma minmin {R : Type*} [semiring R] {f : polynomial R} {fne : f.support.nonempty} {fnz : f ≠ 0} : f.support.min' fne ∈ f.support.min :=
begin
  sorry,
end

[Damiano Testa]

(If you prefer to have {fne : f ≠ 0} as a hypothesis, go ahead!)

[Shing Tak Lam]

lemma minmin {R : Type*} [semiring R] {f : polynomial R} {fne : f.support.nonempty} {fnz : f ≠ 0} :
  f.support.min' fne ∈ f.support.min :=
by rw [option.mem_def, finset.min', option.some_get]

[Mario Carneiro]

The statement doesn't have anything to do with support

[Mario Carneiro]

it's a good idea to generalize away as many details of the original context while retaining the essence of the statement, in this case yielding a statement about finsets

[Damiano Testa]

Mario Carneiro said:

it's a good idea to generalize away as many details of the original context while retaining the essence of the statement, in this case yielding a statement about finsets

I normally try to do that, but in this case, I was unable to formulate f.support.min' fne without the fne : f.support.nonempty assumption...

[Damiano Testa]

Shing Tak Lam said:

lemma minmin {R : Type*} [semiring R] {f : polynomial R} {fne : f.support.nonempty} {fnz : f ≠ 0} :
  f.support.min' fne ∈ f.support.min :=
by rw [option.mem_def, finset.min', option.some_get]

Thanks! I do not understand the proof, but Lean does!

[Mario Carneiro]

you can change the type to s.nonempty

[Mario Carneiro]

you can look at the type of finset.min' to see what things are needed to state it

[Damiano Testa]

Mario Carneiro said:

you can change the type to s.nonempty

Ah, I see what you are saying! I should have made f.support the subject!

[Mario Carneiro]

another thing to notice about shing tak lam's proof is that the lemmas are also not polynomial specific, which suggests that some "trivial generalization" is at play

[Shing Tak Lam]

Here's the proof for any finset (with some comments), and using it in your lemma

import tactic
import data.polynomial.degree.basic

open polynomial

lemma finset.min'_mem_min {α : Type} [decidable_linear_order α] {s : finset α} (hs : s.nonempty) :
  s.min' hs ∈ s.min :=
begin
  -- Unfold the definition of ∈ for options
  rw option.mem_def,
  -- Unfold the definition of min'
  rw finset.min',
  -- some (option.get ↥(s.min.is_some)) is just s.min
  rw option.some_get,
end

lemma minmin {R : Type*} [semiring R] {f : polynomial R} {fne : f.support.nonempty} {fnz : f ≠ 0} :
  f.support.min' fne ∈ f.support.min :=
finset.min'_mem_min _

[Damiano Testa]

Ok, since this is a step in a proof about degrees of polynomials, and, in my mind, finsets are not what I think when I am thinking about polynomials, I overlooked that I should have formulated it with finsets.

[Damiano Testa]

Shing Tak Lam said:

Here's the proof for any finset (with some comments), and using it in your lemma

Very useful: thank you!

[Bryan Gin-ge Chen]

Damiano Testa said:

I am watching the video and I have added and committed a file.

For future reference, the corresponding PR is #4069.