theorem G67CenteredEnvelope.L_error {x : ℝ} (hx : x ∈ Set.Icc (-3 / 5) (3 / 5)) : |MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L x - Real.log (1 + x)| ≤ 1 / 10000000

A two-sided error bound, valid also on the negative half of the centered domain.

theorem G67CenteredEnvelope.constant_log_error {r : ℝ} (hr : r ∈ Set.Icc 1 4) : |MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logLower r - Real.log r| ≤ 1 / 10000000000 ∧ |MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.logUpper r - Real.log r| ≤ 1 / 10000000000

Uniform control of the frozen 32-term constant-log bounds without expanding their sum.

theorem G67CenteredEnvelope.reciprocal_error {s : ℝ} (hs : s ∈ Set.Icc (3 / 20) (7 / 20)) : |G67Centered.reciprocalPolynomial s - 1 / (s * (1 / 2 - s))| ≤ 1 / 10000000000 ∧ |1 / (s * (1 / 2 - s))| ≤ 20

The geometric reciprocal approximation is controlled on the whole containing interval.

theorem G67CenteredEnvelope.product_error {p w r P W R : ℝ} (hp : |p - P| ≤ 11 / 100000000) (hw : |w - W| ≤ 22 / 100000000) (hr : |r - R| ≤ 1 / 10000000000) (hP : |P| ≤ 3) (hW : |W| ≤ 3) (hR : |R| ≤ 20) : p * w * r - 1 / 40000 ≤ P * W * R

Absolute product errors do not assume that any polynomial approximation is nonnegative.