English
There exists a constant c such that for all n ∈ N, log(stirlingSeq(1)) − log(stirlingSeq(n+1)) ≤ c.
Русский
Существует константа c, такая что для всех n ∈ N выполняется log(stirlingSeq(1)) − log(stirlingSeq(n+1)) ≤ c.
LaTeX
$$$\\exists c\\in\\mathbb{R}\\; \\forall n\\in\\mathbb{N},\\quad \\log\\big(\\operatorname{stirlingSeq}(1)\\big) - \\log\\big(\\operatorname{stirlingSeq}(n+1)\\big) \\le c$$$
Lean4
/-- For any `n`, we have `log_stirlingSeq 1 - log_stirlingSeq n ≤ 1/4 * ∑' 1/k^2` -/
theorem log_stirlingSeq_bounded_aux : ∃ c : ℝ, ∀ n : ℕ, log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ c :=
by
let d : ℝ := ∑' k : ℕ, (1 : ℝ) / (↑(k + 1) : ℝ) ^ 2
use 1 / 4 * d
let log_stirlingSeq' : ℕ → ℝ := fun k => log (stirlingSeq (k + 1))
intro n
have h₁ k : log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / (↑(k + 1) : ℝ) ^ 2) := by
convert log_stirlingSeq_sub_log_stirlingSeq_succ k using 1; field_simp
have h₂ : (∑ k ∈ range n, 1 / (↑(k + 1) : ℝ) ^ 2) ≤ d :=
by
have := (summable_nat_add_iff 1).mpr <| Real.summable_one_div_nat_pow.mpr one_lt_two
exact this.sum_le_tsum (range n) (fun k _ => by positivity)
calc
log (stirlingSeq 1) - log (stirlingSeq (n + 1)) = log_stirlingSeq' 0 - log_stirlingSeq' n := rfl
_ = ∑ k ∈ range n, (log_stirlingSeq' k - log_stirlingSeq' (k + 1)) := by rw [← sum_range_sub' log_stirlingSeq' n]
_ ≤ ∑ k ∈ range n, 1 / 4 * (1 / ↑((k + 1)) ^ 2) := (sum_le_sum fun k _ => h₁ k)
_ = 1 / 4 * ∑ k ∈ range n, 1 / ↑((k + 1)) ^ 2 := by rw [mul_sum]
_ ≤ 1 / 4 * d := by gcongr
