OAI/NumberTheory/TwoPointCorrelations/MRTFrequencyCover.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Refinement of a later frequency class by its actual preceding-bin large-value witnesses. The witnesses may overlap; the finite sum charges each preceding bin explicitly.

  1. lemma OAI.TwoPointCorrelations.mrt_nonnegative_integral_cover line 14

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFrequencyCover.lean:14 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.mrt_later_band_integral_cover line 41

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFrequencyCover.lean:41 (same declaration text).