log_stirlingSeq_sub_log_stirlingSeq_succ

English

For every n, log(stirlingSeq(n+1)) − log(stirlingSeq(n+2)) ≤ 1 / (4 (n+1)^2).

Русский

Для каждого n выполняется log(stirlingSeq(n+1)) − log(stirlingSeq(n+2)) ≤ 1 / (4 (n+1)^2).

LaTeX

$$$\\log\\big(\\operatorname{stirlingSeq}(n+1)\\big) - \\log\\big(\\operatorname{stirlingSeq}(n+2)\\big) \\le \\dfrac{1}{4 \\,(n+1)^2}$$$

Lean4

/-- We have the bound `log (stirlingSeq n) - log (stirlingSeq (n+1))` ≤ 1/(4 n^2)
-/
theorem log_stirlingSeq_sub_log_stirlingSeq_succ (n : ℕ) :
    log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 2)) ≤ 1 / (4 * (↑(n + 1) : ℝ) ^ 2) :=
  by
  have h₁ : (0 : ℝ) < ((n : ℝ) + 1) ^ 2 * 4 := by positivity
  have h₃ : (0 : ℝ) < (2 * ((n : ℝ) + 1) + 1) ^ 2 - 1 := by
    ring_nf
    positivity
  refine (log_stirlingSeq_diff_le_geo_sum n).trans ?_
  push_cast
  field_simp
  ring_nf
  norm_cast
  cutsat

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