Documentation

Mathlib.NumberTheory.LSeries.Convergence

Convergence of L-series #

We define LSeries.abscissaOfAbsConv f (as an EReal) to be the infimum of all real numbers x such that the L-series of f converges for complex arguments with real part x and provide some results about it.

Tags #

L-series, abscissa of convergence

noncomputable def LSeries.abscissaOfAbsConv (f : ) :

The abscissa x : EReal of absolute convergence of the L-series associated to f: the series converges absolutely at s when re s > x and does not converge absolutely when re s < x.

Equations
Instances For
    theorem LSeries.abscissaOfAbsConv_congr {f : } {g : } (h : ∀ {n : }, n 0f n = g n) :

    If f and g agree on large n : ℕ, then their LSeries have the same abscissa of absolute convergence.

    theorem LSeries.abscissaOfAbsConv_le_of_le_const_mul_rpow {f : } {x : } (h : ∃ (C : ), ∀ (n : ), n 0f n C * n ^ x) :

    If ‖f n‖ is bounded by a constant times n^x, then the abscissa of absolute convergence of f is bounded by x + 1.

    theorem LSeries.abscissaOfAbsConv_le_of_isBigO_rpow {f : } {x : } (h : f =O[Filter.atTop] fun (n : ) => n ^ x) :

    If ‖f n‖ is O(n^x), then the abscissa of absolute convergence of f is bounded by x + 1.

    theorem LSeries.abscissaOfAbsConv_le_of_le_const {f : } (h : ∃ (C : ), ∀ (n : ), n 0f n C) :

    If f is bounded, then the abscissa of absolute convergence of f is bounded above by 1.

    If f is O(1), then the abscissa of absolute convergence of f is bounded above by 1.