HalaszExceptionalCofactor.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual cofactor bounds with a local frequency hypothesis.

theorem OAI.TwoPointCorrelations.halasz_exceptional_count_window line 13

theorem OAI.TwoPointCorrelations.halasz_exceptional_typical_window line 94

Source documentation

Remaining-band inclusion--exclusion preserves the local frequency window.

theorem halasz_exceptional_typical_window :
    ∃ 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 τ M : ℝ), 0 ≤ M →
      (∀ v : ℝ, |v-t| ≤ Real.log (⌊(2 * N : ℝ) / a⌋₊ : ℝ) ^ 8 →
        1/2 ≤ |v-τ| → 2 * M + K ≤ squaredDistance F (mrtArchimedeanTwist v) ⌊(2 * N : ℝ) / a⌋₊) →
      ‖mrtCofactorPolynomial Q (mrtTypicalCoefficient J P F) N a t‖ ≤
        (2 : ℝ) ^ J.card * C * ((min M (Real.log (1+|τ-t|)) + 1) * Real.exp (-min M (Real.log (1+|τ-t|))) +
          Real.log (Real.log (⌊(2 * N : ℝ) / a⌋₊ : ℝ)) /
…

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