LSeriesSummable_of_abscissaOfAbsConv_lt_re

English

If the abscissa of absolute convergence of f is to the left of the real part of s (i.e. abscissaOfAbsConv f < Re(s)), then the L-series L(f,s) is summable: LSeriesSummable f s.

Русский

Если абсцисса абсолютной сходимости функции f лежит слева от вещественной части комплексного числа s, то серия сходится.

LaTeX

$$$\\forall f:\\mathbb{N}\\to\\mathbb{C},\\; \\text{if } \\operatorname{abscissaOfAbsConv}(f) < \\Re(s) \\text{ then } LSeriesSummable(f,s).$$$

Lean4

theorem LSeriesSummable_of_abscissaOfAbsConv_lt_re {f : ℕ → ℂ} {s : ℂ} (hs : abscissaOfAbsConv f < s.re) :
    LSeriesSummable f s :=
  by
  obtain ⟨y, hy, hys⟩ : ∃ a : ℝ, LSeriesSummable f a ∧ a < s.re := by simpa [abscissaOfAbsConv, sInf_lt_iff] using hs
  exact hy.of_re_le_re <| ofReal_re y ▸ hys.le

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