English
Let f,g: ℕ → ℂ be summable at s. Then the L-series of their convolution equals the product of their L-series: LSeries(convolution f g) s = LSeries f s · LSeries g s.
Русский
Пусть f,g: ℕ → ℂ суммируемы при s. Тогда L‑серия их свёртки равна произведению L‑серий: LSeries(convolution f g) s = LSeries f s · LSeries g s.
LaTeX
$$$LSeriesSummable f s \land LSeriesSummable g s \Rightarrow LSeries (convolution f g) s = LSeries f s \cdot LSeries g s$$$
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 LSeries_convolution' {f g : ℕ → ℂ} {s : ℂ} (hf : LSeriesSummable f s) (hg : LSeriesSummable g s) :
LSeries (f ⍟ g) s = LSeries f s * LSeries g s :=
(LSeriesHasSum.convolution hf.LSeriesHasSum hg.LSeriesHasSum).LSeries_eq
