Zulip Chat Archive

Stream: Is there code for X?

Topic: Eventually monotone sequences converge


view this post on Zulip Hanting Zhang (Apr 05 2021 at 21:53):

This is a bit infuriating:

import analysis.special_functions.integrals
import analysis.asymptotics.asymptotics

noncomputable theory
open filter asymptotics finset
open_locale nat big_operators real asymptotics

namespace real

example :  (c : ), tendsto (λ n, (n!:) / (n ^ (n:) * sqrt n * exp (-n))) at_top (nhds c) :=
begin
  refine (tendsto_of_monotone _).resolve_left _,
  -- This doesn't work because the function isn't completely monotone on ℕ.
  { sorry },
  sorry
end

end real

Are there any lemmas which assert convergence but don't go as far to require exactly where a sequence converges? I would expect these kinds of lemmas to be named like exists_tendsto, but I can't find any. (In this case c is equal to sqrt 2 * \pi, but I can't prove it directly.)

view this post on Zulip Kevin Buzzard (Apr 05 2021 at 22:00):

What's your maths proof that this sequence converges? Lean doesn't do magic. This is equivalent to some weak form of Stirling's formula.

view this post on Zulip Hanting Zhang (Apr 05 2021 at 22:13):

Take the log of the sequence and set d_n = log n! - (n + 1/2 ) * log n + n. Then you bound d_n - d_{n + 1} by 1 / 12 n by truncating its taylor series. So d_n is decreasing but d_n - 1 / 12 n is increasing; hence it must converge to some c.

I'm basically following http://faculty.washington.edu/moishe/hanoiex/counting/Stirling.pdf

view this post on Zulip Kevin Buzzard (Apr 05 2021 at 22:17):

So then that's the proof that you have to formalise. What's your question exactly?

view this post on Zulip Hanting Zhang (Apr 05 2021 at 22:33):

I wanted to ask because I feel like some helpful results about convergence should have already been formalized. And on second thought, I'm kind of just stuck on how to write out the details in Lean... I guess that isn't really a question.

view this post on Zulip Kevin Buzzard (Apr 05 2021 at 22:37):

I think you might be better off starting to formalise the proof and then coming up with a precise question. Things like "a decreasing bounded-below sequence tends to a limit" are going to be in there somewhere but you have a journey to go on before that result is useful to you.

view this post on Zulip Hanting Zhang (Apr 05 2021 at 22:42):

Ok, thanks. I'll probably have real questions after I iron out the details. Back to coding I go. :upside_down:


Last updated: May 19 2021 at 02:10 UTC