tendsto_stirlingSeq_sqrt_pi — Mathlib

English

The Stirling sequence converges to sqrt(pi).

Русский

Последовательность Стирлинга сходится к sqrt(pi).

LaTeX

$$$$ \operatorname{Tendsto}(\mathrm{stirlingSeq})_{atTop} (\mathcal{N}(\sqrt{\pi})). $$$$

Lean4

/-- **Stirling's Formula** -/
theorem tendsto_stirlingSeq_sqrt_pi : Tendsto stirlingSeq atTop (𝓝 (√π)) :=
  by
  obtain ⟨a, hapos, halimit⟩ := stirlingSeq_has_pos_limit_a
  have hπ : π / 2 = a ^ 2 / 2 :=
    tendsto_nhds_unique Wallis.tendsto_W_nhds_pi_div_two (second_wallis_limit a hapos.ne' halimit)
  rwa [(div_left_inj' (two_ne_zero' ℝ)).mp hπ, sqrt_sq hapos.le]

Похожие утверждения