let's try to reproduce arXiv:math/0211148 and arXiv:math/0508042

Goal (arXiv:math/0211148):

• Definition of the sequence in terms of harmonic and natural log
• Definition of γ from sequence at infinite
• Proof of γ in terms of infinite sum
• natural log of 4/π in terms of "alternating" sequence
• Proof that γ = ln 4/π

noncomputable def eulerMascheroniSeq (n : ℕ) : ℝ

definition of the sequence in terms of harmonic

Equations

• eulerMascheroniSeq n = ↑(harmonic n) - Real.log ↑n

theorem eulerMascheroniSeq_one : eulerMascheroniSeq 1 = 1

noncomputable def γ : ℝ

definition of the Euler's constant

Equations

• γ = limUnder Filter.atTop eulerMascheroniSeq

noncomputable def eulerMascheroniSeq' (n : ℕ) : ℝ

Equations

• eulerMascheroniSeq' n = (-1) ^ (n - 1) * eulerMascheroniSeq n

noncomputable def γ' (n : ℕ) : ℝ

definition of the inner of infinite sum

Equations

• γ' n = 1 / ↑n - Real.log ((↑n + 1) / ↑n)

noncomputable def ln4OverPiSeq (n : ℕ) : ℝ

definition of the "alternating" sequence

Equations

• ln4OverPiSeq n = (-1) ^ (n - 1) * γ' n

theorem ln_4_over_pi : Real.log (Real.pi / 4) = ∑' (n : ℕ), ln4OverPiSeq n

theorem γ_eq_sum : γ = ∑' (n : ℕ), γ' n