OAI/NumberTheory/TwoPoint/ShortIntervals/MRTExtraSmallIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Small additional-prime values on the actual no-small class. The integer-kernel error is paid by the final original-band sample count.

  1. lemma OAI.TwoPointCorrelations.mrt_small_cofactor_integral line 14
  2. theorem OAI.TwoPointCorrelations.mrt_extra_small_integral line 46