theorem G12AnalyticCertificate.L_sub_log_le {x : ℝ} (hx : 0 ≤ x) : MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L x - Real.log (1 + x) ≤ x ^ 34 / 34

Analytic remainder bound for the imported polynomial, without coefficient enumeration.

noncomputable def G12AnalyticCertificate.densityPrimitive (u : ℝ) : ℝ

Exact primitive of the original density, not of an altered continuous weight.

Equations

• G12AnalyticCertificate.densityPrimitive u = 33 / 4 * Real.log u + (2 - Real.log (4 / 33 / u)) / u

theorem G12AnalyticCertificate.densityPrimitive_deriv {u : ℝ} (hu : 0 < u) : HasDerivAt densityPrimitive (G12SharpQuadrature.density u) u

theorem G12AnalyticCertificate.high_integral_exact : ∫ (u : ℝ) in 1 / 10..4 / 33, G12SharpQuadrature.density u = densityPrimitive (4 / 33) - densityPrimitive (1 / 10)

FTC eliminates the full high-branch density integral exactly.

theorem G12AnalyticCertificate.upperDensity_pullback {x : ℝ} (hx : 0 ≤ x) : upperDensity (4 / 33 / (1 + x)) * (4 / 33 / (1 + x) ^ 2) = 33 / 4 * (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L x - x / (1 + x))

Pullback identity for the rational envelope, including the Jacobian.

theorem G12AnalyticCertificate.upperDensity_low_pullback {x : ℝ} (hx : 0 ≤ x) : upperDensity (4 / 33 / (1 + x)) / (1 - 4 / 33 / (1 + x)) * (4 / 33 / (1 + x) ^ 2) = 33 / 4 * ((1 + x) * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L x - x) / (x + 29 / 33)

The low pullback preserves exactly the original factor 1/(1-u).