abscissaOfAbsConv_add_le — Mathlib

English

Let f, g: N → C. The abscissa of absolute convergence of f + g is at most the maximum of the abscissas of f and g.

Русский

Пусть f, g: N → C. Абсцисса абсолютной сходимости суммы f + g не превосходит максимум абсцисс f и g.

LaTeX

$$$$ \operatorname{abscissaOfAbsConv}(f+g) \le \max\big(\operatorname{abscissaOfAbsConv}(f), \operatorname{abscissaOfAbsConv}(g)\big). $$$$

Lean4

/-- The abscissa of absolute convergence of `f + g` is at most the maximum of those
of `f` and `g`. -/
theorem abscissaOfAbsConv_add_le (f g : ℕ → ℂ) :
    abscissaOfAbsConv (f + g) ≤ max (abscissaOfAbsConv f) (abscissaOfAbsConv g) :=
  abscissaOfAbsConv_binop_le LSeriesSummable.add f g

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