LSeries_analyticOn

Mathlib.NumberTheory.LSeries.Deriv

URI: https://scilib.ai/kg/mathlib#LSeries_analyticOn

English

The L-series LSeries f is analytic on the open half-plane {s | abscissaOfAbsConv f < s.re}.

Русский

LSeries f аналитична на открытой половине пространства {s | abscissaOfAbsConv f < s.re}.

LaTeX

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

Lean4

theorem LSeries_analyticOn (f : ℕ → ℂ) : AnalyticOn ℂ (LSeries f) {s | abscissaOfAbsConv f < s.re} :=
  (LSeries_analyticOnNhd f).analyticOn

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru