English
The logarithms of Euler factors form a summable sequence; more precisely, the series of -log(1−χ(p) p^(-s)) over primes converges for Re(s) > 1 when χ is a Dirichlet character with χ^2 = 1.
Русский
Логарифмы факторов Эйлера образуют суммируемую последовательность; ряд -log(1−χ(p) p^(-s)) по простым сходится при Re(s) > 1 для χ^2=1.
LaTeX
$$$\text{Summable}\; p:\mathrm{Primes} \mapsto -\log\bigl(1 - χ(p) p^{-s}\bigr)$$$
Lean4
/-- The logarithms of the Euler factors of a Dirichlet L-series form a summable sequence. -/
theorem summable_neg_log_one_sub_mul_prime_cpow {s : ℂ} (hs : 1 < s.re) :
Summable fun p : Nat.Primes ↦ -log (1 - χ p * (p : ℂ) ^ (-s)) :=
by
have (p : Nat.Primes) : ‖χ p * (p : ℂ) ^ (-s)‖ ≤ (p : ℝ) ^ (-s).re := by
simpa only [norm_mul, norm_natCast_cpow_of_re_ne_zero _ <| re_neg_ne_zero_of_one_lt_re hs] using
mul_le_of_le_one_left (by positivity) (χ.norm_le_one _)
refine (Nat.Primes.summable_rpow.mpr ?_).of_nonneg_of_le (fun _ ↦ norm_nonneg _) this |>.of_norm.clog_one_sub.neg
simp only [neg_re, neg_lt_neg_iff, hs]
