Source indexedlemma · leanprover/lean4:v4.32.0

euler_maclaurin_tendsto

PrimeNumberTheoremAnd.EulerMascheroniBounds · PrimeNumberTheoremAnd/EulerMascheroniBounds.lean:199 to 207

Source documentation

γ₂ converges to γ.

Exact Lean statement

lemma euler_maclaurin_tendsto :
    Filter.Tendsto γ₂ Filter.atTop (nhds Real.eulerMascheroniConstant)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma euler_maclaurin_tendsto :    Filter.Tendsto γ₂ Filter.atTop (nhds Real.eulerMascheroniConstant) := by  unfold γ₂  have h : Filter.Tendsto (fun n => (harmonic n : ℝ) - Real.log n - 1 / (2 * n))      Filter.atTop (nhds eulerMascheroniConstant) := by    simpa using Filter.Tendsto.sub Real.tendsto_harmonic_sub_log      (tendsto_inv_atTop_nhds_zero_nat.mul tendsto_const_nhds) |>.congr'      (by filter_upwards [Filter.eventually_ne_atTop 0] with n hn; aesop)  simpa using h.add (tendsto_inv_atTop_nhds_zero_nat.pow 2 |>.mul_const _)