abscissaOfAbsConv_sub_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_sub_le (f g : ℕ → ℂ) :
    abscissaOfAbsConv (f - g) ≤ max (abscissaOfAbsConv f) (abscissaOfAbsConv g) :=
  abscissaOfAbsConv_binop_le LSeriesSummable.sub f g

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