noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarK (z : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarK z = 1 / (1 - z) - 1 / (3 - z)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarH_remainder {z : ℝ} (_hz : 0 ≤ z) (hzu : z ≤ 1 / 2) : goldbachPositiveScalarK z - goldbachPositiveScalarH z = z ^ 32 / (1 - z) - (z / 3) ^ 32 / (3 - z)

Exact signed remainder: the subtracted geometric tail has the correct sign.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarH_bounds {z : ℝ} (hz : 0 ≤ z) (hzu : z ≤ 1 / 2) : 0 ≤ goldbachPositiveScalarK z - goldbachPositiveScalarH z ∧ goldbachPositiveScalarK z - goldbachPositiveScalarH z ≤ 1 / 2 ^ 31

Fixed whole-interval geometric error, not a finite-point test.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarK_bounds {z : ℝ} (_hz : 0 ≤ z) (hzu : z ≤ 1 / 2) : 0 ≤ goldbachPositiveScalarK z ∧ goldbachPositiveScalarK z ≤ 2

Bounds on the exact Jacobian kernel.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalar_derivative_bounds {v : ℝ} (hv : v ∈ Set.Icc 3 5) : have z := (v - 3) / (v - 1); 0 ≤ SwitchingPrinciple.jurkatRichertInnerIntegral v / v - goldbachPositiveScalarP z * goldbachPositiveScalarH z * (2 / (v - 1) ^ 2) ∧ SwitchingPrinciple.jurkatRichertInnerIntegral v / v - goldbachPositiveScalarP z * goldbachPositiveScalarH z * (2 / (v - 1) ^ 2) ≤ 1 / 10 ^ 8

Pointwise derivative comparison on every real point of the actual v-window.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarA_comp_hasDerivAt {v : ℝ} (hv : 3 ≤ v) : HasDerivAt (fun (v : ℝ) => goldbachPositiveScalarA ((v - 3) / (v - 1))) (goldbachPositiveScalarP ((v - 3) / (v - 1)) * goldbachPositiveScalarH ((v - 3) / (v - 1)) * (2 / (v - 1) ^ 2)) v

FTC derivative of the polynomial in the original variable.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalar_integral_bounds {b : ℝ} (hb : b ∈ Set.Icc 3 5) : goldbachPositiveScalarA ((b - 3) / (b - 1)) ≤ ∫ (v : ℝ) in 3..b, SwitchingPrinciple.jurkatRichertInnerIntegral v / v ∧ ∫ (v : ℝ) in 3..b, SwitchingPrinciple.jurkatRichertInnerIntegral v / v ≤ goldbachPositiveScalarA ((b - 3) / (b - 1)) + (b - 3) / 10 ^ 8

Integral sandwich for the literal existing lower-factor correction.