Zulip Chat Archive

Stream: general

Topic: Limits in the stdlib


Donald Sebastian Leung (Feb 21 2020 at 02:29):

Which, if any, of these results on limits are already available in the standard library?

  • 0.99 ... 9 = 1
  • The nth root of n converges to 1 as n approaches infinity
  • For p > 0, 1 / n^p converges to 0 as n approaches infinity

Scott Morrison (Feb 21 2020 at 02:34):

analysis/specific_limits.lean is the place to look

Scott Morrison (Feb 21 2020 at 02:36):

But I only see stuff about geometric sums there, so your second two questions aren't answered.

Yury G. Kudryashov (Feb 21 2020 at 02:40):

The last one easily follows from 1/n tends to zero and continuity of rpow, both facts are in the library

Donald Sebastian Leung (Feb 21 2020 at 02:42):

Thanks for the pointer and replies, I was trying to determine whether they would be suitable as beginner-level exercises on an online platform

So I suppose the last one is hardly an interesting exercise even for a beginner?

Scott Morrison (Feb 21 2020 at 02:43):

The second one I guess you want log n / n tends to zero. I'm not sure if that's in the library.

Scott Morrison (Feb 21 2020 at 02:43):

I think all 3 are good exercises!

Donald Sebastian Leung (Feb 21 2020 at 02:45):

Thanks for the encouragement, I will make a note to author these exercises then, once I get better with Lean :smile: It would also be interesting to see solvers familiar with the stdlib solving it in like one to two lines

Scott Morrison (Feb 21 2020 at 02:45):

There only appears to be one appearance of the regex tendsto.*log in mathlib, proving log goes to 0 near 1.

Scott Morrison (Feb 21 2020 at 02:53):

Ah, but we do have lemma tendsto_pow_mul_exp_neg_at_top_nhds_0 (n : ℕ) : tendsto (λx, x^n * exp (-x)) at_top (𝓝 0) := which should get you most of the way there.


Last updated: Dec 20 2023 at 11:08 UTC