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) :
      abscissaOfAbsConv f = abscissaOfAbsConv g
      source
      theorem LSeries.abscissaOfAbsConv_congr' {f g : ℕ → ℂ} (h : f =ᶠ[Filter.atTop] g) :
      abscissaOfAbsConv f = 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) :
      abscissaOfAbsConv f ≤ ↑x
      source
      theorem LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' {f : ℕ → ℂ} {x : EReal} (h : ∀ (y : ℝ), x < ↑y → LSeriesSummable f ↑y) :
      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) :
      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) :
      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) :
      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] fun (x : ℕ) => 1) :
      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 : (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.

      source
      theorem LSeries.abscissaOfAbsConv_binop_le {F : (ℕ → ℂ) → (ℕ → ℂ) → ℕ → ℂ} (hF : ∀ {f g : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeriesSummable g s → LSeriesSummable (F f g) s) (f g : ℕ → ℂ) :
      abscissaOfAbsConv (F f g) ≤ max (abscissaOfAbsConv f) (abscissaOfAbsConv g)

      If F is a binary operation on ℕ → ℂ with the property that the LSeries of F f g converges whenever the LSeries of f and g do, then the abscissa of absolute convergence of F f g is at most the maximum of the abscissa of absolute convergence of f and that of g.