OAI/NumberTheory/TwoPointCorrelations/MRTGeneralSmallEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The first-small-band energy bound for ordinary multiplicative functions, including the explicit prime-square extraction error.

  1. theorem OAI.TwoPointCorrelations.mrt_general_typical_small_prime_energy line 14

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTGeneralSmallEnergy.lean:14 (same declaration text).