English
Let f,g: N → C. If the L-series of f at s converges with sum a and the L-series of g at s converges with sum b, then the L-series of their convolution f ⍟ g at s converges with sum a b.
Русский
Пусть f,g: ℕ → ℂ. Если L‑серия f в точке s сходится и имеет сумму a, а L‑серия g в точке s сходится и имеет сумму b, то L‑серия их свёртки f ⍟ g в точке s сходится и имеет сумму a b.
LaTeX
$$$LSeriesHasSum f s a \land LSeriesHasSum g s b \Rightarrow LSeriesHasSum (convolution f g) s (a b)$$$
Lean4
/-- The L-series of the convolution product `f ⍟ g` of two sequences `f` and `g`
equals the product of their L-series, assuming both L-series converge. -/
theorem convolution {f g : ℕ → ℂ} {s a b : ℂ} (hf : LSeriesHasSum f s a) (hg : LSeriesHasSum g s b) :
LSeriesHasSum (f ⍟ g) s (a * b) :=
by
have hsum := summable_mul_of_summable_norm hf.summable.norm hg.summable.norm
simpa only [LSeriesHasSum, term_convolution'] using (hf.mul hg hsum).tsum_fiberwise _
