OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFirstResolution.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The first-band logarithmic resolution absorbs the explicit kernel costs for the fixed lower endpoint used in the MRT application.

  1. lemma OAI.TwoPointCorrelations.mrt_first_resolution_lower line 13
  2. lemma OAI.TwoPointCorrelations.mrt_first_kernel_error line 29
  3. theorem OAI.TwoPointCorrelations.mrt_first_kernel_error_eventually line 59