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 : ℕ → ℂ) : 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

• LSeries.abscissaOfAbsConv f = sInf (Real.toEReal '' {x : ℝ | LSeriesSummable f ↑x})

theorem LSeries.abscissaOfAbsConv_congr {f : ℕ → ℂ} {g : ℕ → ℂ} (h : ∀ {n : ℕ}, n ≠ 0 → f n = g n) : LSeries.abscissaOfAbsConv f = LSeries.abscissaOfAbsConv g

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.

theorem LSeriesSummable_of_abscissaOfAbsConv_lt_re {f : ℕ → ℂ} {s : ℂ} (hs : LSeries.abscissaOfAbsConv f < ↑s.re) : LSeriesSummable f s

theorem LSeriesSummable_lt_re_of_abscissaOfAbsConv_lt_re {f : ℕ → ℂ} {s : ℂ} (hs : LSeries.abscissaOfAbsConv f < ↑s.re) : ∃ x < s.re, LSeriesSummable f ↑x

theorem LSeriesSummable.abscissaOfAbsConv_le {f : ℕ → ℂ} {s : ℂ} (h : LSeriesSummable f s) : LSeries.abscissaOfAbsConv f ≤ ↑s.re

theorem LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable {f : ℕ → ℂ} {x : ℝ} (h : ∀ (y : ℝ), x < y → LSeriesSummable f ↑y) : LSeries.abscissaOfAbsConv f ≤ ↑x

theorem LSeries.abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable' {f : ℕ → ℂ} {x : EReal} (h : ∀ (y : ℝ), x < ↑y → LSeriesSummable f ↑y) : LSeries.abscissaOfAbsConv f ≤ x

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.

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.

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.

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.