stirlingSeq'_bounded_by_pos_constant

English

There exists a positive real a such that a ≤ stirlingSeq(n+1) for every natural number n.

Русский

Существет положительная константа a > 0 такая, что a ≤ stirlingSeq(n+1) для всех n ∈ ℕ.

LaTeX

$$$$ \exists a>0, \ \forall n\in\mathbb{N},\ a \le \operatorname{stirlingSeq}(n+1). $$$$

Lean4

/-- The sequence `stirlingSeq` has a positive lower bound.
-/
theorem stirlingSeq'_bounded_by_pos_constant : ∃ a, 0 < a ∧ ∀ n : ℕ, a ≤ stirlingSeq (n + 1) :=
  by
  obtain ⟨c, h⟩ := log_stirlingSeq_bounded_by_constant
  refine ⟨exp c, exp_pos _, fun n => ?_⟩
  rw [← le_log_iff_exp_le (stirlingSeq'_pos n)]
  exact h n

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