L-series

Given a sequence f: ℕ → ℂ, we define the corresponding L-series.

Main Definitions

• LSeries.term f s n is the nth term of the L-series of the sequence f at s : ℂ. We define it to be zero when n = 0.

• LSeries f is the L-series with a given sequence f as its coefficients. This is not the analytic continuation (which does not necessarily exist), just the sum of the infinite series if it exists and zero otherwise.

• LSeriesSummable f s indicates that the L-series of f converges at s : ℂ.

• LSeriesHasSum f s a expresses that the L-series of f converges (absolutely) at s : ℂ to a : ℂ.

Main Results

• LSeriesSummable_of_isBigO_rpow: the LSeries of a sequence f such that f = O(n^(x-1)) converges at s when x < s.re.

• LSeriesSummable.isBigO_rpow: if the LSeries of f is summable at s, then f = O(n^(re s)).

Notation

We introduce L as notation for LSeries and ↗f as notation for fun n : ℕ ↦ (f n : ℂ), both scoped to LSeries.notation. The latter makes it convenient to use arithmetic functions or Dirichlet characters (or anything that coerces to a function N → R, where ℕ coerces to N and R coerces to ℂ) as arguments to LSeries etc.

Tags

L-series

TODO

• Move LSeriesSummable.one_iff_one_lt_re and zeta_LSeriesSummable_iff_one_lt_r to a new file on L-series of specific functions

The terms of an L-series

We define the nth term evaluated at a complex number s of the L-series associated to a sequence f : ℕ → ℂ, LSeries.term f s n, and provide some basic API.

We set LSeries.term f s 0 = 0, and for positive n, LSeries.term f s n = f n / n ^ s.

noncomputable def LSeries.term (f : ℕ → ℂ) (s : ℂ) (n : ℕ) : ℂ

The nth term of the L-series of f evaluated at s. We set it to zero when n = 0.

Equations

• LSeries.term f s n = if n = 0 then 0 else f n / ↑n ^ s

theorem LSeries.term_def (f : ℕ → ℂ) (s : ℂ) (n : ℕ) : LSeries.term f s n = if n = 0 then 0 else f n / ↑n ^ s

@[simp]

theorem LSeries.term_zero (f : ℕ → ℂ) (s : ℂ) : LSeries.term f s 0 = 0

@[simp]

theorem LSeries.term_of_ne_zero {n : ℕ} (hn : n ≠ 0) (f : ℕ → ℂ) (s : ℂ) : LSeries.term f s n = f n / ↑n ^ s

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

theorem LSeries.norm_term_eq (f : ℕ → ℂ) (s : ℂ) (n : ℕ) : ‖LSeries.term f s n‖ = if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re

theorem LSeries.norm_term_le {f : ℕ → ℂ} {g : ℕ → ℂ} (s : ℂ) {n : ℕ} (h : ‖f n‖ ≤ ‖g n‖) : ‖LSeries.term f s n‖ ≤ ‖LSeries.term g s n‖

theorem LSeries.norm_term_le_of_re_le_re (f : ℕ → ℂ) {s : ℂ} {s' : ℂ} (h : s.re ≤ s'.re) (n : ℕ) : ‖LSeries.term f s' n‖ ≤ ‖LSeries.term f s n‖

Definition of the L-series and related statements

We define LSeries f s of f : ℕ → ℂ as the sum over LSeries.term f s. We also provide predicates LSeriesSummable f s stating that LSeries f s is summable and LSeriesHasSum f s a stating that the L-series of f is summable at s and converges to a : ℂ.

noncomputable def LSeries (f : ℕ → ℂ) (s : ℂ) : ℂ

The value of the L-series of the sequence f at the point s if it converges absolutely there, and 0 otherwise.

Equations

• LSeries f s = ∑' (n : ℕ), LSeries.term f s n

theorem LSeries_congr {f : ℕ → ℂ} {g : ℕ → ℂ} (s : ℂ) (h : ∀ (n : ℕ), n ≠ 0 → f n = g n) : LSeries f s = LSeries g s

def LSeriesSummable (f : ℕ → ℂ) (s : ℂ) : Prop

LSeriesSummable f s indicates that the L-series of f converges absolutely at s.

Equations

• LSeriesSummable f s = Summable (LSeries.term f s)

theorem LSeriesSummable_congr {f : ℕ → ℂ} {g : ℕ → ℂ} (s : ℂ) (h : ∀ (n : ℕ), n ≠ 0 → f n = g n) : LSeriesSummable f s ↔ LSeriesSummable g s

theorem LSeriesSummable.congr' {f : ℕ → ℂ} {g : ℕ → ℂ} (s : ℂ) (h : f =ᶠ[Filter.atTop] g) (hf : LSeriesSummable f s) : LSeriesSummable g s

If f and g agree on large n : ℕ and the LSeries of f converges at s, then so does that of g.

theorem LSeriesSummable_congr' {f : ℕ → ℂ} {g : ℕ → ℂ} (s : ℂ) (h : f =ᶠ[Filter.atTop] g) : LSeriesSummable f s ↔ LSeriesSummable g s

If f and g agree on large n : ℕ, then the LSeries of f converges at s if and only if that of g does.

theorem LSeries.eq_zero_of_not_LSeriesSummable (f : ℕ → ℂ) (s : ℂ) : ¬LSeriesSummable f s → LSeries f s = 0

@[simp]

theorem LSeriesSummable_zero {s : ℂ} : LSeriesSummable 0 s

def LSeriesHasSum (f : ℕ → ℂ) (s : ℂ) (a : ℂ) : Prop

This states that the L-series of the sequence f converges absolutely at s and that the value there is a.

Equations

• LSeriesHasSum f s a = HasSum (LSeries.term f s) a

theorem LSeriesHasSum.LSeriesSummable {f : ℕ → ℂ} {s : ℂ} {a : ℂ} (h : LSeriesHasSum f s a) : LSeriesSummable f s

theorem LSeriesHasSum.LSeries_eq {f : ℕ → ℂ} {s : ℂ} {a : ℂ} (h : LSeriesHasSum f s a) : LSeries f s = a

theorem LSeriesSummable.LSeriesHasSum {f : ℕ → ℂ} {s : ℂ} (h : LSeriesSummable f s) : LSeriesHasSum f s (LSeries f s)

theorem LSeriesHasSum_iff {f : ℕ → ℂ} {s : ℂ} {a : ℂ} : LSeriesHasSum f s a ↔ LSeriesSummable f s ∧ LSeries f s = a

theorem LSeriesHasSum_congr {f : ℕ → ℂ} {g : ℕ → ℂ} (s : ℂ) (a : ℂ) (h : ∀ (n : ℕ), n ≠ 0 → f n = g n) : LSeriesHasSum f s a ↔ LSeriesHasSum g s a

theorem LSeriesSummable.of_re_le_re {f : ℕ → ℂ} {s : ℂ} {s' : ℂ} (h : s.re ≤ s'.re) (hf : LSeriesSummable f s) : LSeriesSummable f s'

theorem LSeriesSummable_iff_of_re_eq_re {f : ℕ → ℂ} {s : ℂ} {s' : ℂ} (h : s.re = s'.re) : LSeriesSummable f s ↔ LSeriesSummable f s'

Notation

def LSeries.notation.termL : Lean.ParserDescr

The value of the L-series of the sequence f at the point s if it converges absolutely there, and 0 otherwise.

Equations

• LSeries.notation.termL = Lean.ParserDescr.node `LSeries.notation.termL 1024 (Lean.ParserDescr.symbol "L")

def LSeries.notation.«term↗_» : Lean.ParserDescr

We introduce notation ↗f for f interpreted as a function ℕ → ℂ.

Let R be a ring with a coercion to ℂ. Then we can write ↗χ when χ : DirichletCharacter R or ↗f when f : ArithmeticFunction R or simply f : N → R with a coercion from ℕ to N as an argument to LSeries, LSeriesHasSum, LSeriesSummable etc.

Equations

• LSeries.notation.«term↗_» = Lean.ParserDescr.node `LSeries.notation.term↗_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "↗") (Lean.ParserDescr.cat `term 1024))

Criteria for and consequences of summability of L-series

We relate summability of L-series with bounds on the coefficients in terms of powers of n.

theorem LSeriesSummable.le_const_mul_rpow {f : ℕ → ℂ} {s : ℂ} (h : LSeriesSummable f s) : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re

If the LSeries of f is summable at s, then f n is bounded in absolute value by a constant times n^(re s).

theorem LSeriesSummable.isBigO_rpow {f : ℕ → ℂ} {s : ℂ} (h : LSeriesSummable f s) : f =O[Filter.atTop] fun (n : ℕ) => ↑n ^ s.re

If the LSeries of f is summable at s, then f = O(n^(re s)).

theorem LSeriesSummable_of_le_const_mul_rpow {f : ℕ → ℂ} {x : ℝ} {s : ℂ} (hs : x < s.re) (h : ∃ (C : ℝ), ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)) : LSeriesSummable f s

If f n is bounded in absolute value by a constant times n^(x-1) and re s > x, then the LSeries of f is summable at s.

theorem LSeriesSummable_of_isBigO_rpow {f : ℕ → ℂ} {x : ℝ} {s : ℂ} (hs : x < s.re) (h : f =O[Filter.atTop] fun (n : ℕ) => ↑n ^ (x - 1)) : LSeriesSummable f s

If f = O(n^(x-1)) and re s > x, then the LSeries of f is summable at s.

theorem LSeriesSummable_of_bounded_of_one_lt_re {f : ℕ → ℂ} {m : ℝ} (h : ∀ (n : ℕ), n ≠ 0 → Complex.abs (f n) ≤ m) {s : ℂ} (hs : 1 < s.re) : LSeriesSummable f s

If f is bounded, then its LSeries is summable at s when re s > 1.

theorem LSeriesSummable_of_bounded_of_one_lt_real {f : ℕ → ℂ} {m : ℝ} (h : ∀ (n : ℕ), n ≠ 0 → Complex.abs (f n) ≤ m) {s : ℝ} (hs : 1 < s) : LSeriesSummable f ↑s

If f is bounded, then its LSeries is summable at s : ℝ when s > 1.

theorem LSeriesSummable.one_iff_one_lt_re {s : ℂ} : LSeriesSummable 1 s ↔ 1 < s.re

The LSeries with all coefficients 1 converges at s if and only if re s > 1.

theorem zeta_LSeriesSummable_iff_one_lt_re {s : ℂ} : LSeriesSummable (fun (x : ℕ) => ↑(ArithmeticFunction.zeta x)) s ↔ 1 < s.re

The LSeries associated to the arithmetic function ζ converges at s if and only if re s > 1.