L-series #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Given an arithmetic function, we define the corresponding L-series.
Main Definitions #
nat.arithmetic_function.l_seriesis thel_serieswith a given arithmetic function as its coefficients. This is not the analytic continuation, just the infinite series.nat.arithmetic_function.l_series_summableindicates that thel_seriesconverges at a given point.
Main Results #
nat.arithmetic_function.l_series_summable_of_bounded_of_one_lt_re: thel_seriesof a bounded arithmetic function converges when1 < z.re.nat.arithmetic_function.zeta_l_series_summable_iff_one_lt_re: thel_seriesofζ(whose analytic continuation is the Riemann ζ) converges iff1 < z.re.
f.l_series_summable z indicates that the L-series of f converges at z.
theorem
nat.arithmetic_function.l_series_eq_zero_of_not_l_series_summable
(f : nat.arithmetic_function ℂ)
(z : ℂ) :
¬f.l_series_summable z → f.l_series z = 0
@[simp]
theorem
nat.arithmetic_function.l_series_summable_of_bounded_of_one_lt_real
{f : nat.arithmetic_function ℂ}
{m : ℝ}
(h : ∀ (n : ℕ), ⇑complex.abs (⇑f n) ≤ m)
{z : ℝ}
(hz : 1 < z) :
theorem
nat.arithmetic_function.l_series_summable_iff_of_re_eq_re
{f : nat.arithmetic_function ℂ}
{w z : ℂ}
(h : w.re = z.re) :
f.l_series_summable w ↔ f.l_series_summable z
theorem
nat.arithmetic_function.l_series_summable_of_bounded_of_one_lt_re
{f : nat.arithmetic_function ℂ}
{m : ℝ}
(h : ∀ (n : ℕ), ⇑complex.abs (⇑f n) ≤ m)
{z : ℂ}
(hz : 1 < z.re) :
@[simp]
theorem
nat.arithmetic_function.l_series_add
{f g : nat.arithmetic_function ℂ}
{z : ℂ}
(hf : f.l_series_summable z)
(hg : g.l_series_summable z) :