Equations
- MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarP z = 0 / 1 + z * (0 / 1 + z * (1 / 1 + z * (2 / 3 + z * (2 / 3 + z * (8 / 15 + z * (23 / 45 + z * (46 / 105 + z * (44 / 105 + z * (352 / 945 + z * (563 / 1575 + z * (1126 / 3465 + z * (3254 / 10395 + z * (13016 / 45045 + z * (88069 / 315315 + z * (176138 / 675675 + z * (11384 / 45045 + z * (182144 / 765765 + z * (1593269 / 6891885 + z * (3186538 / 14549535 + z * (15518938 / 72747675 + z * (62075752 / 305540235 + z * (31730711 / 160044885 + z * (63461422 / 334639305 + z * (186088972 / 1003917915 + z * ⋯))))))))))))))))))))))))
Instances For
Inspect dependencies
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarP · compiled type and proof/definition references.
Equations
- MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarH z = 2 / 3 + z * (8 / 9 + z * (26 / 27 + z * (80 / 81 + z * (242 / 243 + z * (728 / 729 + z * (2186 / 2187 + z * (6560 / 6561 + z * (19682 / 19683 + z * (59048 / 59049 + z * (177146 / 177147 + z * (531440 / 531441 + z * (1594322 / 1594323 + z * (4782968 / 4782969 + z * (14348906 / 14348907 + z * (43046720 / 43046721 + z * (129140162 / 129140163 + z * (387420488 / 387420489 + z * (1162261466 / 1162261467 + z * (3486784400 / 3486784401 + z * (10460353202 / 10460353203 + z * (31381059608 / 31381059609 + z * (94143178826 / 94143178827 + z * (282429536480 / 282429536481 + z * (847288609442 / 847288609443 + z * ⋯))))))))))))))))))))))))
Instances For
Inspect dependencies
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarH · compiled type and proof/definition references.
Equations
- MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarA z = 0 / 1 + z * (0 / 1 + z * (0 / 1 + z * (2 / 9 + z * (1 / 3 + z * (2 / 5 + z * (58 / 135 + z * (4 / 9 + z * (47 / 105 + z * (3796 / 8505 + z * (2084 / 4725 + z * (22586 / 51975 + z * (66527 / 155925 + z * (40406 / 96525 + z * (387962 / 945945 + z * (28510936 / 70945875 + z * (1861507 / 4729725 + z * (10335128 / 26801775 + z * (820143224 / 2170943775 + z * (1697133346 / 4583103525 + z * (1188383461 / 3273645375 + z * (34269600082 / 96245174025 + z * (320199806 / 916620705 + z * (3341153524 / 9743909175 + z * (1171148993093 / 3478575575475 + z * ⋯))))))))))))))))))))))))
Instances For
Inspect dependencies
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarA · compiled type and proof/definition references.
Inspect dependencies
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarP_eq · compiled type and proof/definition references.
Inspect dependencies
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarH_eq · compiled type and proof/definition references.
Inspect dependencies
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarP_nonneg · compiled type and proof/definition references.
Inspect dependencies
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarA_zero · compiled type and proof/definition references.
Inspect dependencies
MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachPositiveScalarA_hasDerivAt · compiled type and proof/definition references.