English
In the open half-plane of absolute convergence, the m-th derivative of the L-series is given by (-1)^m times the L-series of log^m * f.
Русский
В открытой половине пространства абсцисс абсолютной сходимости m-я производная L‑серии равна (-1)^m умноженному на LSeries(logMul^[m] f).
LaTeX
$$iteratedDeriv m (LSeries f) s = (-1)^{m} * LSeries (logMul^[m] f) s$$
Lean4
/-- The derivative of the L-series of `f` agrees with the negative of the L-series of
`log * f` on the right half-plane of absolute convergence. -/
theorem LSeries_deriv_eqOn {f : ℕ → ℂ} :
{s | abscissaOfAbsConv f < s.re}.EqOn (deriv (LSeries f)) (-LSeries (logMul f)) :=
deriv_eqOn (isOpen_re_gt_EReal _) fun _ hs ↦ (LSeries_hasDerivAt hs).hasDerivWithinAt
