OAI/NumberTheory/TwoPoint/ShortIntervals/MRTZetaRectangle.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The pole-corrected zeta logarithmic derivative on the entire sparse Perron rectangle, including bounded heights and points left of one.

  1. theorem OAI.TwoPointCorrelations.MRTWeakHurwitzGrowthInput.zeta_sparse_rectangle line 15