Zulip Chat Archive

Stream: new members

Topic: polynomial degree


view this post on Zulip Damiano Testa (Sep 08 2020 at 06:07):

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

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 06:20):

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.

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 06:21):

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

view this post on Zulip Johan Commelin (Sep 08 2020 at 06:23):

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?

view this post on Zulip Damiano Testa (Sep 08 2020 at 06:23):

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!

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 06:23):

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 06:24):

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!

view this post on Zulip Damiano Testa (Sep 08 2020 at 06:25):

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.

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 06:25):

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

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 06:26):

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?

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 06:27):

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 06:27):

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!

view this post on Zulip Johan Commelin (Sep 08 2020 at 06:27):

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

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 06:27):

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 06:27):

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

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 06:27):

Because it should just all be there

view this post on Zulip Johan Commelin (Sep 08 2020 at 06:28):

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 06:28):

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

view this post on Zulip Johan Commelin (Sep 08 2020 at 06:28):

I'm not really aware of it

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 06:28):

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

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 06:29):

I was filling in holes in the with_bot library yesterday.

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 06:30):

Degree is just defined to be some max

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 06:30):

Or some sup

view this post on Zulip Damiano Testa (Sep 08 2020 at 06:32):

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

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 06:50):

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

view this post on Zulip Mario Carneiro (Sep 08 2020 at 07:27):

: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

view this post on Zulip Mario Carneiro (Sep 08 2020 at 07:29):

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 07:31):

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,...

view this post on Zulip Mario Carneiro (Sep 08 2020 at 07:32):

write them down

view this post on Zulip Damiano Testa (Sep 08 2020 at 07:32):

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

view this post on Zulip Mario Carneiro (Sep 08 2020 at 07:32):

don't worry about that

view this post on Zulip Mario Carneiro (Sep 08 2020 at 07:32):

just statements

view this post on Zulip Damiano Testa (Sep 08 2020 at 07:32):

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

view this post on Zulip Mario Carneiro (Sep 08 2020 at 07:32):

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 07:33):

ok, I will get to it!

view this post on Zulip Mario Carneiro (Sep 08 2020 at 07:33):

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 09:01):

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?

view this post on Zulip Damiano Testa (Sep 08 2020 at 09:02):

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).

view this post on Zulip Johan Commelin (Sep 08 2020 at 09:03):

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

view this post on Zulip Johan Commelin (Sep 08 2020 at 09:04):

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 09:05):

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 09:05):

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

view this post on Zulip Johan Commelin (Sep 08 2020 at 09:06):

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 09:06):

I accepted!

view this post on Zulip Damiano Testa (Sep 08 2020 at 09:06):

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

view this post on Zulip Johan Commelin (Sep 08 2020 at 09:07):

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 09:07):

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

view this post on Zulip Johan Commelin (Sep 08 2020 at 09:07):

Hmm, not really

view this post on Zulip Johan Commelin (Sep 08 2020 at 09:07):

No worries

view this post on Zulip Damiano Testa (Sep 08 2020 at 09:07):

Ok

view this post on Zulip Damiano Testa (Sep 08 2020 at 09:08):

I can copy the file elsewhere, of course

view this post on Zulip Kevin Buzzard (Sep 08 2020 at 09:08):

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

view this post on Zulip Johan Commelin (Sep 08 2020 at 09:08):

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

view this post on Zulip Johan Commelin (Sep 08 2020 at 09:08):

Are you hosting the project on github?

view this post on Zulip Damiano Testa (Sep 08 2020 at 09:10):

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...

view this post on Zulip Johan Commelin (Sep 08 2020 at 09:10):

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.

view this post on Zulip Damiano Testa (Sep 08 2020 at 09:10):

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 09:11):

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!

view this post on Zulip Damiano Testa (Sep 08 2020 at 09:17):

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

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 09:17):

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 09:40):

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 11:43):

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 11:44):

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

view this post on Zulip Shing Tak Lam (Sep 08 2020 at 11:50):

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]

view this post on Zulip Mario Carneiro (Sep 08 2020 at 11:50):

The statement doesn't have anything to do with support

view this post on Zulip Mario Carneiro (Sep 08 2020 at 11:51):

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 11:52):

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...

view this post on Zulip Damiano Testa (Sep 08 2020 at 11:53):

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!

view this post on Zulip Mario Carneiro (Sep 08 2020 at 11:53):

you can change the type to s.nonempty

view this post on Zulip Mario Carneiro (Sep 08 2020 at 11:54):

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

view this post on Zulip Damiano Testa (Sep 08 2020 at 11:54):

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!

view this post on Zulip Mario Carneiro (Sep 08 2020 at 11:55):

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

view this post on Zulip Shing Tak Lam (Sep 08 2020 at 11:56):

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 _

view this post on Zulip Damiano Testa (Sep 08 2020 at 11:57):

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.

view this post on Zulip Damiano Testa (Sep 08 2020 at 11:58):

Shing Tak Lam said:

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

Very useful: thank you!

view this post on Zulip Bryan Gin-ge Chen (Sep 10 2020 at 18:39):

Damiano Testa said:

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

For future reference, the corresponding PR is #4069.


Last updated: May 14 2021 at 12:18 UTC