Asymptotics of ζ s as s → 1

The goal of this file is to evaluate the limit of ζ s - 1 / (s - 1) as s → 1.

Main results

• tendsto_riemannZeta_sub_one_div: the limit of ζ s - 1 / (s - 1), at the filter of punctured neighbourhoods of 1 in ℂ, exists and is equal to the Euler-Mascheroni constant γ.
• riemannZeta_one_ne_zero: with our definition of ζ 1 (which is characterised as the limit of ζ s - 1 / (s - 1) / Gammaℝ s as s → 1), we have ζ 1 ≠ 0.

Outline of arguments

We consider the sum F s = ∑' n : ℕ, f (n + 1) s, where s is a real variable and f n s = ∫ x in n..(n + 1), (x - n) / x ^ (s + 1). We show that F s is continuous on [1, ∞), that F 1 = 1 - γ, and that F s = 1 / (s - 1) - ζ s / s for 1 < s.

By combining these formulae, one deduces that the limit of ζ s - 1 / (s - 1) at 𝓝[>] (1 : ℝ) exists and is equal to γ. Finally, using this and the Riemann removable singularity criterion we obtain the limit along punctured neighbourhoods of 1 in ℂ.

Definitions

noncomputable def ZetaAsymptotics.term (n : ℕ) (s : ℝ) : ℝ

Auxiliary function used in studying zeta-function asymptotics.

noncomputable def ZetaAsymptotics.term_sum (s : ℝ) (N : ℕ) : ℝ

Sum of finitely many terms.

noncomputable def ZetaAsymptotics.term_tsum (s : ℝ) : ℝ

Topological sum of terms.

theorem ZetaAsymptotics.term_nonneg (n : ℕ) (s : ℝ) : 0 ≤ term n s

theorem ZetaAsymptotics.term_welldef {n : ℕ} (hn : 0 < n) {s : ℝ} (hs : 0 < s) : IntervalIntegrable (fun (x : ℝ) => (x - ↑n) / x ^ (s + 1)) MeasureTheory.volume (↑n) (↑n + 1)

Evaluation of the sum for s = 1

theorem ZetaAsymptotics.term_one {n : ℕ} (hn : 0 < n) : term n 1 = Real.log (↑n + 1) - Real.log ↑n - 1 / (↑n + 1)

theorem ZetaAsymptotics.term_sum_one (N : ℕ) : term_sum 1 N = Real.log (↑N + 1) - ↑(harmonic (N + 1)) + 1

theorem ZetaAsymptotics.term_tsum_one : HasSum (fun (n : ℕ) => term (n + 1) 1) (1 - Real.eulerMascheroniConstant)

The topological sum of ZetaAsymptotics.term (n + 1) 1 over all n : ℕ is 1 - γ. This is proved by directly evaluating the sum of the first N terms and using the limit definition of γ.

Evaluation of the sum for 1 < s

theorem ZetaAsymptotics.term_of_lt {n : ℕ} (hn : 0 < n) {s : ℝ} (hs : 1 < s) : term n s = 1 / (s - 1) * (1 / ↑n ^ (s - 1) - 1 / (↑n + 1) ^ (s - 1)) - ↑n / s * (1 / ↑n ^ s - 1 / (↑n + 1) ^ s)

theorem ZetaAsymptotics.term_sum_of_lt (N : ℕ) {s : ℝ} (hs : 1 < s) : term_sum s N = 1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

theorem ZetaAsymptotics.term_tsum_of_lt {s : ℝ} (hs : 1 < s) : term_tsum s = 1 / (s - 1) - 1 / s * ∑' (n : ℕ), 1 / (↑n + 1) ^ s

For 1 < s, the topological sum of ZetaAsymptotics.term (n + 1) s over all n : ℕ is 1 / (s - 1) - ζ s / s.

theorem ZetaAsymptotics.zeta_limit_aux1 {s : ℝ} (hs : 1 < s) : ∑' (n : ℕ), 1 / (↑n + 1) ^ s - 1 / (s - 1) = 1 - s * term_tsum s

Reformulation of ZetaAsymptotics.term_tsum_of_lt which is useful for some computations below.

Continuity of the sum

theorem ZetaAsymptotics.continuousOn_term (n : ℕ) : ContinuousOn (fun (x : ℝ) => term (n + 1) x) (Set.Ici 1)

theorem ZetaAsymptotics.continuousOn_term_tsum : ContinuousOn term_tsum (Set.Ici 1)

theorem ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_nhds_right : Filter.Tendsto (fun (s : ℝ) => riemannZeta ↑s - 1 / (↑s - 1)) (nhdsWithin 1 (Set.Ioi 1)) (nhds ↑Real.eulerMascheroniConstant)

First version of the limit formula, with a limit over real numbers tending to 1 from above.

theorem tendsto_riemannZeta_sub_one_div : Filter.Tendsto (fun (s : ℂ) => riemannZeta s - 1 / (s - 1)) (nhdsWithin 1 {1}ᶜ) (nhds ↑Real.eulerMascheroniConstant)

The function ζ s - 1 / (s - 1) tends to γ as s → 1.

theorem isBigO_riemannZeta_sub_one_div {F : Type u_1} [Norm F] [One F] [NormOneClass F] : (fun (s : ℂ) => riemannZeta s - 1 / (s - 1)) =O[nhds 1] fun (x : ℂ) => 1

theorem ZetaAsymptotics.tendsto_Gamma_term_aux : Filter.Tendsto (fun (s : ℂ) => 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (nhdsWithin 1 {1}ᶜ) (nhds (-(↑Real.eulerMascheroniConstant + Complex.log (4 * ↑Real.pi)) / 2))

theorem ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_Gammaℝ : Filter.Tendsto (fun (s : ℂ) => riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (nhdsWithin 1 {1}ᶜ) (nhds ((↑Real.eulerMascheroniConstant - Complex.log (4 * ↑Real.pi)) / 2))

theorem riemannZeta_one : riemannZeta 1 = (↑Real.eulerMascheroniConstant - Complex.log (4 * ↑Real.pi)) / 2

Formula for ζ 1. Note that mathematically ζ 1 is undefined, but our construction ascribes this particular value to it.

theorem completedRiemannZeta_one : completedRiemannZeta 1 = (↑Real.eulerMascheroniConstant - Complex.log (4 * ↑Real.pi)) / 2

Formula for Λ 1. Note that mathematically Λ 1 is undefined, but our construction ascribes this particular value to it.

theorem completedRiemannZeta₀_one : completedRiemannZeta₀ 1 = (↑Real.eulerMascheroniConstant - Complex.log (4 * ↑Real.pi)) / 2 + 1

Formula for Λ₀ 1, where Λ₀ is the entire function satisfying Λ₀ s = π ^ (-s / 2) Γ(s / 2) ζ(s) + 1 / s + 1 / (1 - s) away from s = 0, 1.

Note that s = 1 is not a pole of Λ₀, so this statement (unlike riemannZeta_one) is a mathematically meaningful statement and is not dependent on Mathlib's particular conventions for division by zero.

theorem riemannZeta_one_ne_zero : riemannZeta 1 ≠ 0

With Mathlib's particular conventions, we have ζ 1 ≠ 0.