HalaszCofactorBandCount.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual original prime bands fit the cofactor inclusion-exclusion budget even when their cutoff is specified at the original scale.

theorem OAI.TwoPointCorrelations.halasz_cofactor_band_count line 11

theorem OAI.TwoPointCorrelations.halasz_moderate_actual_cofactor line 42

Source documentation

The moderate-frequency cofactor bound for the actual original bands.

theorem halasz_moderate_actual_cofactor :
    ∃ X₀ : ℝ, ∀ᶠ n : ℕ in atTop,
      ∀ (N : ℕ) (a : ℝ), 1 ≤ a → X₀ ≤ (⌊(N:ℝ)/a⌋₊:ℝ) →
      n = ⌊(2*N:ℝ)/a⌋₊ → ∀ X : ℕ, n ≤ X → X ≤ n^3 →
      ∀ (F : ℕ → ℂ), F 1 = 1 → Multiplicative F → OneBounded F →
      ∀ (P Q : ℝ) (J : ℕ), 1 ≤ Real.log Q →
      mrtBandUpper Q J ≤ Real.exp (Real.sqrt (Real.log X)) →
      ∀ A : Finset ℕ, (∀ p ∈ A, p.Prime) → ∀ t τ : ℝ,
      (∀ v : ℝ, |v| ≤ X → squaredDistance F (mrtArchimedeanTwist τ) X ≤
        squaredDistance F (mrtArchimedeanTwist v) X) →
      |t|+(Real.log n)^8 ≤ X →
      |t-τ|+(Real.log n)^8 ≤ (Real.log X)^20 →
…

Mentions: OAI.TwoPointCorrelations.Multiplicative, OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtBandUpper, OAI.TwoPointCorrelations.mrtArchimedeanTwist