OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMask.lean

GitHub source file

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.

  1. def OAI.TwoPointCorrelations.mrtCountMask line 15

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

  2. lemma OAI.TwoPointCorrelations.finitePrimeDivisorCount_one line 18

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTCountMask.lean:18 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.mrtCountMask_one line 27

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTCountMask.lean:27 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.mrtCountMask_mul line 31

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTCountMask.lean:31 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.mrtCountMask_bounds line 36

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTCountMask.lean:36 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.mrtCountMask_prime line 40

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTCountMask.lean:40 (same declaration text).

  7. def OAI.TwoPointCorrelations.mrtCountMaskedCoefficient line 52

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTCountMask.lean:52 (same declaration text).

  8. lemma OAI.TwoPointCorrelations.Multiplicative.mrtCountMaskedCoefficient line 55

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTCountMask.lean:55 (same declaration text).

  9. lemma OAI.TwoPointCorrelations.OneBounded.mrtCountMaskedCoefficient line 63

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTCountMask.lean:63 (same declaration text).

  10. lemma OAI.TwoPointCorrelations.mrtCountMask_integral line 72

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

  11. lemma OAI.TwoPointCorrelations.mrtCountMaskedCoefficient_integral line 77

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTCountMask.lean:77 (same declaration text).

  12. 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/TwoPointCorrelations/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

  13. theorem OAI.TwoPointCorrelations.mrt_reciprocal_count_polynomial_bound line 96

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

  14. 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/TwoPointCorrelations/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

  15. 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/TwoPointCorrelations/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