English
The residueClass function can be expressed as a linear combination of twists of vonMangoldt by Dirichlet characters; concretely, residueClass(a,n) equals a normalized sum over χ of χ(a)⁻¹ χ(n) vonMangoldt(n).
Русский
residueClass может быть выражена через линейную комбинацию twists vonMangoldt по символьной теории Дирихле: residueClass(a,n) = (q- totient)^-1 ∑ χ χ(a)⁻¹ χ(n) vonMangoldt(n).
LaTeX
$$residueClass(a;n) = (q totient)^{-1} Σ_{χ} χ(a)^{-1} χ(n) vonMangoldt(n)$$
Lean4
theorem abscissaOfAbsConv_residueClass_le_one : abscissaOfAbsConv ↗(residueClass a) ≤ 1 :=
by
refine abscissaOfAbsConv_le_of_forall_lt_LSeriesSummable fun y hy ↦ ?_
unfold LSeriesSummable
have := LSeriesSummable_vonMangoldt <| show 1 < (y : ℂ).re by simp only [ofReal_re, hy]
convert this.indicator {n : ℕ | (n : ZMod q) = a}
ext1 n
by_cases hn : (n : ZMod q) = a
· simp +contextual only [term, Set.indicator, Set.mem_setOf_eq, hn, ↓reduceIte, apply_ite, ite_self]
·
simp +contextual only [term, Set.mem_setOf_eq, hn, not_false_eq_true, Set.indicator_of_notMem, ofReal_zero,
zero_div, ite_self]
