English
Twisting by χ distributes over convolution with two functions f and g: (((χ·) * f) ⍟ (((χ·) * g)) = ((χ·) * (f ⍟ g)).
Русский
Повторное вращение χ над конволюцией двух функций распределяется одинаково: ((χ·) * f) ⍟ ((χ·) * g) = (χ·) * (f ⍟ g).
LaTeX
$$$(((\chi \cdot) * f) \ast ((\chi \cdot) * g)) = (\chi \cdot) * (f * g).$$$
Lean4
/-- The convolution of a Dirichlet character `χ` with the twist `χ * μ` is `δ`,
the indicator function of `{1}`. -/
theorem convolution_mul_moebius {n : ℕ} (χ : DirichletCharacter ℂ n) : ↗χ ⍟ (↗χ * ↗μ) = δ :=
by
have : (1 : ℕ → ℂ) ⍟ (μ ·) = δ :=
by
rw [one_convolution_eq_zeta_convolution, ← one_eq_delta]
simp_rw [← natCoe_apply, ← intCoe_apply, coe_mul, coe_zeta_mul_coe_moebius]
nth_rewrite 1 [← mul_one ↗χ]
simpa only [mul_convolution_distrib χ 1 ↗μ, this] using mul_delta _
