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 γ.

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.

Equations

• ZetaAsymptotics.term n s = ∫ (x : ℝ) in ↑n..↑n + 1, (x - ↑n) / x ^ (s + 1)

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

Sum of finitely many terms.

Equations

• ZetaAsymptotics.term_sum s N = Finset.sum (Finset.range N) fun (n : ℕ) => ZetaAsymptotics.term (n + 1) s

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

Topological sum of terms.

Equations

• ZetaAsymptotics.term_tsum s = ∑' (n : ℕ), ZetaAsymptotics.term (n + 1) s

theorem ZetaAsymptotics.term_nonneg (n : ℕ) (s : ℝ) : 0 ≤ ZetaAsymptotics.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) : ZetaAsymptotics.term n 1 = Real.log (↑n + 1) - Real.log ↑n - 1 / (↑n + 1)

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

theorem ZetaAsymptotics.term_tsum_one : HasSum (fun (n : ℕ) => ZetaAsymptotics.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) : ZetaAsymptotics.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) : ZetaAsymptotics.term_sum s N = 1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * ((Finset.sum (Finset.range N) fun (n : ℕ) => 1 / (↑n + 1) ^ s) - ↑N / (↑N + 1) ^ s)

theorem ZetaAsymptotics.term_tsum_of_lt {s : ℝ} (hs : 1 < s) : ZetaAsymptotics.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 * ZetaAsymptotics.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 : ℝ) => ZetaAsymptotics.term (n + 1) x) (Set.Ici 1)

theorem ZetaAsymptotics.continuousOn_term_tsum : ContinuousOn ZetaAsymptotics.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