MRTCountWindows.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A proved pointwise estimate for the actual reciprocal-count cofactor polynomial. The finite cutoff loss is absolute and all masks are uniform.

theorem OAI.TwoPointCorrelations.mrt_reciprocal_count_window_bound line 16

Source documentation

Fixed-window cofactor cancellation from the original function's pretentious distance. The prime masks and window are arbitrary within the stated finite scale conditions.

Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCountWindows.lean:16 (same declaration text).

theorem mrt_reciprocal_count_window_bound :
    ∃ C K X₀ : ℝ, 0 < C ∧ 0 ≤ K ∧
    ∀ (N : ℕ) (a : ℝ), 1 ≤ a → X₀ ≤ (⌊(N : ℝ) / a⌋₊ : ℝ) →
    ∀ (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 (⌊(2 * N : ℝ) / a⌋₊ : ℝ) ^ 8 ≤ T →
      (∀ v : ℝ, |v| ≤ T →
        2 * M + K ≤ squaredDistance F (mrtArchimedeanTwist v) ⌊(2 * N : ℝ) / a⌋₊) →
      ‖mrtCofactorPolynomial P (mrtMissingCoefficient F Q) N a t‖ ≤ C *
        ((M + 1) * Real.exp (-M) +
          Real.log (Real.log (⌊(2 * N : ℝ) / a⌋₊ : ℝ)) /
…

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