OAI/NumberTheory/TwoPointCorrelations/MRTFactoredReciprocal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Finite reciprocal mass of integers supported on a prime band. Together with the gcd-triple injection this supplies the divisor-square mean bound in MR's mixed prime/cofactor moment without an additional sieve input.

  1. def OAI.TwoPointCorrelations.mrtFactoredUpTo line 16

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFactoredReciprocal.lean:16 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.mrtFactoredUpTo_pos line 19

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFactoredReciprocal.lean:19 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.mrtFactoredUpTo_divisor_closed line 23

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFactoredReciprocal.lean:23 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.mrt_reciprocal_prime_power_series line 31

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFactoredReciprocal.lean:31 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.mrt_reciprocal_prime_power_norm line 38

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFactoredReciprocal.lean:38 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.mrt_factored_reciprocal_series line 44

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFactoredReciprocal.lean:44 (same declaration text).

  7. theorem OAI.TwoPointCorrelations.mrt_factored_reciprocal_sum line 63

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFactoredReciprocal.lean:63 (same declaration text).

  8. theorem OAI.TwoPointCorrelations.mrt_factored_divisor_second_moment line 81

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFactoredReciprocal.lean:81 (same declaration text).

  9. lemma OAI.TwoPointCorrelations.mrt_prime_reciprocal_euler_bound line 93

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFactoredReciprocal.lean:93 (same declaration text).

  10. theorem OAI.TwoPointCorrelations.mrt_factored_divisor_exponential_moment line 110

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTFactoredReciprocal.lean:110 (same declaration text).