OAI/NumberTheory/TwoPoint/Fourier/MajorArcPerturbedSharp.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Preserve the square-root modulus loss through partial summation. The estimates for shorter intervals remain explicit.

  1. theorem OAI.TwoPointCorrelations.major_arc_typical_perturbed_sharp line 12
  2. lemma OAI.TwoPointCorrelations.major_arc_twist_complete line 33
  3. lemma OAI.TwoPointCorrelations.major_arc_divisor_distance line 41