OAI/NumberTheory/TwoPoint/ShortIntervals/MRTNoSmallOffCenter.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The no-small energy at the literal scale L=log N and outside the neighborhood of an actual minimizing twist. The cofactor estimates follow from off-center cancellation.

  1. def OAI.TwoPointCorrelations.mrtNoSmallOffCenter line 16
  2. lemma OAI.TwoPointCorrelations.mrt_no_small_off_center_measurable line 23
  3. theorem OAI.TwoPointCorrelations.mrt_no_small_off_center_energy_sharp line 30
  4. theorem OAI.TwoPointCorrelations.mrt_no_small_off_center_energy line 102