English
The L-function associated to the trivial Dirichlet character modulo N has a simple pole at s = 1 with residue equal to the Euler product ∏_{p ∈ primeFactors(N)} (1 - p^{−1}).
Русский
L-функция тривиального символа по модулю N имеет простой полюс в s = 1, residuum равен ∏_{p|N} (1 - p^{−1}).
LaTeX
$$$\operatorname{Res}_{s=1} L(\text{triv mod }N, s) = \prod_{p \mid N} (1 - p^{-1})$$$
Lean4
/-- The L function of the trivial Dirichlet character mod `N` has a simple pole with
residue `∏ p ∈ N.primeFactors, (1 - p⁻¹)` at `s = 1`. -/
theorem LFunctionTrivChar_residue_one :
Tendsto (fun s ↦ (s - 1) * LFunctionTrivChar N s) (𝓝[≠] 1) (𝓝 <| ∏ p ∈ N.primeFactors, (1 - (p : ℂ)⁻¹)) :=
by
have H :
(fun s ↦ (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s ↦
(∏ p ∈ N.primeFactors, (1 - (p : ℂ) ^ (-s))) * ((s - 1) * riemannZeta s) :=
by
refine Set.EqOn.eventuallyEq_nhdsWithin fun s hs ↦ ?_
rw [mul_left_comm, LFunctionTrivChar_eq_mul_riemannZeta hs]
rw [tendsto_congr' H]
conv => enter [3, 1]; rw [← mul_one <| Finset.prod ..]; enter [1, 2, p]; rw [← cpow_neg_one]
refine .mul (f := fun s ↦ ∏ p ∈ N.primeFactors, _) ?_ riemannZeta_residue_one
refine tendsto_nhdsWithin_of_tendsto_nhds <| Continuous.tendsto ?_ 1
exact
continuous_finset_prod _ fun p hp ↦
by
have : NeZero p := ⟨(Nat.prime_of_mem_primeFactors hp).ne_zero⟩
fun_prop
