OAI/NumberTheory/TwoPoint/ShortIntervals/MRTNoSmallFull.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Full actual no-small energy under a uniform cofactor estimate. Unlike the off-center specialization, this statement has no high-prime input and no minimizing-twist hypothesis.

  1. def OAI.TwoPointCorrelations.mrtActualNoSmall line 14
  2. lemma OAI.TwoPointCorrelations.mrt_actual_no_small_measurable line 20
  3. lemma OAI.TwoPointCorrelations.mrt_no_small_off_center_eq line 25
  4. lemma OAI.TwoPointCorrelations.mrt_actual_bands_bounded line 29
  5. theorem OAI.TwoPointCorrelations.mrt_no_small_full_energy_sharp line 41
  6. theorem OAI.TwoPointCorrelations.mrt_no_small_full_energy line 105