English
The L-series of the von Mangoldt function Λ converges for Re(s) > 1: LSeriesSummable (↗Λ) s when 1 < Re(s).
Русский
Для Re(s) > 1 L-серия по функции Λ сходится: LSeriesSummable (↗Λ) s при 1 < Re(s).
LaTeX
$$$1 < \\operatorname{Re}(s) \\Rightarrow LSeriesSummable(\\uparrow\\Lambda)\\;s$$$
Lean4
/-- The L-series of the von Mangoldt function `Λ` converges at `s` when `re s > 1`. -/
theorem LSeriesSummable_vonMangoldt {s : ℂ} (hs : 1 < s.re) : LSeriesSummable (↗Λ) s :=
by
have hf :=
LSeriesSummable_logMul_of_lt_re (show abscissaOfAbsConv 1 < s.re by rw [abscissaOfAbsConv_one]; exact_mod_cast hs)
rw [LSeriesSummable, ← summable_norm_iff] at hf ⊢
refine hf.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun n ↦ norm_term_le s ?_)
have hΛ : ‖↗Λ n‖ ≤ ‖Complex.log n‖ := by
simpa [abs_of_nonneg, vonMangoldt_nonneg, ← natCast_log, Real.log_natCast_nonneg] using vonMangoldt_le_log
exact hΛ.trans <| by simp
