theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_inner_derivative_quadratic_majorant {t : ℝ} (ht : 3 ≤ t) : Real.log (t - 2) / (t - 1) ≤ (t - 3) / 2

A whole-interval pointwise bound for the derivative of the inner integral.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_inner_shift (s : ℝ) : SwitchingPrinciple.jurkatRichertInnerIntegral s = ∫ (t : ℝ) in 3..s, Real.log (t - 2) / (t - 1)

The shift needed for the analytic envelope, retaining the actual inner integral.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_inner_kernel_continuousOn {a b : ℝ} (ha : 3 ≤ a) : ContinuousOn (fun (t : ℝ) => Real.log (t - 2) / (t - 1)) (Set.Icc a b)

Local analytic regularity used in the envelope comparison.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_inner_quadratic_majorant {s : ℝ} (hs : 3 ≤ s) : SwitchingPrinciple.jurkatRichertInnerIntegral s ≤ (s - 3) ^ 2 / 4

A closed, quadratic envelope for the actual inner integral.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_inner_continuousOn {b : ℝ} (hb : 3 ≤ b) : ContinuousOn SwitchingPrinciple.jurkatRichertInnerIntegral (Set.Icc 3 b)

Inner-integral continuity on arbitrary compact positive ranges.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_nested_inner_cubic_majorant {t : ℝ} (ht : 5 ≤ t) : ∫ (v : ℝ) in 3..t - 2, SwitchingPrinciple.jurkatRichertInnerIntegral v / v ≤ (t - 5) ^ 3 / 36

The inner correction has a cubic envelope, with no discarded nested term.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_nested_inner_continuousOn {b : ℝ} (hb : 5 ≤ b) : ContinuousOn (fun (t : ℝ) => ∫ (v : ℝ) in 3..t - 2, SwitchingPrinciple.jurkatRichertInnerIntegral v / v) (Set.Icc 5 b)

Continuity of the inner correction as a function of the upper variable.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_nested_quartic_majorant {s : ℝ} (hs : 5 ≤ s) : ∫ (t : ℝ) in 5..s, (∫ (v : ℝ) in 3..t - 2, SwitchingPrinciple.jurkatRichertInnerIntegral v / v) / (t - 1) ≤ (s - 5) ^ 4 / 576

The actual third-branch correction is bounded by a quartic on its whole domain.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_inner_increment {s : ℝ} (hs : 5 ≤ s) : SwitchingPrinciple.jurkatRichertInnerIntegral 5 + ∫ (t : ℝ) in 5..s, Real.log (t - 2) / (t - 1) = SwitchingPrinciple.jurkatRichertInnerIntegral s

The log part of the third branch is exactly the increment of the inner integral.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_third_body_split {s : ℝ} (hs : 5 ≤ s) : 1 + SwitchingPrinciple.jurkatRichertInnerIntegral 5 + ∫ (t : ℝ) in 5..s, (Real.log (t - 2) + ∫ (v : ℝ) in 3..t - 2, SwitchingPrinciple.jurkatRichertInnerIntegral v / v) / (t - 1) = 1 + SwitchingPrinciple.jurkatRichertInnerIntegral s + ∫ (t : ℝ) in 5..s, (∫ (v : ℝ) in 3..t - 2, SwitchingPrinciple.jurkatRichertInnerIntegral v / v) / (t - 1)

The third numerator is the full inner integral plus its genuine correction.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_full_rational_majorant {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)) ≤ (1 + max (s - 3) 0 ^ 2 / 4 + max (s - 5) 0 ^ 4 / 576) / (s * (53 / 8 - s))

A concrete, whole-range rational envelope. This is not the requested decimal bound.