Documentation

MathlibNt.SieveTheory.LiLiuGoldbachS3IntegralScalarMainBound

source
theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3base_integrable {a b : ℝ} (ha : 53 / 24 ≤ a) (hab : a ≤ b) (hb : b ≤ 45 / 8) :
IntervalIntegrable (fun (s : ℝ) => 1 / (s * (53 / 8 - s))) MeasureTheory.volume a b
Inspect dependencies

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

source
theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3main_integrable {a b : ℝ} (ha : 53 / 24 ≤ a) (hab : a ≤ b) (hb : b ≤ 45 / 8) :
IntervalIntegrable goldbachS3_scalarMainKernel MeasureTheory.volume a b
Inspect dependencies

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

source
theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3main_high_bound {a : ℝ} (ha : 3 ≤ a) (haU : a ≤ 45 / 8) :
53 * ∫ (s : ℝ) in a..45 / 8, goldbachS3_scalarMainKernel s ≤ (53 * ∫ (s : ℝ) in a..45 / 8, 1 / (s * (53 / 8 - s))) + ∫ (s : ℝ) in a..45 / 8, s3E s
Inspect dependencies

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

source
theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3main4_bound :
53 * ∫ (s : ℝ) in 53 / 24..45 / 8, goldbachS3_scalarMainKernel s ≤ ↑s3B4
Inspect dependencies

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

source
theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.s3main5_bound :
53 * ∫ (s : ℝ) in 265 / 88..45 / 8, goldbachS3_scalarMainKernel s ≤ ↑s3B5
Inspect dependencies

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