English
On the half-plane Re(s) > 1, the auxiliary L-function coincides with the L-series of the residue class a minus the principal part (q totient)^{-1}/(s-1) of its pole at s = 1.
Русский
В полуплоскости Re(s) > 1 вспомогательная L-функция совпадает с L-функцией остаточного класса a за вычетом главной части (q totient)^{-1}/(s-1) полю при s = 1.
LaTeX
$$$LFunctionResidueClassAux(a,s) = L(\\operatorname{residueClass}_a)(s) - (q.totient)^{-1} /(s-1)$ для $1<\\Re(s)$$$
Lean4
/-- The auxiliary function agrees on `re s > 1` 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 its pole at `s = 1`. -/
theorem eqOn_LFunctionResidueClassAux (ha : IsUnit a) :
Set.EqOn (LFunctionResidueClassAux a) (fun s ↦ L (↗(residueClass a)) s - (q.totient : ℂ)⁻¹ / (s - 1))
{s | 1 < s.re} :=
by
intro s hs
replace hs := Set.mem_setOf.mp hs
simp only [LSeries_residueClass_eq ha hs, LFunctionResidueClassAux]
rw [neg_div, ← neg_add', mul_neg, ← neg_mul, div_eq_mul_one_div (q.totient : ℂ)⁻¹, sub_eq_add_neg, ← neg_mul, ←
mul_add]
congrm
(_ * ?_)
-- this should be easier, but `IsUnit.inv ha` does not work here
have ha' : IsUnit a⁻¹ := isUnit_of_dvd_one ⟨a, (ZMod.inv_mul_of_unit a ha).symm⟩
classical -- for `Fintype.sum_eq_add_sum_compl`
rw [Fintype.sum_eq_add_sum_compl 1, MulChar.one_apply ha', one_mul, add_right_comm]
simp only [mul_div_assoc]
congrm (?_ + _)
have hs₁ : s ≠ 1 := fun h ↦ ((h ▸ hs).trans_eq one_re).false
rw [deriv_LFunctionTrivChar₁_apply_of_ne_one _ hs₁, LFunctionTrivChar₁, Function.update_of_ne hs₁, LFunctionTrivChar,
add_div, mul_div_mul_left _ _ (sub_ne_zero_of_ne hs₁)]
conv_lhs => enter [2, 1]; rw [← mul_one (LFunction ..)]
rw [mul_comm _ 1, mul_div_mul_right _ _ <| LFunction_ne_zero_of_one_le_re 1 (.inr hs₁) hs.le]
