English
For any m ∈ N, the series sum over k ≥ 0 of [ 1/(2(k+1)+1) * ((1/(2(m+1)+1))^2)^(k+1) ] converges to log(stirlingSeq(m+1)) − log(stirlingSeq(m+2)).
Русский
Для любого m ∈ N ряд сумма по k ≥ 0: \\sum_{k≥0} 1/(2(k+1)+1) * ((1/(2(m+1)+1))^2)^{(k+1)} сходится к log(stirlingSeq(m+1)) − log(stirlingSeq(m+2)).
LaTeX
$$$\\sum_{k=0}^{\\infty} \\frac{1}{2(k+1)+1} \\left( \\frac{1}{2(m+1)+1} \\right)^{2(k+1)} = \\log\\left(\\operatorname{stirlingSeq}(m+1)\\right) - \\log\\left(\\operatorname{stirlingSeq}(m+2)\\right)$$$
Lean4
/-- The sequence `log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2))` has the series expansion
`∑ 1 / (2 * (k + 1) + 1) * (1 / 2 * (m + 1) + 1)^(2 * (k + 1))`. -/
theorem log_stirlingSeq_diff_hasSum (m : ℕ) :
HasSum (fun k : ℕ => (1 : ℝ) / (2 * ↑(k + 1) + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ ↑(k + 1))
(log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2))) :=
by
let f (k : ℕ) := (1 : ℝ) / (2 * k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
change HasSum (fun k => f (k + 1)) _
rw [hasSum_nat_add_iff]
convert (hasSum_log_one_add_inv m.cast_add_one_pos).mul_left ((↑(m + 1) : ℝ) + 1 / 2) using 1
· ext k
dsimp only [f]
rw [← pow_mul, pow_add]
push_cast
field_simp
· have h (x) (hx : x ≠ (0 : ℝ)) : 1 + x⁻¹ = (x + 1) / x := by field_simp
simp (disch := positivity) only [log_stirlingSeq_formula, log_div, log_mul, log_exp, factorial_succ, cast_mul,
cast_succ, range_one, sum_singleton, h]
ring
