L-series

Given an arithmetic function, we define the corresponding L-series.

Main Definitions

• ArithmeticFunction.LSeries is the LSeries with a given arithmetic function as its coefficients. This is not the analytic continuation, just the infinite series.
• ArithmeticFunction.LSeriesSummable indicates that the LSeries converges at a given point.

Main Results

• ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_real: the LSeries of a bounded arithmetic function converges when 1 < z.re.
• ArithmeticFunction.zeta_LSeriesSummable_iff_one_lt_re: the LSeries of ζ (whose analytic continuation is the Riemann ζ) converges iff 1 < z.re.

def ArithmeticFunction.LSeries (f : ArithmeticFunction ℂ) (z : ℂ) : ℂ

The L-series of an ArithmeticFunction.

Equations

• ArithmeticFunction.LSeries f z = ∑' (n : ℕ), f n / ↑n ^ z

def ArithmeticFunction.LSeriesSummable (f : ArithmeticFunction ℂ) (z : ℂ) : Prop

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

Equations

• ArithmeticFunction.LSeriesSummable f z = Summable fun (n : ℕ) => f n / ↑n ^ z

theorem ArithmeticFunction.LSeries_eq_zero_of_not_LSeriesSummable (f : ArithmeticFunction ℂ) (z : ℂ) : ¬ArithmeticFunction.LSeriesSummable f z → ArithmeticFunction.LSeries f z = 0

@[simp]

theorem ArithmeticFunction.LSeriesSummable_zero {z : ℂ} : ArithmeticFunction.LSeriesSummable 0 z

theorem ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_real {f : ArithmeticFunction ℂ} {m : ℝ} (h : ∀ (n : ℕ), Complex.abs (f n) ≤ m) {z : ℝ} (hz : 1 < z) : ArithmeticFunction.LSeriesSummable f ↑z

theorem ArithmeticFunction.LSeriesSummable_iff_of_re_eq_re {f : ArithmeticFunction ℂ} {w : ℂ} {z : ℂ} (h : w.re = z.re) : ArithmeticFunction.LSeriesSummable f w ↔ ArithmeticFunction.LSeriesSummable f z

theorem ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_re {f : ArithmeticFunction ℂ} {m : ℝ} (h : ∀ (n : ℕ), Complex.abs (f n) ≤ m) {z : ℂ} (hz : 1 < z.re) : ArithmeticFunction.LSeriesSummable f z

theorem ArithmeticFunction.zeta_LSeriesSummable_iff_one_lt_re {z : ℂ} : ArithmeticFunction.LSeriesSummable (↑ArithmeticFunction.zeta) z ↔ 1 < z.re

@[simp]

theorem ArithmeticFunction.LSeries_add {f : ArithmeticFunction ℂ} {g : ArithmeticFunction ℂ} {z : ℂ} (hf : ArithmeticFunction.LSeriesSummable f z) (hg : ArithmeticFunction.LSeriesSummable g z) : ArithmeticFunction.LSeries (f + g) z = ArithmeticFunction.LSeries f z + ArithmeticFunction.LSeries g z