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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_scalarMainKernel s = (1 + MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertInnerIntegral (max s 3)) / (s * (53 / 8 - s))

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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_scalarCorrectionKernel s = (∫ (t : ℝ) in 5..s, (∫ (v : ℝ) in 3..t - 2, MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertInnerIntegral v / v) / (t - 1)) / (s * (53 / 8 - s))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_scalarMain_continuous : ContinuousOn goldbachS3_scalarMainKernel (Set.Icc (53 / 24) (45 / 8))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_scalarBody_low {s : ℝ} (hs : s ≤ 5) : (fun (s : ℝ) => (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))) s = goldbachS3_scalarMainKernel s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_scalarBody_high {s : ℝ} (hs : 5 ≤ s) : (fun (s : ℝ) => (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))) s = goldbachS3_scalarMainKernel s + goldbachS3_scalarCorrectionKernel s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_scalarCorrection_continuous : ContinuousOn goldbachS3_scalarCorrectionKernel (Set.Icc 5 (45 / 8))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_scalar_integral_split {a : ℝ} (ha : 53 / 24 ≤ a) (ha5 : a ≤ 5) : ∫ (s : ℝ) in a..45 / 8, (fun (s : ℝ) => (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))) s = (∫ (s : ℝ) in a..45 / 8, goldbachS3_scalarMainKernel s) + ∫ (s : ℝ) in 5..45 / 8, goldbachS3_scalarCorrectionKernel s

Exact separation of the common third-branch correction, with actual integrability.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_oneThird_integral_split : goldbachS3_oneThirdExpFreeIntegral = (∫ (s : ℝ) in 53 / 24..45 / 8, goldbachS3_scalarMainKernel s) + ∫ (s : ℝ) in 5..45 / 8, goldbachS3_scalarCorrectionKernel s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_threeElevenths_integral_split : goldbachS3_threeEleventhsExpFreeIntegral = (∫ (s : ℝ) in 265 / 88..45 / 8, goldbachS3_scalarMainKernel s) + ∫ (s : ℝ) in 5..45 / 8, goldbachS3_scalarCorrectionKernel s