theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8Plus_upperErrSum_le_sieveDivisorSum (N : ℕ) (hEven : Even N) (Z Δ : ℝ) (Q : ℕ) (hQ : ⌊Δ⌋₊ ≤ Q) : have S := goldbachB8PlusBoundingSieve N hEven Z; LinearSieve.upperErrSum S (⌊Δ⌋₊ + 1) (LinearSieve.upperRosserWeight S.prodPrimes (⌊Δ⌋₊ + 1)) ≤ ∑ d ∈ Finset.Icc 1 Q with d ∣ goldbachB10ProdPrimes N Z, |BoundingSieve.rem d|

Only actual sieve divisors occur; the interval includes modulus one.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8Plus_floor_paidLevel_le_panModulusCutoff (N : ℕ) (B : ℝ) (hlog : 1 ≤ Real.log ↑N) : ⌊↑N ^ (1 / 2) / Real.log ↑N ^ (B + 1)⌋₊ ≤ LiuWeight.panModulusCutoff N B

The paid level has exponent B+1, whereas the supplied Pan window has exponent B.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8Plus_upperErrSum_log_saving (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N), ∀ Z ≤ ↑N ^ (3 / 11), have Δ := ↑N ^ (1 / 2) / Real.log ↑N ^ (B + 1); have S := goldbachB8PlusBoundingSieve N hEven Z; LinearSieve.upperErrSum S (⌊Δ⌋₊ + 1) (LinearSieve.upperRosserWeight S.prodPrimes (⌊Δ⌋₊ + 1)) ≤ C * ↑N / Real.log ↑N ^ U

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB8PlusSiftedCount_upper_paid (U : ℝ) (hU : 0 < U) : ∃ (C : ℝ), 0 < C ∧ ∃ (B : ℝ), 0 ≤ B ∧ ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (ρ : ℝ), 0 < ρ → ∃ (z₀ : ℝ), ∀ (N : ℕ), N₀ ≤ N → ∀ (hEven : Even N) (Z s : ℝ), z₀ ≤ Z → 2 ≤ Z → Z ≤ ↑N ^ (3 / 11) → s = Real.log (↑N ^ (1 / 2) / Real.log ↑N ^ (B + 1)) / Real.log Z → 3 / 2 ≤ s → s ≤ 4 → have S := goldbachB8PlusBoundingSieve N hEven Z; ↑(goldbachB8PlusSiftedAtoms N Z).card ≤ goldbachB8PlusMainMass N * (SwitchingPrinciple.jurkatRichertUpperLinearSieveFactor s + ρ) * AnalyticNumberTheory.Sieve.sieveProductPrimeFactors S + C * ↑N / Real.log ↑N ^ U

The actual labelled upper sieve, with the entire finite remainder paid. The threshold for N is independent of the factor tolerance and the sieve cutoff.