LSeries_zeta_eq_riemannZeta — Mathlib

English

For s with Re(s) > 1, the L-series of ζ equals the Riemann zeta function, riemannZeta(s).

Русский

При Re(s) > 1 L-ряд ζ совпадает с функцией дзета Римана riemannZeta(s).

LaTeX

$$$L(\uparrow ζ)(s) = \operatorname{riemannZeta}(s) \quad (\Re(s) > 1).$$$

Lean4

/-- The L-series of the arithmetic function `ζ` equals the Riemann Zeta Function on its
domain of convergence `1 < re s`. -/
theorem LSeries_zeta_eq_riemannZeta {s : ℂ} (hs : 1 < s.re) : L (↗ζ) s = riemannZeta s :=
  by
  suffices ∑' n, term (fun n ↦ if n = 0 then 0 else 1) s n = ∑' n : ℕ, 1 / (n : ℂ) ^ s by
    simpa [LSeries, zeta_eq_tsum_one_div_nat_cpow hs]
  refine tsum_congr fun n ↦ ?_
  rcases eq_or_ne n 0 with hn | hn <;> simp [hn, ne_zero_of_one_lt_re hs]

Похожие утверждения