noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_innerPolynomial (n m : ℕ) (z : ℝ) : ℝ

The explicit integrated product of the odd logarithm and geometric polynomials.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_innerPolynomial n m z = 2 * ∑ i ∈ Finset.range n, ∑ j ∈ Finset.range m, z ^ (2 * i + j + 2) / (↑(2 * i + 1) * ↑(2 * i + j + 2))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_innerPolynomial_hasDerivAt (n m : ℕ) (z : ℝ) : HasDerivAt (goldbachS3_innerPolynomial n m) ((2 * ∑ i ∈ Finset.range n, z ^ (2 * i + 1) / ↑(2 * i + 1)) * ∑ j ∈ Finset.range m, z ^ j) z

Exact derivative of the fixed rational-coefficient polynomial.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_log_geometric_remainder {z : ℝ} (hz : 0 ≤ z) (hzu : z ≤ 3 / 5) : Real.log ((1 + z) / (1 - z)) / (1 - z) ≤ (2 * ∑ i ∈ Finset.range 24, z ^ (2 * i + 1) / ↑(2 * i + 1)) * ∑ j ∈ Finset.range 48, z ^ j + 1 / 10 ^ 9

A uniform analytic remainder budget on the full transformed S3 range.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_innerEnvelope (s : ℝ) : ℝ

The closed high-accuracy inner-integral envelope.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_innerEnvelope s = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_innerPolynomial 24 48 ((s - 3) / (s - 1)) + (s - 3) / (s - 1) / 10 ^ 9

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_inner_hasDerivAt {s : ℝ} (hs : 3 ≤ s) : HasDerivAt SwitchingPrinciple.jurkatRichertInnerIntegral (Real.log (s - 2) / (s - 1)) s

FTC for the actual shifted inner integral, on the domain used below.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_innerEnvelope_hasDerivAt {s : ℝ} (hs : 3 ≤ s) : HasDerivAt goldbachS3_innerEnvelope (((2 * ∑ i ∈ Finset.range 24, ((s - 3) / (s - 1)) ^ (2 * i + 1) / ↑(2 * i + 1)) * ∑ j ∈ Finset.range 48, ((s - 3) / (s - 1)) ^ j + 1 / 10 ^ 9) * (2 / (s - 1) ^ 2)) s

Derivative of the closed envelope without expanding its coefficients.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_innerEnvelope_derivative_ge {s : ℝ} (hs : s ∈ Set.Icc 3 (45 / 8)) : Real.log (s - 2) / (s - 1) ≤ ((2 * ∑ i ∈ Finset.range 24, ((s - 3) / (s - 1)) ^ (2 * i + 1) / ↑(2 * i + 1)) * ∑ j ∈ Finset.range 48, ((s - 3) / (s - 1)) ^ j + 1 / 10 ^ 9) * (2 / (s - 1) ^ 2)

The polynomial's derivative dominates the real kernel everywhere, not at sample points.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_inner_le_envelope {s : ℝ} (hs : s ∈ Set.Icc 3 (45 / 8)) : SwitchingPrinciple.jurkatRichertInnerIntegral s ≤ goldbachS3_innerEnvelope s

A fixed rational-coefficient, whole-interval envelope for the actual inner integral.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_log_geometric_lower {z : ℝ} (hz : 0 ≤ z) (hzu : z < 1) : (2 * ∑ i ∈ Finset.range 24, z ^ (2 * i + 1) / ↑(2 * i + 1)) * ∑ j ∈ Finset.range 48, z ^ j ≤ Real.log ((1 + z) / (1 - z)) / (1 - z)

The same fixed product polynomial is a lower derivative bound.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_innerPolynomial_le_inner {s : ℝ} (hs : s ∈ Set.Icc 3 (45 / 8)) : goldbachS3_innerPolynomial 24 48 ((s - 3) / (s - 1)) ≤ SwitchingPrinciple.jurkatRichertInnerIntegral s

The transformed polynomial also lies below the actual inner integral.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_innerEnvelope_error {s : ℝ} (hs : s ∈ Set.Icc 3 (45 / 8)) : 0 ≤ goldbachS3_innerEnvelope s - SwitchingPrinciple.jurkatRichertInnerIntegral s ∧ goldbachS3_innerEnvelope s - SwitchingPrinciple.jurkatRichertInnerIntegral s ≤ 3 / (5 * 10 ^ 9)

Two-sided, uniform certification of the approximation error.

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_fullEnvelope (s : ℝ) : ℝ

A closed rational majorant of the entire original piecewise numerator.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_fullEnvelope s = (1 + MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_innerEnvelope (max s 3) + max (s - 5) 0 ^ 4 / 576) / (s * (53 / 8 - s))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_fullEnvelope_majorizes {s : ℝ} (hs : s ∈ Set.Icc (53 / 24) (45 / 8)) : (if s ≤ 3 then 1 else if s ≤ 5 then 1 + SwitchingPrinciple.jurkatRichertInnerIntegral s else 1 + SwitchingPrinciple.jurkatRichertInnerIntegral 5 + ∫ (t : ℝ) in 5..s, (Real.log (t - 2) + ∫ (v : ℝ) in 3..t - 2, SwitchingPrinciple.jurkatRichertInnerIntegral v / v) / (t - 1)) / (s * (53 / 8 - s)) ≤ goldbachS3_fullEnvelope s

Whole-interval majorization of the actual exp-free integrand by a closed expression.