OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterGlobalBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An all-height logarithmic derivative bound with explicit polynomial modulus loss. The stronger high-height result remains available separately.

  1. theorem OAI.TwoPointCorrelations.mrt_character_logderiv_global_bound line 14