OAI/NumberTheory/TwoPoint/ShortIntervals/MRTQuotientFinalBand.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A single final band for every quotient dyadic above the square-root cutoff. The band is chosen before the quotient and the dyadic origin.

  1. lemma OAI.TwoPointCorrelations.mrt_quotient_band_target line 12
  2. lemma OAI.TwoPointCorrelations.mrt_quotient_band_alternative line 31
  3. lemma OAI.TwoPointCorrelations.mrt_quotient_dyadic_log line 72
  4. theorem OAI.TwoPointCorrelations.mrt_quotient_common_final_band line 91