OAI/NumberTheory/TwoPointCorrelations/MRTBandLogGrowth.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform scalar growth estimates for the actual MRT band endpoints. They will discharge the mixed-moment factorial budget for every band.

  1. lemma OAI.TwoPointCorrelations.mrt_log_log_band_upper line 11

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandLogGrowth.lean:11 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.mrt_log_band_lower_fourth line 31

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandLogGrowth.lean:31 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.mrt_band_adjacent_log_product line 42

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandLogGrowth.lean:42 (same declaration text).

  4. theorem OAI.TwoPointCorrelations.mrt_band_factorial_separation line 60

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandLogGrowth.lean:60 (same declaration text).

  5. theorem OAI.TwoPointCorrelations.mrt_band_support_separation line 89

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandLogGrowth.lean:89 (same declaration text).