English
For each n, the difference log(stirlingSeq(n+1)) − log(stirlingSeq(n+2)) is bounded above by a geometric-series expression: ≤ (1/(2(n+1)+1))^2 / (1 − (1/(2(n+1)+1))^2).
Русский
Для каждого n разность log(stirlingSeq(n+1)) − log(stirlingSeq(n+2)) ограничена сверху геометрической суммой: ≤ (1/(2(n+1)+1))^2 / (1 − (1/(2(n+1)+1))^2).
LaTeX
$$$\\log\\big(\\operatorname{stirlingSeq}(n+1)\\big) - \\log\\big(\\operatorname{stirlingSeq}(n+2)\\big) \\le \\dfrac{\\left(\\dfrac{1}{2(n+1)+1}\\right)^2}{1 - \\left(\\dfrac{1}{2(n+1)+1}\\right)^2}$$$
Lean4
/-- We have a bound for successive elements in the sequence `log (stirlingSeq k)`.
-/
theorem log_stirlingSeq_diff_le_geo_sum (n : ℕ) :
log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 2)) ≤
((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - ((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2) :=
by
have h_nonneg : (0 : ℝ) ≤ ((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2 := sq_nonneg _
have g :
HasSum (fun k : ℕ => (((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2) ^ ↑(k + 1))
(((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - ((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2)) :=
by
have := (hasSum_geometric_of_lt_one h_nonneg ?_).mul_left (((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2)
· simp_rw [← _root_.pow_succ'] at this
exact this
rw [one_div, inv_pow]
exact inv_lt_one_of_one_lt₀ (one_lt_pow₀ (lt_add_of_pos_left _ <| by positivity) two_ne_zero)
have hab (k : ℕ) :
(1 : ℝ) / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ ↑(k + 1) ≤
(((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2) ^ ↑(k + 1) :=
by
refine mul_le_of_le_one_left (pow_nonneg h_nonneg ↑(k + 1)) ?_
rw [one_div]
exact inv_le_one_of_one_le₀ (le_add_of_nonneg_left <| by positivity)
exact hasSum_le hab (log_stirlingSeq_diff_hasSum n) g
