OAI/NumberTheory/TwoPoint/ShortIntervals/MRTLaterBinSum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The later frequency classes have a summable bound, with the true resolution and all witness-bin choices included.

  1. lemma OAI.TwoPointCorrelations.mrt_later_bin_prefactor_saving line 12

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTLaterBinSum.lean:12 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.mrt_later_bin_moment_sum line 66

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTLaterBinSum.lean:66 (same declaration text).