theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5ClosedBelow_le_positivePrefix_sifted_normalized_of_pos (eps delta : ℝ) (heps : 0 < eps) (hdelta : 0 < delta) : ∃ (N0 : ℕ), 4 ≤ N0 ∧ ∀ (N : ℕ), N0 ≤ N → ∀ (Z : ℝ), 1 ≤ Z → Z ≤ √↑N → ↑(goldbachS5ClosedBelow (goldbachDifferenceCarrier N eps) N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) (↑N ^ (1 / 10))) ≤ ↑(goldbachB9LowPositivePrefixSiftedCount N eps Z) + delta * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

All finite losses are internal; the threshold is chosen before the sieve cutoff.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS5ClosedBelow_le_positivePrefix_sifted_normalized (delta : ℝ) (hdelta : 0 < delta) (eps : ℝ) (heps : 0 < eps ∧ eps < 2 / 15) : ∃ (N0 : ℕ), 4 ≤ N0 ∧ ∀ (N : ℕ), N0 ≤ N → ∀ (Z : ℝ), 1 ≤ Z → Z ≤ √↑N → ↑(goldbachS5ClosedBelow (goldbachDifferenceCarrier N eps) N (↑N ^ (4 / 53)) (↑N ^ (1 / 3)) (↑N ^ (1 / 10))) ≤ ↑(goldbachB9LowPositivePrefixSiftedCount N eps Z) + delta * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)