Documentation

MathlibNt.SieveTheory.LiLiuGoldbachG9AnalyticScalar

source
theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.endpoints_le_target :
endpointExpression ≤ 527231 / 100000
Inspect dependencies

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

source
theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.actual_le_target :
goldbachB9PaperSplitIntegral ≤ 527231 / 100000
Inspect dependencies

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