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.

Reference

For some background on the design decisions made when implementing L-series in Mathlib (and applications motivating the development), see the paper Formalizing zeta and L-functions in Lean by David Loeffler and Michael Stoll.

Tags

L-series

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.

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

theorem LSeries.term_def₀ {f : ℕ → ℂ} (hf : f 0 = 0) (s : ℂ) (n : ℕ) : term f s n = f n * ↑n ^ (-s)

An alternate spelling of term_def for the case f 0 = 0.

@[simp]

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

@[simp]

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

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

If s ≠ 0, then the if .. then .. else construction in LSeries.term isn't needed, since 0 ^ s = 0.

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

theorem LSeries.pow_mul_term_eq (f : ℕ → ℂ) (s : ℂ) (n : ℕ) : (↑n + 1) ^ s * term f s (n + 1) = f (n + 1)

theorem LSeries.norm_term_eq (f : ℕ → ℂ) (s : ℂ) (n : ℕ) : ‖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‖) : ‖term f s n‖ ≤ ‖term g s n‖

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

theorem LSeries.term_nonneg {a : ℕ → ℂ} {n : ℕ} (h : 0 ≤ a n) (x : ℝ) : 0 ≤ term a (↑x) n

theorem LSeries.term_pos {a : ℕ → ℂ} {n : ℕ} (hn : n ≠ 0) (h : 0 < a n) (x : ℝ) : 0 < term a (↑x) 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.

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.

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.

theorem LSeriesHasSum.LSeriesSummable {f : ℕ → ℂ} {s a : ℂ} (h : LSeriesHasSum f s a) : _root_.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) : _root_.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'

def LSeries.delta (n : ℕ) : ℂ

The indicator function of {1} ⊆ ℕ with values in ℂ.

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.

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.

def LSeries.notation.termδ : Lean.ParserDescr

The indicator function of {1} ⊆ ℕ with values in ℂ.

LSeries of 0 and δ

@[simp]

theorem LSeries_zero : LSeries 0 = 0

theorem LSeries.term_delta (s : ℂ) (n : ℕ) : term delta s n = if n = 1 then 1 else 0

theorem LSeries.mul_delta_eq_smul_delta {f : ℕ → ℂ} : f * delta = f 1 • delta

theorem LSeries.mul_delta {f : ℕ → ℂ} (h : f 1 = 1) : f * delta = delta

theorem LSeries.delta_mul_eq_smul_delta {f : ℕ → ℂ} : delta * f = f 1 • delta

theorem LSeries.delta_mul {f : ℕ → ℂ} (h : f 1 = 1) : delta * f = delta

theorem LSeries_delta : LSeries LSeries.delta = 1

The L-series of δ is the constant function 1.

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 → ‖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 → ‖f n‖ ≤ m) {s : ℝ} (hs : 1 < s) : LSeriesSummable f ↑s

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