OAI/NumberTheory/TwoPointCorrelations/MRTBandSeparation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual MRT bands are disjoint, as required by the corrected Ramaré decomposition; no disjointness hypothesis on those bands remains.

  1. lemma OAI.TwoPointCorrelations.mrt_adjacent_band_gap line 14

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandSeparation.lean:14 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.mrt_band_lower_monotone line 30

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandSeparation.lean:30 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.mrt_band_gap line 39

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandSeparation.lean:39 (same declaration text).

  4. theorem OAI.TwoPointCorrelations.mrt_actual_bands_pairwise_disjoint line 45

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandSeparation.lean:45 (same declaration text).