English
If abscissaOfAbsConv f < s.re and abscissaOfAbsConv g < s.re, then the L-series of their convolution equals the product of their L-series at s: LSeries(convolution f g) s = LSeries f s · LSeries g s.
Русский
Если числа сходимости по абсолютной величине для f и g меньше вещественной части s, то L‑серия их свёртки равна произведению L‑серий при s.
LaTeX
$$$abscissaOfAbsConv f < s.re \land abscissaOfAbsConv g < s.re \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 in their common half-plane of absolute convergence. -/
theorem LSeries_convolution {f g : ℕ → ℂ} {s : ℂ} (hf : abscissaOfAbsConv f < s.re) (hg : abscissaOfAbsConv g < s.re) :
LSeries (f ⍟ g) s = LSeries f s * LSeries g s :=
LSeries_convolution' (LSeriesSummable_of_abscissaOfAbsConv_lt_re hf) (LSeriesSummable_of_abscissaOfAbsConv_lt_re hg)
