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

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3E s = 53 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_innerEnvelope s / (s * (53 / 8 - s))

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3K (a y : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3K a y = -8 / (3 - a) * ∑ k ∈ Finset.range 64, (y / (3 - a)) ^ k + 360 / (29 - 45 * a) * (∑ k ∈ Finset.range 64, (45 * y / (29 - 45 * a)) ^ k + 5 / 2 * (3 / 5) ^ 64)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3kernel_majorant {a z : ℝ} (_ha : 0 ≤ a) (haz : a ≤ z) (hz : z ≤ 3 / 5) (_ha5 : a ≤ 1 / 2) (hu : 45 * (z - a) / (29 - 45 * a) ≤ 3 / 5) : -8 / (3 - z) + 360 / (29 - 45 * z) ≤ s3K a (z - a)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3E_continuousOn {l r : ℝ} (hl : 3 ≤ l) (hr : r ≤ 45 / 8) : ContinuousOn s3E (Set.Icc l r)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3segment_bound {l r a : ℝ} (q : List ℚ) (hl : 3 ≤ l) (hlr : l ≤ r) (hr : r ≤ 45 / 8) (ha : 0 ≤ a) (ha5 : a ≤ 1 / 2) (hdom : ∀ s ∈ Set.Icc l r, a ≤ (s - 3) / (s - 1) ∧ 45 * ((s - 3) / (s - 1) - a) / (29 - 45 * a) ≤ 3 / 5) (hq : ∀ (y : ℝ), s3eval q y = (goldbachS3_innerPolynomial 24 48 (a + y) + (a + y) / 10 ^ 9) * s3K a y) : ∫ (s : ℝ) in l..r, s3E s ≤ s3prim q ((r - 3) / (r - 1) - a) - s3prim q ((l - 3) / (l - 1) - a)