Sharp conductor-logarithmic nonquadratic logarithmic derivative bound #
The product argument is retained quantitatively: first it gives a lower bound for the L-value throughout a narrower strip, and that lower bound is then divided into the sharp derivative estimate. No positive power of the modulus or height occurs.
theorem
AnalyticNumberTheory.LargeSieve.norm_LFunction_lower_of_nonquadratic_conductorLog
{q : ℕ}
[NeZero q]
(χ : DirichletCharacter ℂ q)
(hχsq : χ ^ 2 ≠ 1)
{β t : ℝ}
(hβ :
β ∈ Set.Ico
(1 - 1 / (4398046511104 * (1 + Real.log ↑(DirichletLGlobalConductorLogValueBound.dirichletLConductorHeightCutoff q t)) ^ 9))
1)
:
Quantitative nonquadratic lower bound in the sharp conductor-log strip.
Inspect dependencies
AnalyticNumberTheory.LargeSieve.norm_LFunction_lower_of_nonquadratic_conductorLog · compiled type and proof/definition references.
theorem
AnalyticNumberTheory.LargeSieve.norm_logDeriv_LFunction_le_of_nonquadratic_conductorLog
{q : ℕ}
[NeZero q]
(χ : DirichletCharacter ℂ q)
(hχsq : χ ^ 2 ≠ 1)
{β t : ℝ}
(hβ :
β ∈ Set.Ico
(1 - 1 / (4398046511104 * (1 + Real.log ↑(DirichletLGlobalConductorLogValueBound.dirichletLConductorHeightCutoff q t)) ^ 9))
1)
:
The sharp logarithmic derivative bound, obtained by dividing the derivative estimate by the quantitative L-value lower bound above.
Inspect dependencies
AnalyticNumberTheory.LargeSieve.norm_logDeriv_LFunction_le_of_nonquadratic_conductorLog · compiled type and proof/definition references.