MRTCountMean.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Ordinary mean cancellation with the literal reciprocal prime-count weight. Integrating multiplicative soft masks gives the cofactor weight exactly, while the missing-band and count masks lose only one factor two in pretentious distance.

def OAI.TwoPointCorrelations.mrtMissingCoefficient line 16
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMean.lean:16 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtMissingCoefficient_one line 19
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMean.lean:19 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtMissingCoefficient_multiplicative line 24
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMean.lean:24 (same declaration text).
lemma OAI.TwoPointCorrelations.mrtMissingCoefficient_oneBounded line 32
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMean.lean:32 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_missing_count_one line 40
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMean.lean:40 (same declaration text).

theorem OAI.TwoPointCorrelations.mrt_missing_count_prefix_mean line 49

Source documentation

The constant is uniform over both finite prime masks and the entire softening parameter. No lower bound on the number of selected primes is required.

Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMean.lean:49 (same declaration text).

theorem mrt_missing_count_prefix_mean : ∃ C X₀ : ℝ, 0 < C ∧
    ∀ (N : ℕ), X₀ ≤ N →
    ∀ (F : ℕ → ℂ), F 1 = 1 → Multiplicative F → OneBounded F →
    ∀ (Q P : Finset ℕ), (∀ p ∈ Q, p.Prime) → (∀ p ∈ P, p.Prime) →
    ∀ (t T M : ℝ), 0 ≤ M → |t| + Real.log (N : ℝ) ^ 8 ≤ T →
      (∀ v : ℝ, |v| ≤ T → 2 * M ≤ squaredDistance F (mrtArchimedeanTwist v) N) →
      ∀ u : ℝ, 0 ≤ u → u ≤ 1 →
        ‖∑ n ∈ Icc 1 N,
          mrtCountMaskedCoefficient (mrtMissingCoefficient F Q) P u n *
            conj (mrtArchimedeanTwist t n)‖ ≤ C * N *
          ((M + 1) * Real.exp (-M) + Real.log (Real.log N) / Real.log N) := by
…

Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtArchimedeanTwist, OAI.TwoPointCorrelations.mrtCountMaskedCoefficient, OAI.TwoPointCorrelations.mrtMissingCoefficient

theorem OAI.TwoPointCorrelations.mrt_reciprocal_count_prefix_mean line 79

Source documentation

The reciprocal-count weighted cofactor prefix is the integral of the preceding multiplicative means, not an additional analytic hypothesis.

Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountMean.lean:79 (same declaration text).

theorem mrt_reciprocal_count_prefix_mean : ∃ C X₀ : ℝ, 0 < C ∧
    ∀ (N : ℕ), X₀ ≤ N →
    ∀ (F : ℕ → ℂ), F 1 = 1 → Multiplicative F → OneBounded F →
    ∀ (Q P : Finset ℕ), (∀ p ∈ Q, p.Prime) → (∀ p ∈ P, p.Prime) →
    ∀ (t T M : ℝ), 0 ≤ M → |t| + Real.log (N : ℝ) ^ 8 ≤ T →
      (∀ v : ℝ, |v| ≤ T → 2 * M ≤ squaredDistance F (mrtArchimedeanTwist v) N) →
      ‖∑ n ∈ Icc 1 N,
        (mrtMissingCoefficient F Q n * conj (mrtArchimedeanTwist t n)) /
          ((finitePrimeDivisorCount P n : ℂ) + 1)‖ ≤ C * N *
        ((M + 1) * Real.exp (-M) + Real.log (Real.log N) / Real.log N) := by
…

Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtArchimedeanTwist, OAI.TwoPointCorrelations.mrtMissingCoefficient, OAI.TwoPointCorrelations.finitePrimeDivisorCount