noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.envelope : ℝ

The production logarithmic polynomial, with the literal split weights.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.envelope = (36 / 5 * ∫ (u : ℝ) in 4 / 53..1 / 10, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L (1 - 3 * u) / (u * (1 - u) ^ 2)) + 8 * ∫ (u : ℝ) in 1 / 10..1 / 3, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L (1 - 3 * u) / (u * (1 - u))

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

A whole-half-line analytic remainder; no samples or scalar assumptions.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.continuousOn_envelope_kernel (k : ℕ) : ContinuousOn (fun (u : ℝ) => S3Correction.L (1 - 3 * u) / (u * (1 - u) ^ k)) (Set.Icc (4 / 53) (1 / 3))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.actual_le_envelope : goldbachB9PaperSplitIntegral ≤ envelope