convolution — Mathlib

English

The L-series of the convolution product f ⍟ g is summable whenever both L-series are summable.

Русский

L‑серия свёртки f ⍟ g суммируема тогда и только тогда, когда обе L‑серии суммируемы.

LaTeX

$$$LSeriesSummable f s \Rightarrow LSeriesSummable g s \Rightarrow LSeriesSummable (convolution f g) s$$$

Lean4

/-- The L-series of the convolution product `f ⍟ g` of two sequences `f` and `g`
is summable when both L-series are summable. -/
theorem convolution {f g : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s) (hg : LSeriesSummable g s) :
    LSeriesSummable (f ⍟ g) s :=
  (LSeriesHasSum.convolution hf.LSeriesHasSum hg.LSeriesHasSum).LSeriesSummable

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