A squared-logarithmic conductor-height bound for Dirichlet L-derivatives #
The naturally ordered derivative series is cut at the shared cutoff
q * (⌊|t|⌋₊ + 1). Its finite prefix is estimated by a harmonic sum, and in
the Abel tail the factor q / m pays for the full height of the argument.
theorem
DirichletLGlobalConductorLogDerivativeBound.norm_deriv_LFunction_le_sixtyfour_mul_one_add_log_sq_conductorHeightCutoff
{q : ℕ}
[NeZero q]
(χ : DirichletCharacter ℂ q)
(hχ : χ ≠ 1)
{σ t : ℝ}
(hσlower : 1 / 2 ≤ σ)
(hσupper : σ ≤ 2)
(hnear : 1 - 1 / Real.log ↑(DirichletLGlobalConductorLogValueBound.dirichletLConductorHeightCutoff q t) ≤ σ)
:
Near the line re s = 1, the derivative has squared-logarithmic growth in
the conductor-height cutoff, with no positive power of either modulus or height.