OAI/NumberTheory/TwoPoint/Fourier/MajorArcWorkingLength.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A fifth-root logarithmic cap, obtained from the general square-root cap by substitution. Its size suits the common Diophantine parameter.

  1. def OAI.TwoPointCorrelations.majorArcWorkingLength line 12
  2. lemma OAI.TwoPointCorrelations.major_arc_working_root line 15
  3. lemma OAI.TwoPointCorrelations.major_arc_working_length_le line 20
  4. lemma OAI.TwoPointCorrelations.major_arc_working_length_loglog line 23
  5. lemma OAI.TwoPointCorrelations.major_arc_working_length_exp_upper line 31
  6. theorem OAI.TwoPointCorrelations.major_arc_working_length_power line 36
  7. theorem OAI.TwoPointCorrelations.major_arc_working_length_remainder line 56
  8. theorem OAI.TwoPointCorrelations.major_arc_working_cap_log line 86