OAI/NumberTheory/TwoPointCorrelations/MRTGeometricBins.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exponential sum over the first MRT prime band. Its constant is independent of the number of coarse bins.

  1. lemma OAI.TwoPointCorrelations.mrt_exp_geometric_sum line 14

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

  2. lemma OAI.TwoPointCorrelations.mrt_geometric_denominator_bound line 34

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTGeometricBins.lean:34 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.mrt_first_band_exponential_sum line 51

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTGeometricBins.lean:51 (same declaration text).