OAI/NumberTheory/TwoPointCorrelations/MRTBinPrefactor.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Explicit polynomial factors in the later-band estimate are absorbed by a small part of the saving from the true band endpoints.

  1. lemma OAI.TwoPointCorrelations.mrt_log_band_upper_mono line 12

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBinPrefactor.lean:12 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.mrt_bin_prefactor_exponential line 26

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBinPrefactor.lean:26 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.mrt_actual_bin_prefactor line 67

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBinPrefactor.lean:67 (same declaration text).