abscissaOfAbsConv_convolution_le — Mathlib

English

The abscissa of absolute convergence of the convolution f ⍟ g is at most the maximum of the abscissae of absolute convergence of f and g.

Русский

Абсцисса абсолютной сходимости свёртки f ⍟ g не больше максимума абсисс абсолютной сходимости f и g.

LaTeX

$$$abscissaOfAbsConv (convolution f g) \leq max (abscissaOfAbsConv f) (abscissaOfAbsConv g)$$$

Lean4

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

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