OAI/NumberTheory/TwoPointCorrelations/MRTGeneralPrimeError.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The general-multiplicative discrepancy in extracting a prime factor. It vanishes unless that prime divides the cofactor, and hence has the same prime-square support as the corrected Ramaré denominator error.

  1. lemma OAI.TwoPointCorrelations.mrtTypicalCoefficient_prime_mul_coprime line 14

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTGeneralPrimeError.lean:14 (same declaration text).

  2. def OAI.TwoPointCorrelations.mrtPrimeProductError line 27

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTGeneralPrimeError.lean:27 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.mrt_prime_product_error_bound line 33

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTGeneralPrimeError.lean:33 (same declaration text).