English
Let f,g be arithmetic functions with complex values. If hf and hg are L-series sums for ↗f and ↗g at s with sums a and b, respectively, then the L-series of their product satisfies LSeriesHasSum (↗(f * g)) s (a * b).
Русский
Пусть f,g — арифметические функции со значениями в ℂ. Если hf и hg задают суммы L‑серий ↗f и ↗g в точке s со значениями a и b соответственно, то LSeriesHasSum (↗(f * g)) s (a b).
LaTeX
$$$LSeriesHasSum (\uparrow f) s a \land LSeriesHasSum (\uparrow g) s b \Rightarrow LSeriesHasSum (\uparrow (f * g)) s (a b)$$$
Lean4
/-- The L-series of the (convolution) product of two `ℂ`-valued arithmetic functions `f` and `g`
equals the product of their L-series, assuming both L-series converge. -/
theorem LSeriesHasSum_mul {f g : ArithmeticFunction ℂ} {s a b : ℂ} (hf : LSeriesHasSum (↗f) s a)
(hg : LSeriesHasSum (↗g) s b) : LSeriesHasSum (↗(f * g)) s (a * b) :=
coe_mul f g ▸ hf.convolution hg
