OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionTypical.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The prime-power correction preserves the literal typical mask on small divisors avoiding the selected bands. The remaining divisors are paid by their absolute reciprocal mass, without removing that mask.

  1. def OAI.TwoPointCorrelations.mrtCorrectionMaskedCofactor line 15
  2. lemma OAI.TwoPointCorrelations.mrt_correction_masked_dilation line 19
  3. lemma OAI.TwoPointCorrelations.mrt_correction_masked_oneBounded line 28
  4. lemma OAI.TwoPointCorrelations.mrt_correction_masked_of_avoids line 37
  5. lemma OAI.TwoPointCorrelations.mrt_correction_typical_finite line 45
  6. theorem OAI.TwoPointCorrelations.mrt_correction_typical_short_sum line 56
  7. lemma OAI.TwoPointCorrelations.mrt_correction_typical_integral_sum line 76
  8. theorem OAI.TwoPointCorrelations.mrt_correction_typical_tail line 97
  9. theorem OAI.TwoPointCorrelations.mrt_correction_typical_tail_below_primes line 158