OAI/NumberTheory/TwoPoint/ShortIntervals/MRTAmplificationPower.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The explicit amplification order used between two successive MRT prime scales. The integer ceiling satisfies the exact support inequalities needed by the mixed cofactor moment.

  1. def OAI.TwoPointCorrelations.mrtAmplificationOrder line 14

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTAmplificationPower.lean:14 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.mrt_nat_pow_eq_exp line 17

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTAmplificationPower.lean:17 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.mrt_amplification_order_bounds line 23

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTAmplificationPower.lean:23 (same declaration text).

  4. theorem OAI.TwoPointCorrelations.mrt_short_class_cofactor_energy_chosen line 53

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTAmplificationPower.lean:53 (same declaration text).