OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFirstClassEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The first frequency-class estimate for actual logarithmic prime bins. Prime membership, bin width, and the complete scalar sum are derived here.

  1. theorem OAI.TwoPointCorrelations.mrt_first_log_class_energy line 13