noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_primeKernelIntegral (β : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_primeKernelIntegral β = ∫ (u : ℝ) in 4 / 53..β, MathlibNt.SieveTheory.suzukiContinuousUpperFactor ((1 / 2 - u) / (4 / 53)) / u

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_primeKernel_upper (B β η : ℝ) (hB : 0 ≤ B) (hβ : 4 / 53 < β) (hβu : β ≤ 1 / 3) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∑ p ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) (↑N ^ β), suzukiContinuousUpperFactor (goldbachS3_sieveRatio N B p) / ↑p.totient ≤ goldbachS3_primeKernelIntegral β + η

The main-term payment for the actual closed S3 prime set, with the genuine rounded Pan ratio and the positive inverse-totient correction.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_unitKernel_upper (β η : ℝ) (hβ : 4 / 53 < β) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∑ p ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) (↑N ^ β), 1 / ↑p.totient ≤ Real.log (β / (4 / 53)) + η

Unit-weight payment for additive noise on the same actual closed carrier.