Theorems · Theorem · number theory

LSeries_hasDerivAt

∀ {f : ℕ → ℂ} {s : ℂ}, LSeries.abscissaOfAbsConv f < ↑s.re → HasDerivAt (LSeries f) (-LSeries (LSeries.logMul f) s) s

If re s is greater than the abscissa of absolute convergence of f, then the L-series of f is differentiable with derivative the negative of the L-series of the point-wise product of log with f.

Defined in

Mathlib.NumberTheory.LSeries.Deriv

Cited by

3 results in Mathlib

Foundations

Depth 294 from the axioms · uses propext, Classical.choice, Quot.sound