log_stirlingSeq_bounded_by_constant

English

There exists a constant c such that for all n ≥ 0, log(stirlingSeq(n+1)) ≥ c.

Русский

Существует константа c такая, что для всех n ≥ 0 выполняется log(stirlingSeq(n+1)) ≥ c.

LaTeX

$$$\\exists c\\in\\mathbb{R},\\quad \\forall n\\in\\mathbb{N},\\quad c \\le \\log\\big(\\operatorname{stirlingSeq}(n+1)\\big)$$$

Lean4

/-- The sequence `log_stirlingSeq` is bounded below for `n ≥ 1`. -/
theorem log_stirlingSeq_bounded_by_constant : ∃ c, ∀ n : ℕ, c ≤ log (stirlingSeq (n + 1)) :=
  by
  obtain ⟨d, h⟩ := log_stirlingSeq_bounded_aux
  exact ⟨log (stirlingSeq 1) - d, fun n => sub_le_comm.mp (h n)⟩

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