Eventually monotone sequences converge

Stream: Is there code for X?

[Hanting Zhang]

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.)

[Kevin Buzzard]

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.

[Hanting Zhang]

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

[Kevin Buzzard]

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

[Hanting Zhang]

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.

[Kevin Buzzard]

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.

[Hanting Zhang]

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