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