sqrt_pi_le_stirlingSeq — Mathlib

English

For every positive n, sqrt(pi) ≤ stirlingSeq(n).

Русский

Для каждого положительного n выполняется sqrt(pi) ≤ stirlingSeq(n).

LaTeX

$$$$ \forall n\in\mathbb{N},\ n\neq 0 \Rightarrow \sqrt{\pi} \le \mathrm{stirlingSeq}(n). $$$$

Lean4

/-- The Stirling sequence is bounded below by `√π`, for all positive naturals. Note that this bound
holds for all `n > 0`, rather than for sufficiently large `n`: it is effective.
-/
theorem sqrt_pi_le_stirlingSeq {n : ℕ} (hn : n ≠ 0) : √π ≤ stirlingSeq n :=
  match n, hn with
  | n + 1, _ =>
    stirlingSeq'_antitone.le_of_tendsto (b := n) <| tendsto_stirlingSeq_sqrt_pi.comp (tendsto_add_atTop_nat 1)

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