OAI/NumberTheory/TwoPoint/ShortIntervals/MRTArcRate.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Scalar rates for a square-root modulus loss and the elementary q^(1/100) divisor bound. These estimates do not assume or prove the analytic character-resolution inequality.

  1. lemma OAI.TwoPointCorrelations.mrt_sqrt_modulus_power line 13
  2. theorem OAI.TwoPointCorrelations.mrt_sqrt_modulus_log_saving line 18
  3. lemma OAI.TwoPointCorrelations.mrt_arc_outer_quarter line 54
  4. lemma OAI.TwoPointCorrelations.mrt_arc_short_quarter line 60
  5. lemma OAI.TwoPointCorrelations.mrt_arc_exp_quarter line 72
  6. lemma OAI.TwoPointCorrelations.mrt_arc_exp_modulus line 78
  7. def OAI.TwoPointCorrelations.mrtArcParameter line 91
  8. lemma OAI.TwoPointCorrelations.mrt_min_rpow_le_sum line 94
  9. lemma OAI.TwoPointCorrelations.mrt_arc_parameter_bounds line 102
  10. lemma OAI.TwoPointCorrelations.mrt_arc_parameter_quarter line 115