OAI/NumberTheory/TwoPointCorrelations/MRTBandParameters.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The explicit prime-band endpoints from MRT, Definition 2.1.

  1. def OAI.TwoPointCorrelations.mrtBandLower line 13

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandParameters.lean:13 (same declaration text).

  2. def OAI.TwoPointCorrelations.mrtBandUpper line 16

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandParameters.lean:16 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.mrtBandLower_one line 19

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandParameters.lean:19 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.mrtBandUpper_one line 22

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandParameters.lean:22 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.mrt_band_log_ratio line 25

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandParameters.lean:25 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.mrt_band_endpoints line 38

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandParameters.lean:38 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.mrt_band_index_le_log_upper line 68

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandParameters.lean:68 (same declaration text).

  8. lemma OAI.TwoPointCorrelations.mrt_band_ratio_sum line 79

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandParameters.lean:79 (same declaration text).