OAI/NumberTheory/TwoPoint/ShortIntervals/MRTAmplification.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Amplification on the multiscale classes where a preceding short-prime polynomial is large. The inserted power is estimated by the actual mixed prime/cofactor moment, not by an assumed large-value proposition.

  1. theorem OAI.TwoPointCorrelations.mrt_amplified_energy line 15

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTAmplification.lean:15 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.mrt_large_prime_class_cofactor_energy line 36

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTAmplification.lean:36 (same declaration text).