Zulip Chat Archive

Stream: Is there code for X?

Topic: Computing limit as x approaches some number or infinity


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Oct 25 2020 at 20:34):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Formally Verified Waffle Maker (Oct 25 2020 at 20:38):

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

view this post on Zulip Mario Carneiro (Oct 25 2020 at 20:39):

that's certainly doable with some elbow grease

view this post on Zulip Mario Carneiro (Oct 25 2020 at 20:39):

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

view this post on Zulip 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

view this post on Zulip 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 limx2x\displaystyle\lim_{x\to\infty} 2x into Lean and get ∞ out.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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