Euler–Mascheroni Constant as an Infinite Sum

This file proves that the Euler–Mascheroni constant can be expressed as the infinite sum

∑' n, (1 / (n + 1) - log ((n + 2) / (n + 1))).

We conclude that the series sums to Real.eulerMascheroniConstant.

noncomputable def EulerMascheroniInfiniteSum.eulerMascheroni_sum_inner (n : ℕ) : ℝ

Inner sum of the infinite sum definition

Equations

• EulerMascheroniInfiniteSum.eulerMascheroni_sum_inner n = 1 / (↑n + 1) - Real.log ((↑n + 2) / (↑n + 1))

theorem EulerMascheroniInfiniteSum.eulerMascheroni_sum_inner_nonneg (n : ℕ) : 0 ≤ eulerMascheroni_sum_inner n

theorem EulerMascheroniInfiniteSum.eulerMascheroni_sum_partial (N : ℕ) : ∑ k ∈ Finset.range N, eulerMascheroni_sum_inner k = ↑(harmonic N) - Real.log (↑N + 1)

theorem EulerMascheroniInfiniteSum.eulerMascheroni_sum_bound (N : ℕ) : ∑ k ∈ Finset.range N, eulerMascheroni_sum_inner k ≤ 1

theorem EulerMascheroniInfiniteSum.eulerMascheroni_tsum : ∑' (n : ℕ), eulerMascheroni_sum_inner n = Real.eulerMascheroniConstant

the infinite sum is equal to Real.eulerMascheroniConstant