Weak-strip difference bounds for Dirichlet L-functions

This module integrates the continued derivative along a horizontal segment and then applies the pointwise weak-strip derivative estimate at every point of the integration path.

theorem DirichletLWeakStripDifferenceBound.integral_deriv_LFunction_eq_sub {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1) (σ₁ σ₂ t : ℝ) : ∫ (σ : ℝ) in σ₁..σ₂, deriv (DirichletCharacter.LFunction χ) (↑σ + ↑t * Complex.I) = DirichletCharacter.LFunction χ (↑σ₂ + ↑t * Complex.I) - DirichletCharacter.LFunction χ (↑σ₁ + ↑t * Complex.I)

The horizontal integral of the derivative of a nonprincipal Dirichlet L-function is the difference of its endpoint values.

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

Integrating the pointwise derivative estimate gives a Lipschitz bound along any horizontal segment contained in the requested weak strip.