Limits in the stdlib

Stream: general

[Donald Sebastian Leung]

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]

analysis/specific_limits.lean is the place to look

[Scott Morrison]

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

[Yury G. Kudryashov]

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

[Donald Sebastian Leung]

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]

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]

I think all 3 are good exercises!

[Donald Sebastian Leung]

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]

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

[Scott Morrison]

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.