English
For any Dirichlet character χ and Re(s) > 1, the L-series of the twist of Λ by χ equals the negative derivative of the L-series of χ divided by the L-series of χ: L((↗χ * ↗Λ), s) = -d/ds L(↗χ) s / L(↗χ) s.
Русский
Для любого χ при Re(s) > 1: L((↗χ * ↗Λ), s) = - (d/ds) L(↗χ, s) / L(↗χ, s).
LaTeX
$$L(↑χ * ↑Λ) s = - deriv(L ↑χ) s / L ↑χ s$$
Lean4
/-- The L-series of the twist of the von Mangoldt function `Λ` by a Dirichlet character `χ` at `s`
equals the negative logarithmic derivative of the L-series of `χ` when `re s > 1`. -/
theorem LSeries_twist_vonMangoldt_eq {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :
L (↗χ * ↗Λ) s = -deriv (L ↗χ) s / L (↗χ) s :=
by
rcases eq_or_ne N 0 with rfl | hN
·
simp [modZero_eq_delta, delta_mul_eq_smul_delta, LSeries_delta]
-- now `N ≠ 0`
have hχ : LSeriesSummable (↗χ) s := (LSeriesSummable_iff hN χ).mpr hs
have hs' : abscissaOfAbsConv ↗χ < s.re := by rwa [absicssaOfAbsConv_eq_one hN, ← EReal.coe_one, EReal.coe_lt_coe_iff]
have hΛ : LSeriesSummable (↗χ * ↗Λ) s := LSeriesSummable_twist_vonMangoldt χ hs
rw [eq_div_iff <| LSeries_ne_zero_of_one_lt_re χ hs, ← LSeries_convolution' hΛ hχ, convolution_twist_vonMangoldt,
LSeries_deriv hs', neg_neg]
exact LSeries_congr (fun _ ↦ by simp [mul_comm, logMul]) s
