GoldbachSieveApplication.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A finite, unconditional Selberg upper bound for ordered prime pairs with the actual Goldbach local density and explicit root-count error. The analytic estimates for the optimizing weights and denominator are separate tasks.

theorem OAI.Problem337.goldbach_primePairs_lambdaSquared_bound line 19

Source documentation

The actual Goldbach local density and progression error may be inserted in the multiplicity-preserving Selberg model. All arithmetic approximation input has been discharged; the weights are still arbitrary with w 1 = 1.

theorem goldbach_primePairs_lambdaSquared_bound (N P : ℕ)
    (hN : 2 ∣ N) (hP : Squarefree P) (w : ℕ → ℝ) (hw : w 1 = 1) :
    ((PrimePairSieve.primePairs N).card : ℝ) ≤
      ((N - 1 : ℕ) : ℝ) *
        (∑ d ∈ P.divisors, BoundingSieve.lambdaSquared w d * goldbachSieveDensity N d) +
      (∑ d ∈ P.divisors, |BoundingSieve.lambdaSquared w d| * goldbachSieveRootCount N d) +
      2 * P.primeFactors.card := by
…

Mentions: OAI.Problem337.PrimePairSieve.primePairs, OAI.Problem337.goldbachSieveDensity, OAI.Problem337.goldbachSieveRootCount