MinorArcSieveSaving.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The four-prime estimate in corrected MRT, equation (3.3).

theorem OAI.TwoPointCorrelations.minor_arc_sieve_saving line 14

Source documentation

The additive-energy sieve and rational kernel give the required uniform four-prime saving. The prime set may be any subset of the dyadic prime block.

theorem minor_arc_sieve_saving :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ R : ℝ in atTop,
      ∀ (P : Finset ℕ) (N : ℕ),
      (∀ p ∈ P, p.Prime ∧ p ≠ 2 ∧ p ≤ N) → (N : ℝ) ≤ 2 * R →
      ∀ H W V : ℝ, 1 ≤ W → W ≤ R →
      ∀ (a : ℤ) (q : ℕ), 2 ≤ q → W ≤ (q : ℝ) → (q : ℝ) ≤ H / W →
      R ≤ H / W → 0 ≤ V → V ≤ H / R →
      ∀ α : ℝ, IsCoprime (q : ℤ) a →
      |α - (a : ℝ) / (q : ℝ)| ≤ 1 / (q : ℝ) ^ 2 →
      (∑ p₁ ∈ P, ∑ p₂ ∈ P, ∑ p₃ ∈ P, ∑ p₄ ∈ P,
        minorArcGeometricBound V (α * ((p₁ : ℝ) + p₂ - p₃ - p₄))) ≤
          C * H * R ^ 3 * (1 + Real.log H) / (W * Real.log R ^ 4) := by
…

Mentions: OAI.TwoPointCorrelations.minorArcGeometricBound