L-series

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

Main Definitions

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

Main Results

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

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

The L-series of an ArithmeticFunction.

Equations

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

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

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

Equations

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

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

@[simp]

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

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

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

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

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

@[simp]

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