English
The L-function has a residue at s = 1 equal to the average value of Φ, i.e., (1/N) ∑_j Φ(j).
Русский
Резиду Л-функции в точке s = 1 равна среднему значению Φ: (1/N) ∑_j Φ(j).
LaTeX
$$$$\operatorname{Res}_{s=1} L(\Phi, s) = \frac{1}{N} \sum_{j} \Phi(j).$$$$
Lean4
/-- The L-function of `Φ` has a residue at `s = 1` equal to the average value of `Φ`. -/
theorem LFunction_residue_one (Φ : ZMod N → ℂ) :
Tendsto (fun s ↦ (s - 1) * LFunction Φ s) (𝓝[≠] 1) (𝓝 (∑ j, Φ j / N)) :=
by
simp only [LFunction, mul_sum]
refine tendsto_finset_sum _ fun j _ ↦ ?_
rw [(by ring : Φ j / N = Φ j * (1 / N * 1)), one_div, ← cpow_neg_one]
simp only [show ∀ a b c d : ℂ, a * (b * (c * d)) = c * (b * (a * d)) by intros; ring]
refine tendsto_const_nhds.mul (.mul ?_ <| hurwitzZeta_residue_one _)
exact ((continuous_neg.const_cpow (Or.inl <| NeZero.ne _)).tendsto _).mono_left nhdsWithin_le_nhds
