MathlibNt.SieveTheory.LiLiuGoldbachS3RetainedScalar

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_oneThird_scalar_le_retained236056871187 :

53 * goldbachS3_oneThirdExpFreeIntegral ≤ 236056871187 / 10000000000

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_threeElevenths_scalar_le_retained195190815363 :

53 * goldbachS3_threeEleventhsExpFreeIntegral ≤ 195190815363 / 10000000000

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_oneThird_coefficient_le_retained236056871187 :

53 / 2 * Real.exp (-Real.eulerMascheroniConstant) * goldbachS3_primeKernelIntegral (1 / 3) ≤ 236056871187 / 10000000000

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_threeElevenths_coefficient_le_retained195190815363 :

53 / 2 * Real.exp (-Real.eulerMascheroniConstant) * goldbachS3_primeKernelIntegral (3 / 11) ≤ 195190815363 / 10000000000

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_normalized_upper_retained236056871187 (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) :

∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachS3Closed (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (1 / 3))) ≤ ((1 - ε) * (236056871187 / 10000000000) + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Inspect dependencies

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

source

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS3_normalized_upper_retained195190815363 (δ ε : ℝ) (hδ : 0 < δ) (hε : 0 < ε) (hεu : ε < 2 / 15) :

∃ (N₀ : ℕ), 4 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → Even N → ↑(goldbachS3Closed (goldbachDifferenceCarrier N ε) N (↑N ^ (4 / 53)) (↑N ^ (3 / 11))) ≤ ((1 - ε) * (195190815363 / 10000000000) + δ) * (SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2)

Inspect dependencies

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