OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMixedScale.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Explicit sufficient logarithmic scale separations for the amplified moment. The factorial budget is derived, rather than assumed.

  1. lemma OAI.TwoPointCorrelations.mrt_amplification_cost_coarse line 10

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMixedScale.lean:10 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.mrt_mixed_scale_guard line 35

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMixedScale.lean:35 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.mrt_amplification_cost_of_separation line 46

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMixedScale.lean:46 (same declaration text).

  4. theorem OAI.TwoPointCorrelations.mrt_mixed_threshold_of_separation line 62

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMixedScale.lean:62 (same declaration text).