OAI/NumberTheory/TwoPointCorrelations/MRTCorrectionEuler.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite-Euler-product criterion for the absolutely summable correction in the general-multiplicative reduction. The criterion is proved from local prime-power sums, not used as a new analytic input.

  1. theorem OAI.TwoPointCorrelations.mrt_summable_of_local_euler_bound line 17

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCorrectionEuler.lean:17 (same declaration text).