LSeriesSummable_mul — Mathlib

English

For arithmetic functions f and g, the L-series of their Dirichlet convolution is summable whenever both L-series are summable.

Русский

Для арифметических функций f и g сумма L‑серии свёртки существует, когда обе L‑серии суммируемы.

LaTeX

$$$LSeriesSummable (\uparrow f) s \land LSeriesSummable (\uparrow g) s \Rightarrow LSeriesSummable (\uparrow (f * g)) s$$$

Lean4

/-- The L-series of the (convolution) product of two `ℂ`-valued arithmetic functions `f` and `g`
is summable when both L-series are summable. -/
theorem LSeriesSummable_mul {f g : ArithmeticFunction ℂ} {s : ℂ} (hf : LSeriesSummable (↗f) s)
    (hg : LSeriesSummable (↗g) s) : LSeriesSummable (↗(f * g)) s :=
  coe_mul f g ▸ hf.convolution hg

Похожие утверждения