OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionParameters.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Scalar budgets for the prime-power correction. The real parameter W allows the published logarithmic cutoff, while the actual divisor cutoff is the natural floor of W^5.

  1. def OAI.TwoPointCorrelations.mrtCorrectionCutoff line 13
  2. lemma OAI.TwoPointCorrelations.mrt_correction_fifth_tail line 15
  3. lemma OAI.TwoPointCorrelations.mrt_correction_endpoint line 20
  4. lemma OAI.TwoPointCorrelations.mrt_correction_cutoff_bounds line 35
  5. lemma OAI.TwoPointCorrelations.mrt_correction_cutoff_tail line 48
  6. lemma OAI.TwoPointCorrelations.mrt_correction_cutoff_scale line 66
  7. lemma OAI.TwoPointCorrelations.mrt_correction_quotient_length line 80
  8. lemma OAI.TwoPointCorrelations.mrt_correction_quotient_power line 97