theorem
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1_lowerFactor_continuousAt_betaRatio :
The same actual integral formula used at five is continuous at the beta ratio.
Inspect dependencies
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1_lowerFactor_continuousAt_betaRatio · compiled type and proof/definition references.
theorem
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1_exists_betaRatio_below
(η : ℝ)
(hη : 0 < η)
:
∃ (s : ℝ),
4 ≤ s ∧ s < 33 / 8 ∧ SwitchingPrinciple.dimensionOneLowerLinearSieveFactor (33 / 8) - η ≤ SwitchingPrinciple.dimensionOneLowerLinearSieveFactor s
Choose a fixed admissible ratio strictly below the endpoint before selecting N.
Inspect dependencies
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachS1_exists_betaRatio_below · compiled type and proof/definition references.