English
Let q be a positive integer and a an invertible residue modulo q. Then the L-series of the von Mangoldt function restricted to the residue class of a modulo q is a linear combination of the logarithmic derivatives of Dirichlet L-functions modulo q; precisely for Re(s) > 1 it holds an explicit identity expressing LSeries of the residue class in terms of Dirichlet characters.
Русский
Пусть q — положительное целое число, а — единично обратимый элемент по модулю q. Тогда L‑серия vonMangoldt, ограниченная остаточным классом a mod q, является линейной комбинацией логарифмических производных L-функций Дирихле по модулю q; для Re(s) > 1 выполняется явное тождество, выражающее LSeries остаточного класса через символы Дирихле.
LaTeX
$$$LSeries(\\operatorname{residueClass}_a)(s) = -\\left(\\phi(q)\\right)^{-1} \\sum_{\\chi: DirichletCharacter(\\mathbb{C},q)} χ(a)^{-1} \\frac{\\frac{d}{ds}LFunction(χ)(s)}{LFunction(χ)(s)} \\, , \\quad \\text{for } 1 < \\Re(s).$$$
Lean4
/-- The L-series of the von Mangoldt function restricted to the residue class `a` mod `q`
with `a` invertible in `ZMod q` is a linear combination of logarithmic derivatives of
L-functions of the Dirichlet characters mod `q` (on `re s > 1`). -/
theorem LSeries_residueClass_eq (ha : IsUnit a) {s : ℂ} (hs : 1 < s.re) :
LSeries (↗(residueClass a)) s =
-(q.totient : ℂ)⁻¹ * ∑ χ : DirichletCharacter ℂ q, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s) :=
by
simp only [deriv_LFunction_eq_deriv_LSeries _ hs, LFunction_eq_LSeries _ hs, neg_mul, ← mul_neg,
← Finset.sum_neg_distrib, ← neg_div, ← LSeries_twist_vonMangoldt_eq _ hs]
rw [eq_inv_mul_iff_mul_eq₀ <| mod_cast (Nat.totient_pos.mpr q.pos_of_neZero).ne']
simp_rw [← LSeries_smul, ← LSeries_sum <| fun χ _ ↦ (LSeriesSummable_twist_vonMangoldt χ hs).smul _]
refine LSeries_congr (fun {n} _ ↦ ?_) s
simp only [Pi.smul_apply, residueClass_apply ha, smul_eq_mul, ← mul_assoc, mul_inv_cancel_of_invertible, one_mul,
Finset.sum_apply, Pi.mul_apply]
