English
There is a precise formula expressing residueClass as a linear combination of Dirichlet characters; this is the exact equality residueClass = (q totient)^{-1} Σ χ χ a⁻¹ χ n vonMangoldt(n).
Русский
Существует точная формула выражающая residueClass как линейную комбинацию символов Дирихле: residueClass = (q totient)^{-1} Σ χ χ a⁻¹ χ n vonMangoldt(n).
LaTeX
$$$\operatorname{residueClass}(a;n) = (q\varphi(q))^{-1} \sum_{\chi} χ(a)^{-1} χ(n) \ Λ(n)$$$
Lean4
/-- The set we are interested in (prime numbers in the residue class `a`) is the same as the support
of `ArithmeticFunction.vonMangoldt.residueClass` restricted to primes (and divided by `n`;
this is how this result is used later). -/
theorem support_residueClass_prime_div :
Function.support (fun n : ℕ ↦ (if n.Prime then residueClass a n else 0) / n) =
{p : ℕ | p.Prime ∧ (p : ZMod q) = a} :=
by
simp only [Function.support, ne_eq, div_eq_zero_iff, ite_eq_right_iff, Set.indicator_apply_eq_zero, Set.mem_setOf_eq,
Nat.cast_eq_zero, not_or, Classical.not_imp]
ext1 p
simp only [Set.mem_setOf_eq]
exact ⟨fun H ↦ ⟨H.1.1, H.1.2.1⟩, fun H ↦ ⟨⟨H.1, H.2, vonMangoldt_ne_zero_iff.mpr H.1.isPrimePow⟩, H.1.ne_zero⟩⟩
