OAI/NumberTheory/TwoPoint/ShortIntervals/MRTNoSmallCount.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The optimized moment applied to every actual logarithmic bin in the last-band witness cover. No abstract covering family is assumed.

  1. theorem OAI.TwoPointCorrelations.mrt_no_small_final_samples line 13