OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMovingStripNorm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The shrinking-disk estimate inside a narrower zero-free strip. This extension to the left of one is used for the smoothed Mangoldt contour.

  1. theorem OAI.TwoPointCorrelations.mrt_moving_strip_logderiv line 13