OAI/NumberTheory/TwoPoint/Fourier/MajorArcPublishedRate.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The common major/minor-arc parameter and its quantitative rates. The fifth-root working length retains the published logarithmic error.

  1. def OAI.TwoPointCorrelations.majorArcParameter line 12
  2. lemma OAI.TwoPointCorrelations.major_arc_parameter_bounds line 15
  3. def OAI.TwoPointCorrelations.majorArcWorkingError line 26
  4. lemma OAI.TwoPointCorrelations.major_arc_working_short line 29
  5. lemma OAI.TwoPointCorrelations.major_arc_working_exponential line 43
  6. lemma OAI.TwoPointCorrelations.major_arc_working_outer line 59
  7. lemma OAI.TwoPointCorrelations.major_arc_working_min line 81
  8. lemma OAI.TwoPointCorrelations.major_arc_parameter_rate line 93
  9. theorem OAI.TwoPointCorrelations.major_arc_sharp_energy_rate line 108
  10. lemma OAI.TwoPointCorrelations.major_arc_sharp_distance_rate line 143
  11. lemma OAI.TwoPointCorrelations.major_arc_inverse_working_rate line 164
  12. theorem OAI.TwoPointCorrelations.major_arc_weighted_energy_rate line 177