OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterStripBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual logarithmic derivative is bounded by an absolute constant times log(q*(abs(t)+2))^2 on a narrower classical high-height strip.

  1. lemma OAI.TwoPointCorrelations.mrt_character_log_height_ge_half line 13
  2. theorem OAI.TwoPointCorrelations.mrt_character_logderiv_strip_bound line 22