OAI/NumberTheory/TwoPoint/ShortIntervals/MRTNoSmallCoarse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Complete additional-prime coarse-polynomial energy on the actual no-small class. The prime sparse theorem and the pointwise cofactor saving are explicit; all sample counts, set splits and bin sums are discharged.

  1. theorem OAI.TwoPointCorrelations.mrt_no_small_coarse_energy line 16