English
The L-series of von Mangoldt Λ equals the negative derivative of the Riemann zeta function divided by the zeta function: L((↗Λ), s) = -ζ'(s)/ζ(s) for Re(s) > 1.
Русский
L-ряд Λ равен отрицательной производной дзета-функции, деленной на дзета-функцию: L((↗Λ), s) = -ζ'(s)/ζ(s).
LaTeX
$$L(↑Λ) s = - deriv(riemannZeta) s / riemannZeta s$$
Lean4
/-- The L-series of the von Mangoldt function `Λ` equals the negative logarithmic derivative
of the Riemann zeta function on its domain of convergence `re s > 1`. -/
theorem LSeries_vonMangoldt_eq_deriv_riemannZeta_div {s : ℂ} (hs : 1 < s.re) :
L (↗Λ) s = -deriv riemannZeta s / riemannZeta s :=
by
suffices deriv (L 1) s = deriv riemannZeta s by rw [LSeries_vonMangoldt_eq hs, ← LSeries_one_eq_riemannZeta hs, this]
refine Filter.EventuallyEq.deriv_eq <| Filter.eventuallyEq_iff_exists_mem.mpr ?_
exact ⟨{z | 1 < z.re}, (isOpen_lt continuous_const continuous_re).mem_nhds hs, fun _ ↦ LSeries_one_eq_riemannZeta⟩
