theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbach_lowerFactor_continuousOn_four_six : ContinuousOn SwitchingPrinciple.dimensionOneLowerLinearSieveFactor (Set.Icc 4 6)

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

The third upper interval in same-source integrated-lower form. This is not yet the paper's reordered double-integral presentation.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachUpperThirdIntervalFactor s = (2 * Real.exp Real.eulerMascheroniConstant * (1 + MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertInnerIntegral 5) + ∫ (t : ℝ) in 5..s, MathlibNt.SieveTheory.SwitchingPrinciple.dimensionOneLowerLinearSieveFactor (t - 1)) / s

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbach_suzukiUpperFactor_eq_third {s : ℝ} (hs5 : 5 ≤ s) (hs7 : s ≤ 7) : suzukiContinuousUpperFactor s = goldbachUpperThirdIntervalFactor s

The actual source-series upper factor on the entire third interval. All source contracts and the amplitude normalization are supplied internally.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachUpperThirdIntervalFactor_continuousOn : ContinuousOn goldbachUpperThirdIntervalFactor (Set.Icc 5 7)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbach_suzukiUpperFactor_continuousOn_threeHalves_seven : ContinuousOn suzukiContinuousUpperFactor (Set.Icc (3 / 2) 7)

All three actual source intervals glue continuously, including 3 and 5.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbach_one_le_suzukiUpperFactor {s : ℝ} (hs : 1 < s) : 1 ≤ suzukiContinuousUpperFactor s

Nonnegative odd source layers give the sign needed for weighted upper sums.