OAI/NumberTheory/TwoPoint/ShortIntervals/MRTArcOuterScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform outer logarithms at the final modulus exponent. The proof keeps the actual floor quotient and allows the combined divisor W^6.

  1. lemma OAI.TwoPointCorrelations.mrt_polylog_quotient_logs line 12
  2. theorem OAI.TwoPointCorrelations.mrt_arc_quotient_outer_logs_sharp line 41