OAI/NumberTheory/TwoPoint/ShortIntervals/MRTShortEuler.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

An absolute Euler-factor bound on one short prime bin. Counting all integers in the bin already suffices, so this local mixed-moment constant requires no additional prime-distribution theorem.

  1. lemma OAI.TwoPointCorrelations.mrt_short_bin_reciprocal_mass line 14

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTShortEuler.lean:14 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.mrt_short_bin_reciprocal_square_mass line 30

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTShortEuler.lean:30 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.mrt_short_bin_euler_cube line 47

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTShortEuler.lean:47 (same declaration text).