MRTCountMask.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Reciprocal prime-count weights as an integral of multiplicative soft masks. This is the exact cofactor-weight reduction used in MRT Appendix A, Lemma A.5.

def OAI.TwoPointCorrelations.mrtCountMask line 15
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMask.lean:15 (same declaration text).
lemma OAI.TwoPointCorrelations.finitePrimeDivisorCount_one line 18
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMask.lean:18 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCountMask_one line 27
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMask.lean:27 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCountMask_mul line 31
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMask.lean:31 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCountMask_bounds line 36
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMask.lean:36 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCountMask_prime line 40
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMask.lean:40 (same declaration text).
def OAI.TwoPointCorrelations.mrtCountMaskedCoefficient line 52
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMask.lean:52 (same declaration text).
lemma OAI.TwoPointCorrelations.Multiplicative.mrtCountMaskedCoefficient line 55
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMask.lean:55 (same declaration text).
lemma OAI.TwoPointCorrelations.OneBounded.mrtCountMaskedCoefficient line 63
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMask.lean:63 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCountMask_integral line 72
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMask.lean:72 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtCountMaskedCoefficient_integral line 77
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMask.lean:77 (same declaration text).
theorem OAI.TwoPointCorrelations.mrt_reciprocal_count_polynomial line 87
Source documentation
The literal reciprocal-count cofactor polynomial is the average of the corresponding soft-mask polynomials.
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMask.lean:87 (same declaration text).
```
theorem mrt_reciprocal_count_polynomial (S P : Finset ℕ) (a : ℕ → ℂ) :
    (∑ n ∈ S, a n / ((finitePrimeDivisorCount P n : ℂ) + 1)) =
      ∫ u in (0 : ℝ)..1, ∑ n ∈ S, mrtCountMaskedCoefficient a P u n := by
…
```
Mentions: OAI.TwoPointCorrelations.finitePrimeDivisorCount, OAI.TwoPointCorrelations.mrtCountMaskedCoefficient
theorem OAI.TwoPointCorrelations.mrt_reciprocal_count_polynomial_bound line 96
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMask.lean:96 (same declaration text).
theorem OAI.TwoPointCorrelations.mrtCountMaskedCoefficient_distance line 110
Source documentation
Every member of the cofactor integral keeps at least half of the original distance, uniformly in the softening parameter.
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMask.lean:110 (same declaration text).
```
theorem mrtCountMaskedCoefficient_distance (F twist : ℕ → ℂ) (P : Finset ℕ)
    {u : ℝ} (hu : 0 ≤ u) (hu1 : u ≤ 1) (N : ℕ)
    (hF : ∀ p ∈ primesUpTo N, ‖F p‖ ≤ 1)
    (htwist : ∀ p ∈ primesUpTo N, ‖twist p‖ ≤ 1) :
    squaredDistance F twist N ≤
      2 * squaredDistance (mrtCountMaskedCoefficient F P u) twist N := by
…
```
Mentions: OAI.TwoPointCorrelations.primesUpTo, OAI.TwoPointCorrelations.mrtCountMaskedCoefficient
theorem OAI.TwoPointCorrelations.mrt_missing_count_mask_distance line 121
Source documentation
Missing-band and reciprocal-count masks are combined before applying the distance inequality, so there is only one factor-two loss.
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMask.lean:121 (same declaration text).
```
theorem mrt_missing_count_mask_distance (F twist : ℕ → ℂ) (Q P : Finset ℕ)
    {u : ℝ} (hu : 0 ≤ u) (hu1 : u ≤ 1) (N : ℕ)
    (hF : ∀ p ∈ primesUpTo N, ‖F p‖ ≤ 1)
    (htwist : ∀ p ∈ primesUpTo N, ‖twist p‖ ≤ 1) :
    squaredDistance F twist N ≤ 2 * squaredDistance
      (mrtCountMaskedCoefficient (fun n => F n * (mrtPrimeMask Q n : ℂ)) P u) twist N := by
…
```
Mentions: OAI.TwoPointCorrelations.primesUpTo, OAI.TwoPointCorrelations.mrtCountMaskedCoefficient, OAI.TwoPointCorrelations.mrtPrimeMask