English
The auxiliary L-function for a residue class a modulo q is defined by a specific linear combination involving the trivial Dirichlet character and all nontrivial Dirichlet characters, and it is used in analytic proofs of Dirichlet's theorem.
Русский
Вспомогательная L-функция для остаточного класса a по модулю q задаётся через линейную комбинацию, включающую тривиальный и все не тривиальные символы Дирихле, и применяется в аналитических доказательствах теоремы Дирихле.
LaTeX
$$$\\mathrm{LFunctionResidueClassAux}(a,s) = \\frac{1}{q.totient} \\Big(-\\frac{d}{ds}LFunctionTrivChar_1(q,s) / LFunctionTrivChar_1(q,s) - \\sum_{\\chi \\in \\{1\\}^{c}} χ(a)^{-1} \\frac{d}{ds}LFunction(χ)(s) / LFunction(χ)(s) \\Big)$$$
Lean4
/-- The auxiliary function used, e.g., with the Wiener-Ikehara Theorem to prove
Dirichlet's Theorem. On `re s > 1`, it agrees with the L-series of the von Mangoldt
function restricted to the residue class `a : ZMod q` minus the principal part
`(q.totient)⁻¹/(s-1)` of the pole at `s = 1`;
see `ArithmeticFunction.vonMangoldt.eqOn_LFunctionResidueClassAux`. -/
noncomputable abbrev LFunctionResidueClassAux (s : ℂ) : ℂ :=
(q.totient : ℂ)⁻¹ *
(-deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s -
∑ χ ∈ ({ 1 }ᶜ : Finset (DirichletCharacter ℂ q)), χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s)
