theorem DirichletCharacter.prod_one_add_inv_primeFactors_le_one_add_log (q : ℕ) (hq : 1 ≤ q) : ∏ p ∈ q.primeFactors, (1 + (↑p)⁻¹) ≤ 1 + Real.log ↑q

Expanding the squarefree Euler product injects its terms into the harmonic sum. In particular this also handles q = 1, when both products are empty.

theorem DirichletCharacter.principalEulerFactorNorm_le_one_add_inv {s : ℂ} (hs : 1 ≤ s.re) {p : ℕ} (hp : Nat.Prime p) : ‖1 - ↑p ^ (-s)‖ ≤ 1 + (↑p)⁻¹

On re s ≥ 1, each omitted Euler factor has norm at most 1 + 1/p.

theorem DirichletCharacter.principalEulerCorrectionNorm_le_one_add_log (q : ℕ) (hq : 1 ≤ q) {s : ℂ} (hs : 1 ≤ s.re) : ‖∏ p ∈ q.primeFactors, (1 - ↑p ^ (-s))‖ ≤ 1 + Real.log ↑q

The principal-character Euler correction has only logarithmic modulus cost.

theorem DirichletCharacter.norm_LFunctionTrivChar_le_one_add_log_mul_riemannZeta (q : ℕ) [NeZero q] {s : ℂ} (hs : 1 ≤ s.re) (hsne : s ≠ 1) : ‖LFunctionTrivChar q s‖ ≤ (1 + Real.log ↑q) * ‖riemannZeta s‖

A logarithmic-modulus bound for the principal Dirichlet L-function in the closed half-plane re s ≥ 1, away from the zeta pole.

theorem DirichletCharacter.norm_LFunction_sq_le_one_add_log_mul_riemannZeta {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hquad : χ ^ 2 = 1) {s : ℂ} (hs : 1 ≤ s.re) (hsne : s ≠ 1) : ‖LFunction (χ ^ 2) s‖ ≤ (1 + Real.log ↑q) * ‖riemannZeta s‖

If a character squares to the trivial character, the same logarithmic bound applies to the L-function of its square.