LSeries_differentiableOn — Mathlib

English

The L-series LSeries f is complex differentiable on the open half-plane where abscissaOfAbsConv f < s.re.

Русский

LSeries f является комплексно дифференцируемой на открытой половине пространства, где abscissaOfAbsConv f < s.re.

LaTeX

$$DifferentiableOn \mathbb{C} (LSeries f) {s | abscissaOfAbsConv f < s.re}$$

Lean4

/-- The L-series of `f` is complex differentiable in its open half-plane of absolute
convergence. -/
theorem LSeries_differentiableOn (f : ℕ → ℂ) : DifferentiableOn ℂ (LSeries f) {s | abscissaOfAbsConv f < s.re} :=
  fun _ hz ↦ (LSeries_hasDerivAt hz).differentiableAt.differentiableWithinAt

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