English
A further reformulation of residueClass as a Dirichlet-twisted sum, showing the same linear combination with scaled coefficients.
Русский
Дополнительная переработка residueClass как сумма twists Dirichlet, демонстрирующая ту же линейную комбинацию с масштабированными коэффициентами.
LaTeX
$$$\operatorname{residueClass}(a) = (q\varphi(q))^{-1} \sum_{\chi} χ(a)^{-1} χ(n) Λ(n)$$$
Lean4
/-- We can express `ArithmeticFunction.vonMangoldt.residueClass` as a linear combination
of twists of the von Mangoldt function by Dirichlet characters. -/
theorem residueClass_eq (ha : IsUnit a) :
↗(residueClass a) = (q.totient : ℂ)⁻¹ • ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ • (fun n : ℕ ↦ χ n * vonMangoldt n) :=
by
ext1 n
simpa only [Pi.smul_apply, Finset.sum_apply, smul_eq_mul, ← mul_assoc] using residueClass_apply ha n
