MRTTypicalWindow.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact remaining-band inclusion--exclusion inside the fixed-window cofactor. The resulting pointwise bound keeps its finite 2^#J cost explicit. No estimate for the typical polynomial is assumed.

lemma OAI.TwoPointCorrelations.mrtTypicalCoefficient_expansion line 15
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalWindow.lean:15 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_typical_cofactor_expansion line 37
Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalWindow.lean:37 (same declaration text).

theorem OAI.TwoPointCorrelations.mrt_typical_cofactor_window_bound line 61

Source documentation

Applying the proved general Halász estimate to every actual missing-band cofactor. This version is intended for frequencies far from a minimizing twist; the near-twist Euler argument separately avoids the power-of-two loss.

Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTTypicalWindow.lean:61 (same declaration text).

theorem mrt_typical_cofactor_window_bound :
    ∃ C K X₀ : ℝ, 0 < C ∧ 0 ≤ K ∧
    ∀ (N : ℕ) (a : ℝ), 1 ≤ a → X₀ ≤ (⌊(N : ℝ) / a⌋₊ : ℝ) →
    ∀ (F : ℕ → ℂ), F 1 = 1 → Multiplicative F → OneBounded F →
    ∀ (ι : Type*) (J : Finset ι) (P : ι → Finset ℕ) (Q : Finset ℕ),
      (∀ j ∈ J, ∀ p ∈ P j, p.Prime) → (∀ p ∈ Q, 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 Q (mrtTypicalCoefficient J P F) N a t‖ ≤
        (2 : ℝ) ^ J.card * C * ((M + 1) * Real.exp (-M) +
…

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