A genuine weak-strip bound for nonprincipal Dirichlet L-values

The naturally ordered conditional value series is split at m = ⌊|t|⌋₊ + 1. Its finite prefix is bounded term by term and its explicit Abel tail is absorbed into one fixed logarithmic bound.

theorem DirichletLWeakStripValueBound.norm_value_truncation_le {q : ℕ} (χ : DirichletCharacter ℂ q) {A σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (hσ : 1 - A / Real.log |t| ≤ σ) (ht : 3 < |t|) : have m := ⌊|t|⌋₊ + 1; ‖∑ n ∈ Finset.range m, DirichletLAbelWeightVariation.cpowWeight (↑σ + ↑t * Complex.I) ↑n * χ ↑n‖ ≤ Real.exp A * 2 * Real.log |t|

The finite value truncation costs only one logarithm in the weak strip.

theorem DirichletLWeakStripValueBound.canonical_value_tail_le_fixed_log {q : ℕ} {A σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (hσ : 1 - A / Real.log |t| ≤ σ) (hσ2 : σ ≤ 2) (ht : 3 < |t|) : have m := ⌊|t|⌋₊ + 1; ↑q * (↑m ^ (-σ) + ‖↑σ + ↑t * Complex.I‖ / σ * ↑m ^ (-σ)) ≤ Real.exp A * (50 * ↑q) * Real.log |t|

At the canonical cutoff the explicit Abel tail is bounded by a fixed multiple of exp A * q * log |t|.

theorem DirichletLWeakStripValueBound.norm_LFunction_le_fixed_log {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) {A σ t : ℝ} (hA : A ∈ Set.Ioc 0 (1 / 2)) (hσ : 1 - A / Real.log |t| ≤ σ) (hσ2 : σ ≤ 2) (ht : 3 < |t|) : ‖DirichletCharacter.LFunction χ (↑σ + ↑t * Complex.I)‖ ≤ Real.exp A * (100 * ↑q) * Real.log |t|

Fully explicit weak-strip value bound for a nonprincipal character.

The principal-character lane

theorem DirichletLWeakStripValueBound.principalEulerFactorNorm_le_prime {s : ℂ} (hs : 0 ≤ s.re) {p : ℕ} (hp : Nat.Prime p) : ‖1 - ↑p ^ (-s)‖ ≤ ↑p

A bad Euler factor is bounded by its underlying prime throughout the closed right half-plane. The nonnegative-real-part version is useful because the zeta zero-free strip extends slightly to the left of re s = 1.

theorem DirichletLWeakStripValueBound.principalEulerCorrectionNorm_le_modulus_of_nonneg_re (q : ℕ) [NeZero q] {s : ℂ} (hs : 0 ≤ s.re) : ‖∏ p ∈ q.primeFactors, (1 - ↑p ^ (-s))‖ ≤ ↑q

The finite Euler correction for the principal character costs at most its modulus. This stronger nonnegative-real-part form covers the zeta strip.

theorem DirichletLWeakStripValueBound.principalEulerCorrectionNorm_le_modulus (q : ℕ) [NeZero q] {s : ℂ} (hs : 1 ≤ s.re) : ‖∏ p ∈ q.primeFactors, (1 - ↑p ^ (-s))‖ ≤ ↑q

Requested re s ≥ 1 specialization of the Euler-correction bound.

theorem DirichletLWeakStripValueBound.exists_principal_norm_LFunctionTrivChar_le_log : ∃ (A : ℝ) (_ : A ∈ Set.Ioc 0 (1 / 2)) (C : ℝ) (_ : 0 < C), ∀ (q : ℕ) [inst : NeZero q] (σ t : ℝ), 3 < |t| → σ ∈ Set.Icc (1 - A / Real.log |t|) 2 → ‖DirichletCharacter.LFunctionTrivChar q (↑σ + ↑t * Complex.I)‖ ≤ C * ↑q * Real.log |t|

Uniform weak-strip logarithmic bound for the principal Dirichlet L-function. The zeta constants are selected before the modulus.