theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainLogProductSum_eq_actualTriangleMass (N : ℕ) : goldbachB10MainLogProductSum N (↑N ^ goldbachB10Beta) (↑N ^ goldbachB10Gamma) = goldbachB10ActualTriangleMass N

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10I10_nonneg : 0 ≤ goldbachB10I10

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10MainMass_le_I10_eventually (ε η : ℝ) (hε : 0 < ε) (hεlt : ε < 1) (hη : 0 < η) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → goldbachB10MainMass N ε (↑N ^ goldbachB10Beta) (↑N ^ goldbachB10Gamma) ≤ ((1 - ε) * goldbachB10I10 + η) * (↑N / Real.log ↑N)

The actual floor Li mass has the printed double integral as a one-sided main term.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachB10SiftedCount_I10_upper (δ : ℝ) (hδ : 0 < δ) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (ε : ℝ), 0 < ε → ε < 1 → ∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → have Δ := ↑N ^ (1 / 2) / Real.log ↑N ^ (B + 1); have Z := Δ ^ (1 / 2); ↑(goldbachB10SiftedCount N ε (↑N ^ goldbachB10Beta) (↑N ^ goldbachB10Gamma) Z) ≤ (8 * (1 - ε) * goldbachB10I10 + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Actual B10 count at a legal chosen cutoff, bounded by the printed integral. This theorem does not assume or certify any decimal approximation to the integral.