OAI/NumberTheory/TwoPoint/ShortIntervals/MRTArcSubdivision.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Subdivide before applying the major-arc perturbation estimate. The chosen length keeps the phase variation bounded and still satisfies the lower length required by the small-divisor correction.

  1. def OAI.TwoPointCorrelations.mrtArcSubdivisionLength line 12
  2. lemma OAI.TwoPointCorrelations.mrt_arc_subdivision_bounds line 14
  3. lemma OAI.TwoPointCorrelations.mrt_arc_subdivision_remainder line 42
  4. lemma OAI.TwoPointCorrelations.mrt_arc_subdivision_phase line 53
  5. theorem OAI.TwoPointCorrelations.mrt_arc_subdivision_integral line 66