OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalFactors.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.mrtPrimeAvoids line 15

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalFactors.lean:15 (same declaration text).

2. def OAI.TwoPointCorrelations.mrtPrimeMask line 17

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalFactors.lean:17 (same declaration text).

3. def OAI.TwoPointCorrelations.mrtTypical line 20

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalFactors.lean:20 (same declaration text).

4. lemma OAI.TwoPointCorrelations.mrtPrimeMask_bounds line 23

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalFactors.lean:23 (same declaration text).

5. lemma OAI.TwoPointCorrelations.mrtPrimeAvoids_union line 28

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalFactors.lean:28 (same declaration text).

6. lemma OAI.TwoPointCorrelations.mrtPrimeMask_union line 33

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalFactors.lean:33 (same declaration text).

7. lemma OAI.TwoPointCorrelations.mrtPrimeAvoids_mul line 38

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalFactors.lean:38 (same declaration text).

8. lemma OAI.TwoPointCorrelations.mrtPrimeMask_mul line 48

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalFactors.lean:48 (same declaration text).

9. lemma OAI.TwoPointCorrelations.mrtPrimeMask_one line 53

   Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalFactors.lean:53 (same declaration text).

10. lemma OAI.TwoPointCorrelations.mrtPrimeMask_prime line 60

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalFactors.lean:60 (same declaration text).

11. lemma OAI.TwoPointCorrelations.mrtPrimeMask_biUnion line 72

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalFactors.lean:72 (same declaration text).

12. lemma OAI.TwoPointCorrelations.mrtTypical_prod line 79

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalFactors.lean:79 (same declaration text).

13. theorem OAI.TwoPointCorrelations.mrtTypical_inclusion_exclusion line 96

    Source documentation

    Exact inclusion-exclusion over missing prime bands, the expansion in MRT Appendix A before its near-twist mean-value estimate.

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalFactors.lean:96 (same declaration text).

    theorem mrtTypical_inclusion_exclusion {ι : Type*} (J : Finset ι)
        (P : ι → Finset ℕ) (n : ℕ) :
        (∑ I ∈ J.powerset, (-1 : ℝ) ^ I.card * mrtPrimeMask (I.biUnion P) n) =
          if mrtTypical J P n then 1 else 0 := by
    …

    Mentions: OAI.TwoPointCorrelations.mrtPrimeMask, OAI.TwoPointCorrelations.mrtTypical

14. lemma OAI.TwoPointCorrelations.mrtPrimeAvoids_of_lt line 105

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalFactors.lean:105 (same declaration text).

15. theorem OAI.TwoPointCorrelations.mrtTypical_mul_of_avoids line 112

    Source documentation

    Dividing out a number smaller than all the selected primes does not change membership in the typical-factorization set.

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalFactors.lean:112 (same declaration text).

    theorem mrtTypical_mul_of_avoids {ι : Type*} (J : Finset ι) (P : ι → Finset ℕ)
        (hP : ∀ j ∈ J, ∀ p ∈ P j, p.Prime) {d : ℕ}
        (hd : mrtPrimeAvoids (J.biUnion P) d) (n : ℕ) :
        mrtTypical J P (d * n) ↔ mrtTypical J P n := by
    …

    Mentions: OAI.TwoPointCorrelations.mrtPrimeAvoids, OAI.TwoPointCorrelations.mrtTypical

16. lemma OAI.TwoPointCorrelations.mrtPrimeMask_complex_oneBounded line 126

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalFactors.lean:126 (same declaration text).

17. lemma OAI.TwoPointCorrelations.mrtPrimeMask_complex_multiplicative line 132

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalFactors.lean:132 (same declaration text).