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 : ℝ)
:
The horizontal integral of the derivative of a nonprincipal Dirichlet L-function is the difference of its endpoint values.
Inspect dependencies
DirichletLWeakStripDifferenceBound.integral_deriv_LFunction_eq_sub · compiled type and proof/definition references.
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)
:
Integrating the pointwise derivative estimate gives a Lipschitz bound along any horizontal segment contained in the requested weak strip.
Inspect dependencies
DirichletLWeakStripDifferenceBound.norm_LFunction_sub_le_fixed_log_sq_mul · compiled type and proof/definition references.