OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLogClassBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds for the actual first-small logarithmic classes. The first-band cost occurs once; the later costs form an inverse-square sum.

  1. def OAI.TwoPointCorrelations.mrtLogExtractionError line 14
  2. theorem OAI.TwoPointCorrelations.mrt_log_class_energy line 19