English
Equations expressing residueClass as a linear combination of twists with Dirichlet characters; the equality is stated componentwise on the natural numbers.
Русский
Уравнение, выражающее residueClass через линейную комбинацию twists с символами Дирихле; равенство выполняется по каждому n.
LaTeX
$$∗ равенство residueClass как сумма по χ ∈ Dirichlet(ℂ,q) хχ⁻¹ · χ(n) · vonMangoldt(n)$$
Lean4
/-- We can express `ArithmeticFunction.vonMangoldt.residueClass` as a linear combination
of twists of the von Mangoldt function by Dirichlet characters. -/
theorem residueClass_apply (ha : IsUnit a) (n : ℕ) :
residueClass a n = (q.totient : ℂ)⁻¹ * ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * χ n * vonMangoldt n :=
by
rw [eq_inv_mul_iff_mul_eq₀ <| mod_cast (Nat.totient_pos.mpr q.pos_of_neZero).ne']
simp +contextual only [residueClass, Set.indicator_apply, Set.mem_setOf_eq, apply_ite, ofReal_zero, mul_zero,
← Finset.sum_mul, sum_char_inv_mul_char_eq ℂ ha n, eq_comm (a := a), ite_mul, zero_mul, ↓reduceIte, ite_self]
