MathlibNt.SieveTheory.LiLiuGoldbachS3IntegralScalarInnerBounds

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3segment0_domain {s : ℝ} (hs : s ∈ Set.Icc 3 4) :

0 ≤ (s - 3) / (s - 1) ∧ 45 * ((s - 3) / (s - 1) - 0) / (29 - 45 * 0) ≤ 3 / 5

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3segment0_domain · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3segment1_domain {s : ℝ} (hs : s ∈ Set.Icc 4 5) :

1 / 3 ≤ (s - 3) / (s - 1) ∧ 45 * ((s - 3) / (s - 1) - 1 / 3) / (29 - 45 * (1 / 3)) ≤ 3 / 5

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3segment1_domain · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3segment2_domain {s : ℝ} (hs : s ∈ Set.Icc 5 (45 / 8)) :

1 / 2 ≤ (s - 3) / (s - 1) ∧ 45 * ((s - 3) / (s - 1) - 1 / 2) / (29 - 45 * (1 / 2)) ≤ 3 / 5

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3segment2_domain · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3integral0_bound :

∫ (s : ℝ) in 3..4, s3E s ≤ ↑s3j0

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3integral0_bound · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3integral0b_bound :

∫ (s : ℝ) in 265 / 88..4, s3E s ≤ ↑s3j0b

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3integral0b_bound · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3integral1_bound :

∫ (s : ℝ) in 4..5, s3E s ≤ ↑s3j1

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3integral1_bound · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3integral2_bound :

∫ (s : ℝ) in 5..45 / 8, s3E s ≤ ↑s3j2

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3integral2_bound · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3E_integrable {a b : ℝ} (ha : 3 ≤ a) (hab : a ≤ b) (hb : b ≤ 45 / 8) :

IntervalIntegrable s3E MeasureTheory.volume a b

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3E_integrable · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3I4_bound :

∫ (s : ℝ) in 3..45 / 8, s3E s ≤ ↑s3j0 + ↑s3j1 + ↑s3j2

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3I4_bound · compiled type and proof/definition references.

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3I5_bound :

∫ (s : ℝ) in 265 / 88..45 / 8, s3E s ≤ ↑s3j0b + ↑s3j1 + ↑s3j2

Inspect dependencies

MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3I5_bound · compiled type and proof/definition references.