OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBinMomentSum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The complete finite witness-bin sum. Both bin cardinalities and the remaining exponential sum are bounded using their actual endpoints.

  1. def OAI.TwoPointCorrelations.mrtLogBins line 13

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTBinMomentSum.lean:13 (same declaration text).

  2. theorem OAI.TwoPointCorrelations.mrt_actual_bin_moment_sum line 16

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTBinMomentSum.lean:16 (same declaration text).