Documentation

Mathlib.NumberTheory.Harmonic.ZetaAsymp

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 #

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
Instances For
    noncomputable def ZetaAsymptotics.term_sum (s : ) (N : ) :

    Sum of finitely many terms.

    Equations
    Instances For
      noncomputable def ZetaAsymptotics.term_tsum (s : ) :

      Topological sum of terms.

      Equations
      Instances For
        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)

        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 * (nFinset.range 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 #

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

        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))

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

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

        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.

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