Zulip Chat Archive
Stream: maths
Topic: Limit of polynomials
Riccardo Brasca (Nov 27 2020 at 20:25):
I have a monic polynomial $P$ (with integer coefficients if that matters, it is the cyclotomic polynomial). I need that for $x$ large enough $P(x)$ is bigger than $1$ (to be precise I am interested only at this result for $x$ an integer). Normally I would just say that the limit for $x \to +\infty$ of $P(x)$ is $+\infty$.
How can I start proving this in lean? Should I look in the analysis part of the library? I had a quick look but I didn't find any polynomial.
Thank you!
Reid Barton (Nov 27 2020 at 20:28):
Is docs#polynomial.tendsto_infinity close enough?
Riccardo Brasca (Nov 27 2020 at 20:31):
Ah, it was in topology, non analysis!
Reid Barton (Nov 27 2020 at 20:31):
This was for the fundamental theorem of algebra so it might not be very suited to the integers
Heather Macbeth (Nov 27 2020 at 20:31):
There's docs#tendsto_pow_at_top for semirings
Riccardo Brasca (Nov 27 2020 at 20:33):
It is exactly what I need, thank you!! It is even already translated in $\varepsilon\delta$ terms... I thought I had to learn something about filters.
Patrick Massot (Nov 28 2020 at 01:09):
That's too bad! But I'm sure you'll have other opportunities to learn about filters.
Kevin Buzzard (Nov 28 2020 at 07:49):
Maybe we should remove those epsilon delta translations, they're probably not used in mathlib and if they are then we're doing it wrong
Anatole Dedecker (Nov 28 2020 at 09:24):
Hmmmmmm I don't agree on that (but I may be absolutely wrong, this is only my naive opinion). If I understand it correctly, the goal of mathlib is not only to be a big selfcontained collection of theorems, it should also be usable by external users to make their project in Lean. So, although epsilon delta definitions should not be used inside mathlib itself, I think there might be a lot of people who want to do analysis using mathlib without having to learn all of the theory behind filters.
Eric Wieser (Nov 28 2020 at 09:39):
If there's a strong urge to remove them, they could go into an "examples" directory or something so that we still ensure that they build and users who don't know about filters yet can use them to help learn.
Eric Wieser (Nov 28 2020 at 09:39):
Perhaps we need a "filters game"?
Sebastien Gouezel (Nov 28 2020 at 10:20):
Why would you want to remove the epsilondelta properties? There are some situations where these are precisely the way you will need to use a limit, so they definitely belong to mathlib.
Riccardo Brasca (Nov 28 2020 at 10:22):
My, very personal, opinion is that it should be easy to obtain concrete results like the one I needed. I have no idea how hard it is to translate a result in the language of filters to something concrete, but I guess not that much. BTW, I don't see in mathlib any result about limit of polynomials using filters...
Riccardo Brasca (Nov 28 2020 at 10:27):
I mean that results like "if $f$ tends to $\infty$, written in the language of filters, then blah blah" are definitely useful. I agree that having explicitly that " for all $M \in \mathbf{R}$ there exist $x_0 \in \mathbf{R}$ such that $\exp(x) > M$ if $x > x_0$" is quite redundant.
Kevin Buzzard (Nov 28 2020 at 10:27):
Oh sorry, I was just trying to wind Riccardo up! I wasn't being at all serious
Kevin Buzzard (Nov 28 2020 at 10:28):
But I do agree there should be a filter game
Riccardo Brasca (Nov 28 2020 at 10:31):
Don't worry, I will learn filters anyway :grinning_face_with_smiling_eyes:
Kevin Buzzard (Nov 28 2020 at 10:35):
Maybe you should write it :D
Kevin Buzzard (Nov 28 2020 at 10:36):
They are hugely powerful. I spent some time over the summer writing proofs like "closed subspace of compact space is compact" and "compact subspace of Hausdorff space is closed" using the open set proof, and I don't know if this has something to do with type theory or what, but the proofs were much longer than the filter proofs.
Reid Barton (Nov 28 2020 at 10:36):
Really a topology game in general would make a great sequel
Kevin Buzzard (Nov 28 2020 at 10:37):
Right, I was just thinking this. Building up the basic results in a first undergrad topology course using filters would be interesting for lots of reasons.
Kevin Buzzard (Nov 28 2020 at 10:40):
One reason the open set proofs were a bit clunky was that we use the axiom of choice all the time in the natural proofs. For example, we say "say X is a compact subset of a Hausdorff space. Fix a not in X. Now for every x in X, let's choose disjoint opens containing a and x (using the axiom of choice). Cover X by the xopens, take a finite subcover, take the intersection of the finitely many corresponding neighbourhoods of a and there's your open neighbourhood of a disjoint from X". This is a very natural proof for mathematicians, but there is some classical.some
involved in Lean.
Kevin Buzzard (Nov 28 2020 at 10:42):
But the moment you start asking about a constructive proof you run into issues that there is more than one constructive statement of the theorem. For example does "Hausdorff" mean "given a and x, there exists disjoint opens" or does it mean "there exists a function which takes two distinct elements and spits out two disjoint opens"? These are different things constructively.
Kevin Buzzard (Nov 28 2020 at 10:45):
I supervised an undergraduate project on doing topology with filters last year, because I know from experience that one way to learn a topic is to make an undergraduate do a project in it and then you have to answer their questions. I was really impressed by the supershort proof that an arbitrary product of compact spaces was compact.
Kevin Buzzard (Nov 28 2020 at 10:46):
This theorem was filed in my mind up until that point as "elementary, but quite tricky".
Anatole Dedecker (Nov 28 2020 at 10:51):
On the specific topic of proving analysis results about polynomial functions, I was also surprised to see that there was almost nothing in mathlib. I wanted to give it a try but I didn't know which setup I should have used (the way typeclass hierarchy is set up is still a bit of a mystery to me), so I did nothing useful. Maybe I should have done it with reals first and then try to generalize.
Mario Carneiro (Nov 28 2020 at 10:55):
Kevin Buzzard said:
But the moment you start asking about a constructive proof you run into issues that there is more than one constructive statement of the theorem. For example does "Hausdorff" mean "given a and x, there exists disjoint opens" or does it mean "there exists a function which takes two distinct elements and spits out two disjoint opens"? These are different things constructively.
Or does it mean "if every pair of opens around a and x intersect then a = x"
Kevin Buzzard (Nov 28 2020 at 10:58):
The funniest (for my sense of humour at least) part of this was that when I was raging about all this on Twitter, arguing that the maths proof I presented was clearly the "natural" one, a whole bunch of constructivists popped up (as they often do on Twitter) and started explaining the proper way to do it, and they all had different ideas. I hadn't really internalised that there were lots of different kinds of constructivists. One said that all topology should be done classically, one said that I should be using locales, one said my definition of Hausdorff was wrong, one said it was right but instead of choosing a set I should use all the sets (and this argument does work, I checked it in Lean).
Kevin Buzzard (Nov 28 2020 at 11:00):
As for limits of polynomials, I quite agree that we are missing tons of stuff. At Xena last week I wrote over 20 lines of code proving (in a way a beginner could understand) that the limit of $\frac{n+7}{n}$ was 1 as $n$ tended to infinity, and then the next question was to prove that the limit of $\frac{n}{n+7}$ was 1 and the students were like "please skip it". Then the next one was $\frac{n^2+5n+6}{n^32}$ and they were like "please skip that one too".
Kevin Buzzard (Nov 28 2020 at 11:02):
And because I couldn't really imagine using any techniques which we hadn't seen already in the first proof, I agreed and we went on to other questions. The computations really were a bit painful, and the reason is simply that nobody has tried to make them easier  certainly myself I'd rather be proving that if $a_n\to l$ and $b_n\to m$ then $a_nb_n\to lm$ by building up a little library of results about limits (which I should say I defined by hand using the epsilonN definition), I think this is an intrinsically more interesting thing to be doing in Lean.
Kevin Buzzard (Nov 28 2020 at 11:03):
Kevin Buzzard (Nov 28 2020 at 11:06):
use (ceil ((37 : ℝ) / ε)).nat_abs,
says "OK so in this proof we'll be skipping between the reals, the integers and the naturals". I think there's exists_nat_gt
in the library and perhaps this would have made life a bit easier, but there are clearly a bunch of things one could easily prove here which would enable people to compute the limit of $p(x)/q(x)$ as $x\to\infty$ for e.g. all polynomials $p,q$ and a bunch of other things too (e.g. polynomial plus bounded function, in many cases), for $x$ running through nat or pnat (as the lecturer insists on using) or the reals etc.
Patrick Massot (Nov 28 2020 at 11:07):
What is missing here are lots of lemmas about asymptotics (little o and big O).
Kevin Buzzard (Nov 28 2020 at 11:08):
Yes, and Eberl just did them in Isabelle/HOL so we have something to work on too. Not sure how interested he was in sequences though.
Anatole Dedecker (Nov 28 2020 at 11:08):
I was hoping that this could be simplified by what I defined in #4979 : the idea would be to say : n ~ n
and n+7 ~ n
so n/(n+7) ~ n/n = 1
. But the thing I haven't managed to do yet is prove that every polynomial is equivalent to its leading term at infinity
Patrick Massot (Nov 28 2020 at 11:27):
Yes, Anatole, this is exactly what I meant.
Kevin Buzzard (Nov 28 2020 at 11:33):
oh here you can of course just use some easy epsilon delta argument :P (or maybe an epsilon N argument in this case)
Anatole Dedecker (Nov 28 2020 at 11:40):
Yeah I guess the problem really is I wanted to start with the most general statement so I got stuck on simple things. I'll give it a try again when I have some time
Jasmin Blanchette (Nov 28 2020 at 20:18):
Eberl also has a nice real_asymp
tactic based on Multiseries and inspired by some Maple implementation. Maybe it can serve as inspiration (if it doesn't already).
Riccardo Brasca (Dec 02 2020 at 13:37):
Is there any reason why is_absolute_value
takes value in a linear_ordered_field
rather then in a linear_ordered_ring
(maybe even semiring)? The definition makes sense, and since we have results like polynomial.tendsto_infinity
that work, for example, for polynomials over ℤ
, we can obtain directly that $P(x)$ is big enough as an integer, where $P \in \mathbf{Z}[x]$, without going to ℚ
and then going back to ℤ
.
Kevin Buzzard (Dec 02 2020 at 16:56):
Make a new branch of mathlib, change the definition of is_absolute_value
, push to github and tomorrow when you remember, take a look and see if it compiled!
Riccardo Brasca (Dec 02 2020 at 17:10):
I just did that locally: the first properties in data.real.cau_seq
can be generalized easily to the case of linear_ordered_comm_ring R
, but then I tried to modify the proof that $\lim{x \to \infty} P(x) = \infty$ and realized that this is probably false! If in R
there is an infinitesimal element ε
but no infinite elements then the polynomial C ε * X
is bounded :dizzy:
Anatole Dedecker (Dec 09 2020 at 18:38):
Ok so I have good and bad news.

I've managed to prove that for any polynomial
P
on anormed_linear_ordered_field
, we have(λ x, eval x P) ~[at_top] (λ x, P.leading_coeff * x ^ P.nat_degree)
, from which I deduced the three cases for the limit of P/Q depending on the degree (either infinity, 0, or ratio of leading coeffs). I'll PR all of this soon 
I tried proving a random example using these. But it is still incredibly boring because of the lack of automation about polynomial, which makes it quite boring. This gives the following proof, which is very long, but most of the length comes from proving degrees. If you have any advice on how to make this shorter, I'll take it !
Anatole Dedecker (Dec 09 2020 at 18:39):
example : tendsto (λ x : ℝ, (3*x^2  6*x + 7)/(12*x^2 + 4)) at_top (𝓝 (1/4)) :=
begin
have key1 : ∀ x:ℝ, 3*x^26*x+7 = eval x (monomial 2 3  monomial 1 6 + monomial 0 7) := by simp,
have key2 : ∀ x:ℝ, 12*x^2+4 = eval x (monomial 2 12 + monomial 0 4) := by simp,
simp_rw [key1, key2],
set A : polynomial ℝ := monomial 2 3  monomial 1 6 + monomial 0 7,
set B : polynomial ℝ := monomial 2 12 + monomial 0 4,
have degA1 : (monomial 2 3 : polynomial ℝ).degree = (2:ℕ) := degree_monomial _ (by norm_num),
have degA2 : (monomial 1 6 : polynomial ℝ).degree = (1:ℕ) := degree_monomial _ (by norm_num),
have degA3 : (monomial 0 7 : polynomial ℝ).degree = (0:ℕ) := degree_monomial _ (by norm_num),
have degA4 : (monomial 2 3  monomial 1 6 : polynomial ℝ).degree = (2:ℕ) :=
degA1 ▸ degree_sub_eq_left_of_degree_lt (by rw [degA1, degA2] ; dec_trivial),
have degA : A.degree = (2:ℕ) :=
degA4 ▸ degree_add_eq_left_of_degree_lt (by rw [degA3, degA4] ; dec_trivial),
have degB1 : (monomial 2 12 : polynomial ℝ).degree = (2:ℕ) := degree_monomial _ (by norm_num),
have degB2 : (monomial 0 4 : polynomial ℝ).degree = (0:ℕ) := degree_monomial _ (by norm_num),
have degB : B.degree = (2:ℕ) :=
degB1 ▸ degree_add_eq_left_of_degree_lt (by rw [degB1, degB2] ; dec_trivial),
have leadA : A.leading_coeff = 3,
{ unfold leading_coeff nat_degree,
rw degA,
simp only [coeff_add,coeff_sub,coeff_monomial,if_true,option.get_or_else_coe,eq_self_iff_true],
norm_num },
have leadB : B.leading_coeff = 12,
{ unfold leading_coeff nat_degree,
rw degB,
simp only [coeff_add,coeff_sub,coeff_monomial,if_true,option.get_or_else_coe,eq_self_iff_true],
norm_num },
convert A.eval_div_tendsto_leading_coeff_div_of_degree_eq B (degA.trans degB.symm) using 2,
rw [leadA, leadB],
norm_num
end
Johan Commelin (Dec 09 2020 at 20:52):
I think that if there is a char_zero R
floating around, then some norm_num
plugin should be able to handle a lot of these computations. But unfortunately I don't know how to write such a plugin.
Alex J. Best (Dec 09 2020 at 21:25):
A little while back in https://leanprover.zulipchat.com/#narrow/stream/239415metaprogramming.2F.20tactics/topic/constant.20polynomial.20tactic/near/201179210 @Jack J Garzella was thinking about making a tactic for this sort of stuff, not sure how far it got though
Jack J Garzella (Dec 27 2020 at 06:11):
@Anatole Dedecker @Alex J. Best I was hoping to make such a tactic. Unfortunately, I got busy (I'm a first year graduate student) before I could get started, so I haven't actually done anything :/. Most likely I won't get to do much Lean until March, so if it's something you're interested in have at it.
Last updated: May 18 2021 at 07:19 UTC