stirlingSeq_has_pos_limit_a — Mathlib

English

The sequence stirlingSeq has a positive limit a as n → ∞.

Русский

Предел последовательности stirlingSeq существует и положителен: a > 0, a = lim_{n→∞} stirlingSeq(n).

LaTeX

$$$$ \exists a \in \mathbb{R}, a>0 \land \operatorname{Tendsto}(\mathrm{stirlingSeq})_{atTop} (\mathcal{N}(a)). $$$$

Lean4

/-- The limit `a` of the sequence `stirlingSeq` satisfies `0 < a` -/
theorem stirlingSeq_has_pos_limit_a : ∃ a : ℝ, 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a) :=
  by
  obtain ⟨x, x_pos, hx⟩ := stirlingSeq'_bounded_by_pos_constant
  have hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ)) := by simpa [lowerBounds] using hx
  refine ⟨_, lt_of_lt_of_le x_pos (le_csInf (Set.range_nonempty _) hx'), ?_⟩
  rw [← Filter.tendsto_add_atTop_iff_nat 1]
  exact tendsto_atTop_ciInf stirlingSeq'_antitone ⟨x, hx'⟩

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