Documentation

MathlibNt.SieveTheory.LiLiuGoldbachG12EvaluationScalar

source
theorem G12AnalyticCertificate.rationalIntegral_le_target :
2 * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L (1 / 2) * endpoints ≤ 66821 / 100000

Fixed endpoint log estimates close the original rational envelope.

Inspect dependencies

G12AnalyticCertificate.rationalIntegral_le_target · compiled type and proof/definition references.

source
theorem G12AnalyticCertificate.actual_le_target :
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12SharpIntegralConstant ≤ 66821 / 100000

Unconditional bound for the production sharp G12 integral constant.

Inspect dependencies

G12AnalyticCertificate.actual_le_target · compiled type and proof/definition references.