theorem
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_author_actual_small_epsilon
(δ : ℝ)
:
Exact actual-count input expected by the existing final assembly. The small-epsilon window is furnished here, not assumed by a downstream caller.
Inspect dependencies
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachWeightG11_author_actual_small_epsilon · compiled type and proof/definition references.