OAI/NumberTheory/TwoPoint/ShortIntervals/MRTWeakVKDerivative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform high-height logarithmic-derivative consequence of the explicit weak Hurwitz growth input. The polynomial modulus loss has disappeared: only log q occurs in the final bound.

  1. theorem OAI.TwoPointCorrelations.MRTWeakHurwitzGrowthInput.logderiv line 16