theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPair_product_bounds {N r s : ℕ} (hN : 4 ≤ N) (hr : r ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) (hs : s ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) (↑N ^ (3 / 11))) : 0 < r * s ∧ ↑N ^ (8 / 53) ≤ ↑(r * s) ∧ ↑(r * s) ≤ ↑N ^ (13 / 33)

Actual prime-pair membership supplies both product power bounds.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairMovingMain (N : ℕ) (hEven : Even N) (ε B ρ : ℝ) (T : Finset (ℕ × ℕ)) : ℝ

A nonnegative kernel on the original pair labels at the genuine natural layer.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairMovingMain N hEven ε B ρ T = ∑ a ∈ T, have S := MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3BoundingSieve N hEven ε (↑N ^ (4 / 53)) (a.1 * a.2); have D := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B / (a.1 * a.2) + 1; S.totalMass * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S * max 0 (MathlibNt.SieveTheory.JurkatRichert1965ChenGammaOneQOne.jr1965f (Real.log ↑D / Real.log (↑N ^ (4 / 53))) - ρ)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairMovingMain_paid (U : ℝ) (hU : 0 < U) : ∃ (B : ℝ), 0 ≤ B ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (ρ : ℝ), 0 < ρ → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N) (ε : ℝ), 0 ≤ ε → ε < 2 / 15 → ∀ (T : Finset (ℕ × ℕ)), (∀ a ∈ T, a.1 ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) ∧ a.2 ∈ goldbachClosedPrimes N (↑N ^ (4 / 53)) (↑N ^ (3 / 11)) ∧ a.1 ≤ a.2) → goldbachPairMovingMain N hEven ε B ρ T - C * ↑N / Real.log ↑N ^ U ≤ ∑ a ∈ T, ↑(literalH (goldbachDifferenceCarrier N ε) N (a.1 * a.2) (↑N ^ (4 / 53)))

Actual moving lower kernels with the complete BV error paid, including the low-coordinate branch. The threshold precedes epsilon and every pair family.