MRTTypicalFactors.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Exact finite typical-factorization masks used by MRT. The prime bands are kept arbitrary here; scale and sieve bounds are separate analytic steps.

def OAI.TwoPointCorrelations.mrtPrimeAvoids line 15
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalFactors.lean:15 (same declaration text).
def OAI.TwoPointCorrelations.mrtPrimeMask line 17
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalFactors.lean:17 (same declaration text).
def OAI.TwoPointCorrelations.mrtTypical line 20
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalFactors.lean:20 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtPrimeMask_bounds line 23
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalFactors.lean:23 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtPrimeAvoids_union line 28
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalFactors.lean:28 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtPrimeMask_union line 33
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalFactors.lean:33 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtPrimeAvoids_mul line 38
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalFactors.lean:38 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtPrimeMask_mul line 48
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalFactors.lean:48 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtPrimeMask_one line 53
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalFactors.lean:53 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtPrimeMask_prime line 60
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalFactors.lean:60 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtPrimeMask_biUnion line 72
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalFactors.lean:72 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtTypical_prod line 79
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalFactors.lean:79 (same declaration text).
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/TwoPoint/ShortIntervals/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
lemma OAI.TwoPointCorrelations.mrtPrimeAvoids_of_lt line 105
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalFactors.lean:105 (same declaration text).
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/TwoPoint/ShortIntervals/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
lemma OAI.TwoPointCorrelations.mrtPrimeMask_complex_oneBounded line 126
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalFactors.lean:126 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtPrimeMask_complex_multiplicative line 132
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTTypicalFactors.lean:132 (same declaration text).