Limit of polynomials

Stream: maths

[Riccardo Brasca]

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]

Is docs#polynomial.tendsto_infinity close enough?

[Riccardo Brasca]

Ah, it was in topology, non analysis!

[Reid Barton]

This was for the fundamental theorem of algebra so it might not be very suited to the integers

[Heather Macbeth]

There's docs#tendsto_pow_at_top for semirings

[Riccardo Brasca]

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]

That's too bad! But I'm sure you'll have other opportunities to learn about filters.

[Kevin Buzzard]

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]

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 self-contained 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]

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]

Perhaps we need a "filters game"?

[Sebastien Gouezel]

Why would you want to remove the epsilon-delta 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]

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]

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]

Oh sorry, I was just trying to wind Riccardo up! I wasn't being at all serious

[Kevin Buzzard]

But I do agree there should be a filter game

[Riccardo Brasca]

Don't worry, I will learn filters anyway :grinning_face_with_smiling_eyes:

[Kevin Buzzard]

Maybe you should write it :D

[Kevin Buzzard]

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]

Really a topology game in general would make a great sequel

[Kevin Buzzard]

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]

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 x-opens, 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]

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]

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 super-short proof that an arbitrary product of compact spaces was compact.

[Kevin Buzzard]

This theorem was filed in my mind up until that point as "elementary, but quite tricky".

[Anatole Dedecker]

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]

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]

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]

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^3-2}$ and they were like "please skip that one too".

[Kevin Buzzard]

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 epsilon-N definition), I think this is an intrinsically more interesting thing to be doing in Lean.

[Kevin Buzzard]

https://github.com/ImperialCollegeLondon/M40002/blob/60f07e2b2e1e460495e9a9756df44b5e0dedcff3/src/solutions_sheet_three.lean#L28-L55

[Kevin Buzzard]

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]

What is missing here are lots of lemmas about asymptotics (little o and big O).

[Kevin Buzzard]

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]

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]

Yes, Anatole, this is exactly what I meant.

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

Ok so I have good and bad news.

• I've managed to prove that for any polynomial P on a normed_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]

example : tendsto (λ x : ℝ, (3*x^2 - 6*x + 7)/(12*x^2 + 4)) at_top (𝓝 (1/4)) :=
begin
  have key1 : ∀ x:ℝ, 3*x^2-6*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]

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]

A little while back in https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.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]

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