OAI/NumberTheory/TwoPoint/Fourier/MajorArcRationalSharp.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Rational short sums with the square-root character loss. The reciprocal gcd volume is retained before summing the strata.

  1. def OAI.TwoPointCorrelations.majorArcDivisorWindow line 14
  2. lemma OAI.TwoPointCorrelations.major_arc_divisor_window line 22
  3. lemma OAI.TwoPointCorrelations.major_arc_divisor_window_average line 36
  4. theorem OAI.TwoPointCorrelations.major_arc_typical_rational_sharp line 78