noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EulerCorrection (N : ℕ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11EulerCorrection N = (1 + 1 / (↑N ^ (4 / 53) - 2)) ^ 21

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_weighted_density_upper : ∃ (C : ℝ), 0 < C ∧ ∃ (K : ℝ), 1 < K ∧ ∀ (θ : ℝ), 0 < θ → θ < 1 / 8 → ∃ (Q₀ : ℝ), 4 ≤ Q₀ ∧ ∀ (N : ℕ), 4 ≤ N → Even N → 4 ≤ ↑N ^ (4 / 53) → ∀ (Q : ℝ), Q₀ ≤ Q → Q ≤ ↑N → √↑N ≤ Q ^ 2 → 0 ≤ fouvryG9UpperFactor N Q C K θ ∧ ∀ (ι : Type) (I : Finset ι) (a : ι → ℕ) (w : ι → ℝ), (∀ i ∈ I, 0 ≤ w i) → (∀ i ∈ I, w i ≠ 0 → 0 < a i ∧ (∀ p ∈ (a i).primeFactors, ↑N ^ (4 / 53) ≤ ↑p) ∧ (a i).primeFactors.card ≤ 21) → ∑ i ∈ I, w i * LiLiuPrereqWF.externalDensity true (fouvryG9SievePrimes N √↑N) (LiLiuPrereqWF.externalInternalLevel Q θ) θ (√↑N) (LiLiuPrereqWF.progressionDensity (a i)) ≤ fouvryG9UpperFactor N Q C K θ * fouvryG9BaseEuler N √↑N * goldbachG11EulerCorrection N * ∑ i ∈ I, w i

Uniform analytic evaluation of a finite weighted progression-density main term. Its hypotheses are literal rough support and nonnegative weights, not an assumed distribution estimate. The constants precede all changing finite data.