theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10HighFirstPairs_eq_filter (N : ℕ) (hN : 2 ≤ N) : goldbachC10Pairs N (↑N ^ (1 / 10)) (↑N ^ (1 / 3)) = {rs ∈ goldbachC9Pairs N | ↑N ^ (1 / 10) ≤ ↑rs.1}

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5HighFirstActualAtoms (N : ℕ) (ε : ℝ) : Finset ((_ : ℕ × ℕ) × ℕ)

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5HighFirstActualAtoms N ε = {x ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5ActualAtoms N ε | ↑N ^ (1 / 10) ≤ ↑x.fst.1}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5HighFirstClosed_eq_card (N : ℕ) (hN : 2 ≤ N) (ε : ℝ) : goldbachS5Closed (goldbachDifferenceCarrier N ε) N (↑N ^ (1 / 10)) (↑N ^ (1 / 3)) = ↑(goldbachS5HighFirstActualAtoms N ε).card

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstAtoms_eq_filter (N : ℕ) (hN : 2 ≤ N) : goldbachB10Atoms N 0 (↑N ^ (1 / 10)) (↑N ^ (1 / 3)) = {x ∈ goldbachB9PlusAtoms N | ↑N ^ (1 / 10) ≤ ↑x.fst.1}

Equality of labelled mothers, including the closed first-prime boundary.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB9HighFirstSiftedAtoms_eq_filter (N : ℕ) (hN : 2 ≤ N) (Z : ℝ) : goldbachB10SiftedAtoms N 0 (↑N ^ (1 / 10)) (↑N ^ (1 / 3)) Z = {x ∈ goldbachB9PlusSiftedAtoms N Z | ↑N ^ (1 / 10) ≤ ↑x.fst.1}

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5HighFirstSwitch_mem {N : ℕ} {ε : ℝ} (hN : 2 ≤ N) (hε : 0 < ε) (hcut : ↑N ^ (2 / 3) ≤ ε * ↑N) {x : (_ : ℕ × ℕ) × ℕ} (hx : x ∈ goldbachS5GoodNonsquareAtoms N ε) (hfirst : ↑N ^ (1 / 10) ≤ ↑x.fst.1) : goldbachS5Switch x ∈ goldbachB10Atoms N 0 (↑N ^ (1 / 10)) (↑N ^ (1 / 3)) ∧ Nat.Prime (goldbachB9PlusOutput N (goldbachS5Switch x))

The original injective atom map preserves the restricted first-prime label.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5HighFirstClosed_le_sifted {N : ℕ} {ε Z : ℝ} (hN : 2 ≤ N) (hε : 0 < ε) (hcut : ↑N ^ (2 / 3) ≤ ε * ↑N) (hZ : 1 ≤ Z) : goldbachS5Closed (goldbachDifferenceCarrier N ε) N (↑N ^ (1 / 10)) (↑N ^ (1 / 3)) ≤ goldbachB10SiftedCount N 0 (↑N ^ (1 / 10)) (↑N ^ (1 / 3)) Z + 400 * goldbachBadCount (goldbachDifferenceCarrier N ε) N + 400 * goldbachS5SquareCount N + 400 * ↑⌊Z⌋₊

Only the error budgets use the full family; the main term is the high mother itself.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5HighFirstClosed_le_sifted_normalized (ε η : ℝ) (hε : 0 < ε) (hη : 0 < η) : ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (Z : ℝ), 1 ≤ Z → Z ≤ √↑N → ↑(goldbachS5Closed (goldbachDifferenceCarrier N ε) N (↑N ^ (1 / 10)) (↑N ^ (1 / 3))) ≤ ↑(goldbachB10SiftedCount N 0 (↑N ^ (1 / 10)) (↑N ^ (1 / 3)) Z) + η * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)