OAI/NumberTheory/TwoPoint/ShortIntervals/MRTShortSubdivisionSharp.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Subdivision with the exact common outer cutoff. The last complete block starts no later than H-h, so its short window stays below X+H.

  1. lemma OAI.TwoPointCorrelations.mrt_subdivision_shift_le line 13
  2. theorem OAI.TwoPointCorrelations.mrt_short_integral_subdivision_sharp line 21
  3. theorem OAI.TwoPointCorrelations.mrt_arc_subdivision_integral_sharp line 56