LSeries_analyticOnNhd — Mathlib

English

The L-series LSeries f is analytic in a neighborhood of every point in the open half-plane of absolute convergence.

Русский

LSeries f аналитична в окрестности каждой точки в открытой половине пространства абсцисс абсолютной сходимости.

LaTeX

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

Lean4

/-- The L-series of `f` is holomorphic on its open half-plane of absolute convergence. -/
theorem LSeries_analyticOnNhd (f : ℕ → ℂ) : AnalyticOnNhd ℂ (LSeries f) {s | abscissaOfAbsConv f < s.re} :=
  (LSeries_differentiableOn f).analyticOnNhd <| isOpen_re_gt_EReal _

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