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) : abscissaOfAbsConv f = abscissaOfAbsConv g

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.

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) : abscissaOfAbsConv f ≤ ↑x

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

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.

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.

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.

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.

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.

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.