OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMixedThreshold.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The factorial and support growth in the amplified cofactor moment are paid from half of the gap between successive prime thresholds.

  1. def OAI.TwoPointCorrelations.mrtAmplificationCost line 10

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

  2. lemma OAI.TwoPointCorrelations.mrt_mixed_threshold_exponent line 14

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

  3. theorem OAI.TwoPointCorrelations.mrt_mixed_threshold_bound line 33

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMixedThreshold.lean:33 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.mrt_amplification_cost_bound line 87

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMixedThreshold.lean:87 (same declaration text).

  5. theorem OAI.TwoPointCorrelations.mrt_mixed_threshold_amplification line 102

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTMixedThreshold.lean:102 (same declaration text).