OAI/NumberTheory/TwoPointCorrelations/MRTCoarseBins.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Coarse cofactor windows for a multiplicative prime bin. The weights are the actual Ramaré weights, and moving all primes in a bin to its lower endpoint changes coefficients only in two short boundary strips.

  1. def OAI.TwoPointCorrelations.mrtCoarseRamareWeight line 15

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseBins.lean:15 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.mrtCoarseRamareWeight_nonneg line 20

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseBins.lean:20 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.mrt_coarse_weight_le_one line 26

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

  4. lemma OAI.TwoPointCorrelations.mrt_coarse_window_support line 36

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseBins.lean:36 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.mrt_coarse_window_interior line 45

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

  6. lemma OAI.TwoPointCorrelations.mrt_coarse_weight_zero line 57

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseBins.lean:57 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.mrt_coarse_weight_interior line 74

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseBins.lean:74 (same declaration text).

  8. def OAI.TwoPointCorrelations.mrtCoarseBoundaryCoefficient line 89

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseBins.lean:89 (same declaration text).

  9. lemma OAI.TwoPointCorrelations.mrt_coarse_boundary_abs line 94

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseBins.lean:94 (same declaration text).

  10. theorem OAI.TwoPointCorrelations.mrt_coarse_boundary_support line 104

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCoarseBins.lean:104 (same declaration text).