## Stream: Is there code for X?

### Topic: Eventually monotone sequences converge

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

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

#### 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

#### Kevin Buzzard (Apr 05 2021 at 22:17):

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

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

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

#### 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