OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionShortWindow.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact short-window convolution and the uniform large-divisor tail in the reduction to completely multiplicative functions.

  1. lemma OAI.TwoPointCorrelations.mrt_correction_finite_sum line 14
  2. lemma OAI.TwoPointCorrelations.mrt_correction_short_sum_fixed line 33
  3. theorem OAI.TwoPointCorrelations.mrt_correction_short_sum line 51
  4. lemma OAI.TwoPointCorrelations.mrt_dilation_prefix_count line 61
  5. lemma OAI.TwoPointCorrelations.mrt_dilation_short_integral line 96
  6. lemma OAI.TwoPointCorrelations.mrt_correction_integral_sum line 113
  7. theorem OAI.TwoPointCorrelations.mrt_correction_short_integral_tail line 131