OAI/NumberTheory/TwoPoint/ShortIntervals/MRTNoSmallCard.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual final original band gives the cardinality needed by the integer-kernel estimate on every separated subset of the no-small class.

  1. theorem OAI.TwoPointCorrelations.mrt_no_small_card_at_scale line 15