noncomputable def
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12SharpIntegralConstant :
Original author sieve weight with both source-certified Buchstab branches.
Equations
Instances For
Inspect dependencies
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12SharpIntegralConstant · compiled type and proof/definition references.
theorem
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g12Sharp_authorLowHigh_integral_budget
(δ : ℝ)
(hδ : 0 < δ)
:
∃ (K : ℕ),
4 ≤ K ∧ ∀ N ≥ K,
∀ (ε : ℝ),
Real.log ↑N / ↑N * 400 * (goldbachG12AuthorLowMotherMass N ε + 8 * G12ClippedWindow.highMass N ε) ≤ goldbachG12SharpIntegralConstant + δ
Actual low mother and ungated high mass, with both approximation losses paid.
Inspect dependencies
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g12Sharp_authorLowHigh_integral_budget · compiled type and proof/definition references.