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