OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBandEuler.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exact finite Euler-product bounds for inclusion-exclusion over prime bands. Each nonempty-band factor pays a square root of its Euler product, with only the summable prime-square error remaining.

  1. lemma OAI.TwoPointCorrelations.mrt_local_euler_log_bound line 14
  2. lemma OAI.TwoPointCorrelations.mrt_exp_sub_one_bound line 33
  3. lemma OAI.TwoPointCorrelations.mrt_euler_block_exp line 47
  4. theorem OAI.TwoPointCorrelations.mrt_euler_block_difference_bound line 62