OAI/NumberTheory/TwoPoint/ShortIntervals/MRTExtractionErrors.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The prime-square and coarse-bin errors sum independently of the number of MRT bands. The only input is their actual lower endpoints.

  1. lemma OAI.TwoPointCorrelations.mrt_finite_reciprocal_square_tail line 13
  2. lemma OAI.TwoPointCorrelations.mrt_resolution_le_band_lower line 33
  3. lemma OAI.TwoPointCorrelations.mrt_prime_extraction_error line 57
  4. theorem OAI.TwoPointCorrelations.mrt_prime_extraction_error_sum line 71