noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG6Pairs (N : ℕ) (z b : ℝ) : Finset (ℕ × ℕ)

The original G6 labels, with the smaller selected prime first.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG6Pairs N z b = Finset.image (fun (a : (_ : ℕ) × ℕ) => (a.snd, a.fst)) ((MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N z b).sigma fun (s : ℕ) => MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N z ↑s)

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG7Pairs (N : ℕ) (z b c : ℝ) : Finset (ℕ × ℕ)

The original closed G7 labels; the shared endpoint is not removed.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG7Pairs N z b c = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N z b ×ˢ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachClosedPrimes N b c

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.mem_goldbachG6Pairs_iff {N : ℕ} {z b : ℝ} {a : ℕ × ℕ} : a ∈ goldbachG6Pairs N z b ↔ a.2 ∈ goldbachClosedPrimes N z b ∧ a.1 ∈ goldbachClosedPrimes N z ↑a.2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG6Pairs_sum_eq (A : Finset ℕ) (N : ℕ) (z b : ℝ) : ∑ a ∈ goldbachG6Pairs N z b, literalH A N (a.1 * a.2) z = goldbachWeightG6 A N z b

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG7Pairs_sum_eq (A : Finset ℕ) (N : ℕ) (z b c : ℝ) : ∑ a ∈ goldbachG7Pairs N z b c, literalH A N (a.1 * a.2) z = goldbachWeightG7 A N z b c

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairLowerMain (N : ℕ) (ε B : ℝ) (T : Finset (ℕ × ℕ)) : ℝ

The actual signed ordinary Rosser main term, not an integral approximation.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPairLowerMain N ε B T = MathlibNt.SieveTheory.BombieriVinogradov.trueLogarithmicIntegral ↑(MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1Endpoint N ε) * ∑ a ∈ T, 1 / ↑(a.1 * a.2).totient * ∑ d ∈ (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1ProdPrimes N (↑N ^ (4 / 53))).divisors, MathlibNt.SieveTheory.LinearSieve.lowerRosserWeight (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1ProdPrimes N (↑N ^ (4 / 53))) (MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N B / (a.1 * a.2) + 1) d / ↑d.totient

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG67_lowerRosser_paid (U : ℝ) (hU : 0 < U) : ∃ (B : ℝ), 0 ≤ B ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (ε : ℝ), 0 < ε → ε < 2 / 15 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → goldbachPairLowerMain N ε B (goldbachG6Pairs N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) - C * ↑N / Real.log ↑N ^ U ≤ ↑(goldbachWeightG6 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33))) ∧ goldbachPairLowerMain N ε B (goldbachG7Pairs N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11))) - C * ↑N / Real.log ↑N ^ U ≤ ↑(goldbachWeightG7 (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (4 / 33)) (↑N ^ (3 / 11)))

The same BV constants pay each original G6 and G7 family. They remain separate families: their common closed endpoint is counted in each original term.