Commit 2024-06-04 08:01 ab939c0c

View on Github →

feat(NumberTheory/Harmonic): explicit formula for ζ 1 (#13434) Mathematically Riemann zeta is not defined at 1, but our construction ascribes a value to ζ 1. This PR calculates the value, and shows that it is not zero.

Estimated changes

Modified Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean

added theorem ZetaAsymptotics.tendsto_Gamma_term_aux

added theorem ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_Gammaℝ

modified theorem ZetaAsymptotics.term_tsum_one

added theorem completedRiemannZeta_one

added theorem completedRiemannZeta₀_one

added theorem riemannZeta_one

added theorem riemannZeta_one_ne_zero