LSeries_hasDerivAt — Mathlib

English

If abscissaOfAbsConv f < s.re, then the derivative of LSeries f at s equals the negative of the L-series of logMul f at s:

Русский

Если abscissaOfAbsConv f < s.re, то производная LSeries f в s равна минусу LSeries(logMul f) в s.

LaTeX

$$HasDerivAt (LSeries f) (-LSeries (logMul f) s) s$$

Lean4

/-- 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`. -/
theorem LSeries_hasDerivAt {f : ℕ → ℂ} {s : ℂ} (h : abscissaOfAbsConv f < s.re) :
    HasDerivAt (LSeries f) (-LSeries (logMul f) s) s :=
  (LSeriesSummable_logMul_and_hasDerivAt h).2

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