abscissaOfAbsConv_le — Mathlib

English

If LSeriesSummable f s holds, then the abscissa of absolute convergence satisfies abscissaOfAbsConv f ≤ Re(s).

Русский

Если сумма L‑серии сходится при s, то абсцисса абсолютной сходимости не превосходит вещественную часть s.

LaTeX

$$$\\forall f:\\mathbb{N}\\to\\mathbb{C},\\; LSeriesSummable f s \\Rightarrow \\operatorname{abscissaOfAbsConv}(f) \\le \\Re(s).$$$

Lean4

theorem abscissaOfAbsConv_le {f : ℕ → ℂ} {s : ℂ} (h : LSeriesSummable f s) : abscissaOfAbsConv f ≤ s.re :=
  sInf_le <| by simpa using h.of_re_le_re (by simp)

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