noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairKernelSum (N : ℕ) (K : ℝ × ℝ → ℝ) (T : Finset (ℕ × ℕ)) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairKernelSum N K T = ∑ p ∈ T, K (MathlibNt.SieveTheory.LiuWeight.pairLogCoordinate N p) / (↑p.1 * ↑p.2)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.coprimePrimeLogRectanglePairs_subset_closed (N : ℕ) (a b c d : ℝ) : LiuWeight.coprimePrimeLogRectanglePairs N a b c d ⊆ goldbachClosedPrimes N (↑N ^ a) (↑N ^ b) ×ˢ goldbachClosedPrimes N (↑N ^ c) (↑N ^ d)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.coprimePrimeKernelRectangle_le_closed (N : ℕ) (a b c d : ℝ) (K : ℝ × ℝ → ℝ) (hK : ∀ (x : ℝ × ℝ), 0 ≤ K x) : LiuWeight.coprimePrimeKernelRectangle N a b c d K ≤ goldbachPairKernelSum N K (goldbachClosedPrimes N (↑N ^ a) (↑N ^ b) ×ˢ goldbachClosedPrimes N (↑N ^ c) (↑N ^ d))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG6_coprime_square_kernel_le (N : ℕ) (a b : ℝ) (K : ℝ × ℝ → ℝ) (hK : ∀ (x : ℝ × ℝ), 0 ≤ K x) (hsym : ∀ (u v : ℝ), K (u, v) = K (v, u)) : 1 / 2 * LiuWeight.coprimePrimeKernelRectangle N a b a b K ≤ goldbachPairKernelSum N K (goldbachG6Pairs N (↑N ^ a) (↑N ^ b))

The closed square retains its diagonal and all original copN labels.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_goldbachG6_kernel_integral_lower {a b : ℝ} (ha : 0 < a) (hab : a < b) {K : ℝ × ℝ → ℝ} {L : NNReal} (hK : LipschitzWith L K) (hpos : ∀ (x : ℝ × ℝ), 0 ≤ K x) (hsym : ∀ (u v : ℝ), K (u, v) = K (v, u)) {η : ℝ} (hη : 0 < η) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → (1 / 2 * ∫ (u : ℝ) (v : ℝ) in a..b, K (u, v) / (u * v)) - η ≤ goldbachPairKernelSum N K (goldbachG6Pairs N (↑N ^ a) (↑N ^ b))

General symmetric nonnegative Lipschitz kernels on the original G6 labels.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_goldbachG7_kernel_integral_lower {a b c : ℝ} (ha : 0 < a) (hab : a < b) (hbc : b < c) {K : ℝ × ℝ → ℝ} {L : NNReal} (hK : LipschitzWith L K) (hpos : ∀ (x : ℝ × ℝ), 0 ≤ K x) {η : ℝ} (hη : 0 < η) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → (∫ (u : ℝ) in a..b, ∫ (v : ℝ) in b..c, K (u, v) / (u * v)) - η ≤ goldbachPairKernelSum N K (goldbachG7Pairs N (↑N ^ a) (↑N ^ b) (↑N ^ c))

The G7 shared closed boundary is retained; the lower rectangle is only a subset.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.exists_goldbachG67_kernel_integral_lower {a b c : ℝ} (ha : 0 < a) (hab : a < b) (hbc : b < c) {K : ℝ × ℝ → ℝ} {L : NNReal} (hK : LipschitzWith L K) (hpos : ∀ (x : ℝ × ℝ), 0 ≤ K x) (hsym : ∀ (u v : ℝ), K (u, v) = K (v, u)) {η : ℝ} (hη : 0 < η) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ((1 / 2 * ∫ (u : ℝ) (v : ℝ) in a..b, K (u, v) / (u * v)) + ∫ (u : ℝ) in a..b, ∫ (v : ℝ) in b..c, K (u, v) / (u * v)) - η ≤ goldbachPairKernelSum N K (goldbachG6Pairs N (↑N ^ a) (↑N ^ b)) + goldbachPairKernelSum N K (goldbachG7Pairs N (↑N ^ a) (↑N ^ b) (↑N ^ c))

A common threshold and an explicitly split error budget for both original families.