Computing limit as x approaches some number or infinity

Stream: Is there code for X?

[Formally Verified Waffle Maker]

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

[Bryan Gin-ge Chen]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Mario Carneiro]

that's certainly doable with some elbow grease

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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

[Patrick Massot]

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]

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]

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