OAI/NumberTheory/TwoPoint/ShortIntervals/MRTRealPrimeBins.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Real short-prime bins, as used in the Ramaré decomposition, fit the integer endpoint mixed-moment theorem without moving any prime.

  1. lemma OAI.TwoPointCorrelations.mrt_real_prime_bin_subset line 13

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

  2. lemma OAI.TwoPointCorrelations.mrt_real_prime_bin_ceil line 22

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRealPrimeBins.lean:22 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.mrt_real_short_class_cofactor_energy line 35

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTRealPrimeBins.lean:35 (same declaration text).