OAI/NumberTheory/TwoPoint/Fourier/MajorArcWorkingBand.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Prime-band costs for the fifth-root working length. Both density and the minor-arc fourth root have the same elementary rate.

  1. lemma OAI.TwoPointCorrelations.major_arc_working_log_lower line 12
  2. lemma OAI.TwoPointCorrelations.major_arc_working_upper_log line 29
  3. lemma OAI.TwoPointCorrelations.major_arc_working_band_density line 49
  4. lemma OAI.TwoPointCorrelations.major_arc_minor_working_rate line 73
  5. lemma OAI.TwoPointCorrelations.major_arc_working_band_budget line 91
  6. lemma OAI.TwoPointCorrelations.major_arc_working_band_resolution line 104