Stream: Is there code for X?

Topic: Computing limit as x approaches some number or infinity

Formally Verified Waffle Maker (Oct 25 2020 at 20:28):

Is there a way to compute the limit of some function as x approaches 2, or x approaches negative infinity?

Bryan Gin-ge Chen (Oct 25 2020 at 20:32):

What do you mean by "compute" exactly? Regardless, the answer is probably not in Lean, since the reals in mathlib are noncomputable.

Bryan Gin-ge Chen (Oct 25 2020 at 20:34):

mathlib does contain proofs of several specific limit computations in analysis.specific_limits.

Kevin Buzzard (Oct 25 2020 at 20:35):

You might be able to prove that a certain number is a limit, but Lean is not really for computing, it's for proving.

Formally Verified Waffle Maker (Oct 25 2020 at 20:37):

That's unfortunate, since it would be nice if Lean could help mathematicians by having the ability to compute certain expressions, like a CAS.

Mario Carneiro (Oct 25 2020 at 20:37):

Well, it again depends on what you mean by "compute", because there are several tactics that get within striking distance of computing limits like a CAS

Formally Verified Waffle Maker (Oct 25 2020 at 20:38):

By compute I mean calculating $\displaystyle\lim_{x\to\infty} 2x$ for instance to be $\infty$.

Mario Carneiro (Oct 25 2020 at 20:39):

that's certainly doable with some elbow grease

Mario Carneiro (Oct 25 2020 at 20:39):

not sure how far simp lemmas will take you to get that exact result

Mario Carneiro (Oct 25 2020 at 20:40):

we have lemmas for computing derivatives but I don't know about limits, unless the function is continuous and we can just evaluate it

Bryan Gin-ge Chen (Oct 25 2020 at 20:41):

It's provable using e.g. docs#filter.tendsto_at_top_mono, but there isn't currently a way to just throw the equivalent of $\displaystyle\lim_{x\to\infty} 2x$ into Lean and get ∞ out.

Patrick Massot (Oct 25 2020 at 20:42):

Let's be clear: what Bryan says is clearly a defect that will have to be fixed at some point, but this require work. It's not something that is meant to stay like this forever.

Mario Carneiro (Oct 25 2020 at 20:43):

One reasonable general approach here would be to calculate the big O expansion of the function automatically

Patrick Massot (Oct 25 2020 at 20:45):

As far as I know, the current state of the art is still https://www21.in.tum.de/~eberlm/pubs/real_asymp.html

Patrick Massot (Oct 25 2020 at 20:46):

It's not in Lean but in another proof assistant called Isabelle. One day we'll have it, but this is non-trivial work.

Heather Macbeth (Oct 25 2020 at 22:26):

Another way of gluing together the existing lemmas in the library to get this: docs#tendsto_at_top_mul_left plus docs#filter.tendsto_id

Last updated: May 17 2021 at 14:12 UTC