OAI/NumberTheory/TwoPointCorrelations/MRTFrequencyPartition.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The first-small-band frequency partition. Every later class supplies an actual large polynomial in the preceding band; the exceptional set is exactly the set on which every band has a large polynomial.

  1. def OAI.TwoPointCorrelations.mrtSmallFrequencyBand line 14

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

  2. def OAI.TwoPointCorrelations.mrtFirstSmallBand line 18

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFrequencyPartition.lean:18 (same declaration text).

  3. def OAI.TwoPointCorrelations.mrtNoSmallBand line 22

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

  4. lemma OAI.TwoPointCorrelations.mrt_small_frequency_band_measurable line 26

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFrequencyPartition.lean:26 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.mrt_first_small_band_measurable line 38

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

  6. lemma OAI.TwoPointCorrelations.mrt_no_small_band_measurable line 46

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFrequencyPartition.lean:46 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.mrt_first_small_band_disjoint line 53

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFrequencyPartition.lean:53 (same declaration text).

  8. theorem OAI.TwoPointCorrelations.mrt_frequency_partition line 62

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFrequencyPartition.lean:62 (same declaration text).

  9. theorem OAI.TwoPointCorrelations.mrt_later_band_large_witness line 92

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFrequencyPartition.lean:92 (same declaration text).

  10. theorem OAI.TwoPointCorrelations.mrt_no_small_band_large_witness line 103

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFrequencyPartition.lean:103 (same declaration text).

  11. theorem OAI.TwoPointCorrelations.mrt_frequency_partition_integral line 113

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFrequencyPartition.lean:113 (same declaration text).