theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pairs_filter_first_ge (N : ℕ) (b c t : ℝ) (hbt : b ≤ t) : {rs ∈ goldbachC10Pairs N b c | t ≤ ↑rs.1} = goldbachC10Pairs N t c

Raising the first-prime lower cutoff gives precisely the closed high subfamily.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pairs_sum_split_first {α : Type u_1} [AddCommMonoid α] (N : ℕ) (b c t : ℝ) (hbt : b ≤ t) (f : ℕ × ℕ → α) : ∑ rs ∈ goldbachC10Pairs N b c, f rs = ∑ rs ∈ goldbachC10Pairs N b c with ↑rs.1 < t, f rs + ∑ rs ∈ goldbachC10Pairs N t c, f rs

Exact labelled partition, valid for any additive weights; no inequality is subtracted.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5ClosedBelow (A : Finset ℕ) (N : ℕ) (b c t : ℝ) : ℤ

Strict low first-prime part of the original H-sum, with all other labels retained.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5ClosedBelow A N b c t = ∑ rs ∈ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10Pairs N b c with ↑rs.1 < t, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.literalH A (N * rs.1) (rs.1 * rs.2) ↑rs.2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Closed_eq_below_add_raisedCutoff (A : Finset ℕ) (N : ℕ) (b c t : ℝ) (hbt : b ≤ t) : goldbachS5Closed A N b c = goldbachS5ClosedBelow A N b c t + goldbachS5Closed A N t c

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5Closed_actual_split_first (N : ℕ) (hN : 2 ≤ N) (ε : ℝ) : goldbachS5Closed (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) = goldbachS5ClosedBelow (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) (↑N ^ (1 / 10)) + goldbachS5Closed (goldbachDifferenceCarrier N ε) N (↑N ^ (1 / 10)) (↑N ^ (1 / 3))

The source-paper boundary goes to the high term; the original epsilon carrier is unchanged. Neither a high-only analytic upper bound nor a low improved estimate is claimed here.