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

source
noncomputable def LSeries.abscissaOfAbsConv (f : ℕ → ℂ) :
EReal

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
    source
    theorem LSeries.abscissaOfAbsConv_congr {f g : ℕ → ℂ} (h : ∀ {n : ℕ}, n ≠ 0 → f n = g n) :
    LSeries.abscissaOfAbsConv f = LSeries.abscissaOfAbsConv g
    source
    theorem LSeries.abscissaOfAbsConv_congr' {f g : ℕ → ℂ} (h : f =ᶠ[Filter.atTop] g) :
    LSeries.abscissaOfAbsConv f = LSeries.abscissaOfAbsConv g

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

    source
    theorem LSeriesSummable_of_abscissaOfAbsConv_lt_re {f : ℕ → ℂ} {s : ℂ} (hs : LSeries.abscissaOfAbsConv f < ↑s.re) :
    LSeriesSummable f s
    source
    theorem LSeriesSummable_lt_re_of_abscissaOfAbsConv_lt_re {f : ℕ → ℂ} {s : ℂ} (hs : LSeries.abscissaOfAbsConv f < ↑s.re) :
    ∃ x < s.re, LSeriesSummable f ↑x
    source
    theorem LSeriesSummable.abscissaOfAbsConv_le {f : ℕ → ℂ} {s : ℂ} (h : LSeriesSummable f s) :
    LSeries.abscissaOfAbsConv f ≤ ↑s.re
    source
    theorem LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable {f : ℕ → ℂ} {x : ℝ} (h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y) :
    LSeries.abscissaOfAbsConv f ≤ ↑x
    source
    theorem LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' {f : ℕ → ℂ} {x : EReal} (h : ∀ (y : ℝ), x < ↑y → LSeriesSummable f ↑y) :
    LSeries.abscissaOfAbsConv f ≤ x
    source
    theorem LSeries.abscissaOfAbsConv_le_of_le_const_mul_rpow {f : ℕ → ℂ} {x : ℝ} (h : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ x) :
    LSeries.abscissaOfAbsConv f ≤ ↑x + 1

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

    source
    theorem LSeries.abscissaOfAbsConv_le_of_isBigO_rpow {f : ℕ → ℂ} {x : ℝ} (h : f =O[Filter.atTop] fun (n : ℕ) => ↑n ^ x) :
    LSeries.abscissaOfAbsConv f ≤ ↑x + 1

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

    source
    theorem LSeries.abscissaOfAbsConv_le_of_le_const {f : ℕ → ℂ} (h : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C) :
    LSeries.abscissaOfAbsConv f ≤ 1

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

    source
    theorem LSeries.abscissaOfAbsConv_le_one_of_isBigO_one {f : ℕ → ℂ} (h : f =O[Filter.atTop] 1) :
    LSeries.abscissaOfAbsConv f ≤ 1

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

    source
    theorem LSeries.summable_real_of_abscissaOfAbsConv_lt {f : ℕ → ℝ} {x : ℝ} (h : (LSeries.abscissaOfAbsConv fun (x : ℕ) => ↑(f x)) < ↑x) :
    Summable fun (n : ℕ) => f n / ↑n ^ x

    If f is real-valued and x is strictly greater than the abscissa of absolute convergence of f, then the real series ∑' n, f n / n ^ x converges.