LSeriesHasSum

Mathlib.NumberTheory.LSeries.Basic

URI: https://scilib.ai/kg/mathlib#LSeriesSummable.LSeriesHasSum

English

If f is L-series summable at s, then f has a sum at s given by LSeries f s.

Русский

Если L-серия суммируема в s, значит существует сумма, равная LSeries f s.

LaTeX

$$LSeriesSummable(f,s) → LSeriesHasSum(f,s, LSeries(f,s))$$

Lean4

theorem LSeriesHasSum {f : ℕ → ℂ} {s : ℂ} (h : LSeriesSummable f s) : LSeriesHasSum f s (LSeries f s) :=
  h.hasSum

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

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

Разделы

Аффилиация

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