OAI/NumberTheory/TwoPoint/Fourier/MajorArcPerturbation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A finite partial-summation form of the major-arc frequency perturbation. The error uses the actual shorter windows before averaging the origin; no frequency supremum is moved inside an integral.

  1. lemma OAI.TwoPointCorrelations.major_arc_abel_bound line 16
  2. lemma OAI.TwoPointCorrelations.major_arc_character_step line 38
  3. lemma OAI.TwoPointCorrelations.major_arc_frequency_perturbation line 57
  4. theorem OAI.TwoPointCorrelations.major_arc_integral_perturbation line 75
  5. lemma OAI.TwoPointCorrelations.major_arc_integral_perturbation_uniform line 86