LSeries_deriv — Mathlib

English

The derivative of LSeries equals minus LSeries of logMul f on the right half-plane where abscissaOfAbsConv f is less than s.re.

Русский

Производная L‑серии равна минусу LSeries(logMul f) на области, где abscissaOfAbsConv f < s.re.

LaTeX

$${s | abscissaOfAbsConv f < s.re}.EqOn (deriv (LSeries f)) (-LSeries (logMul f))$$

Lean4

/-- If `re s` is greater than the abscissa of absolute convergence of `f`, then
the derivative of this L-series at `s` is the negative of the L-series of `log * f`. -/
theorem LSeries_deriv {f : ℕ → ℂ} {s : ℂ} (h : abscissaOfAbsConv f < s.re) :
    deriv (LSeries f) s = -LSeries (logMul f) s :=
  (LSeries_hasDerivAt h).deriv

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