noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L (x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L x = 1 / 1 * x ^ 1 + -1 / 2 * x ^ 2 + 1 / 3 * x ^ 3 + -1 / 4 * x ^ 4 + 1 / 5 * x ^ 5 + -1 / 6 * x ^ 6 + 1 / 7 * x ^ 7 + -1 / 8 * x ^ 8 + 1 / 9 * x ^ 9 + -1 / 10 * x ^ 10 + 1 / 11 * x ^ 11 + -1 / 12 * x ^ 12 + 1 / 13 * x ^ 13 + -1 / 14 * x ^ 14 + 1 / 15 * x ^ 15 + -1 / 16 * x ^ 16 + 1 / 17 * x ^ 17 + -1 / 18 * x ^ 18 + 1 / 19 * x ^ 19 + -1 / 20 * x ^ 20 + 1 / 21 * x ^ 21 + -1 / 22 * x ^ 22 + 1 / 23 * x ^ 23 + -1 / 24 * x ^ 24 + 1 / 25 * x ^ 25 + -1 / 26 * x ^ 26 + 1 / 27 * x ^ 27 + -1 / 28 * x ^ 28 + 1 / 29 * x ^ 29 + -1 / 30 * x ^ 30 + 1 / 31 * x ^ 31 + -1 / 32 * x ^ 32 + 1 / 33 * x ^ 33

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.dL (x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.dL x = 1 / 1 * x ^ 0 + -1 / 1 * x ^ 1 + 1 / 1 * x ^ 2 + -1 / 1 * x ^ 3 + 1 / 1 * x ^ 4 + -1 / 1 * x ^ 5 + 1 / 1 * x ^ 6 + -1 / 1 * x ^ 7 + 1 / 1 * x ^ 8 + -1 / 1 * x ^ 9 + 1 / 1 * x ^ 10 + -1 / 1 * x ^ 11 + 1 / 1 * x ^ 12 + -1 / 1 * x ^ 13 + 1 / 1 * x ^ 14 + -1 / 1 * x ^ 15 + 1 / 1 * x ^ 16 + -1 / 1 * x ^ 17 + 1 / 1 * x ^ 18 + -1 / 1 * x ^ 19 + 1 / 1 * x ^ 20 + -1 / 1 * x ^ 21 + 1 / 1 * x ^ 22 + -1 / 1 * x ^ 23 + 1 / 1 * x ^ 24 + -1 / 1 * x ^ 25 + 1 / 1 * x ^ 26 + -1 / 1 * x ^ 27 + 1 / 1 * x ^ 28 + -1 / 1 * x ^ 29 + 1 / 1 * x ^ 30 + -1 / 1 * x ^ 31 + 1 / 1 * x ^ 32

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.A (x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.A x = 1 / 4 * x ^ 2 + -1 / 6 * x ^ 3 + 5 / 48 * x ^ 4 + -1 / 15 * x ^ 5 + 2 / 45 * x ^ 6 + -13 / 420 * x ^ 7 + 151 / 6720 * x ^ 8 + -16 / 945 * x ^ 9 + 83 / 6300 * x ^ 10 + -73 / 6930 * x ^ 11 + 1433 / 166320 * x ^ 12 + -647 / 90090 * x ^ 13 + 15341 / 2522520 * x ^ 14 + -28211 / 5405400 * x ^ 15 + 10447 / 2306304 * x ^ 16 + -608 / 153153 * x ^ 17 + 19345 / 5513508 * x ^ 18 + -18181 / 5819814 * x ^ 19 + 130349 / 46558512 * x ^ 20 + -771079 / 305540235 * x ^ 21 + 731957 / 320089770 * x ^ 22 + -2786599 / 1338557220 * x ^ 23 + 122289917 / 64250746560 * x ^ 24 + -14614772 / 8365982625 * x ^ 25 + 140001721 / 87006219300 * x ^ 26 + -134354573 / 90352612350 * x ^ 27 + 774885169 / 562194032400 * x ^ 28 + -745984697 / 582272390700 * x ^ 29 + 41711914513 / 34936343442000 * x ^ 30 + -80530073893 / 72201776446800 * x ^ 31 + 4825521853483 / 4620913692595200 * x ^ 32 + -145908326272 / 148916163921525 * x ^ 33 + 282654114997 / 306857549898900 * x ^ 34

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.dA (x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.dA x = 1 / 2 * x ^ 1 + -1 / 2 * x ^ 2 + 5 / 12 * x ^ 3 + -1 / 3 * x ^ 4 + 4 / 15 * x ^ 5 + -13 / 60 * x ^ 6 + 151 / 840 * x ^ 7 + -16 / 105 * x ^ 8 + 83 / 630 * x ^ 9 + -73 / 630 * x ^ 10 + 1433 / 13860 * x ^ 11 + -647 / 6930 * x ^ 12 + 15341 / 180180 * x ^ 13 + -28211 / 360360 * x ^ 14 + 10447 / 144144 * x ^ 15 + -608 / 9009 * x ^ 16 + 19345 / 306306 * x ^ 17 + -18181 / 306306 * x ^ 18 + 651745 / 11639628 * x ^ 19 + -771079 / 14549535 * x ^ 20 + 731957 / 14549535 * x ^ 21 + -2786599 / 58198140 * x ^ 22 + 122289917 / 2677114440 * x ^ 23 + -14614772 / 334639305 * x ^ 24 + 140001721 / 3346393050 * x ^ 25 + -134354573 / 3346393050 * x ^ 26 + 774885169 / 20078358300 * x ^ 27 + -745984697 / 20078358300 * x ^ 28 + 41711914513 / 1164544781400 * x ^ 29 + -80530073893 / 2329089562800 * x ^ 30 + 4825521853483 / 144403552893600 * x ^ 31 + -145908326272 / 4512611027925 * x ^ 32 + 282654114997 / 9025222055850 * x ^ 33

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.B (x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.B x = 1 / 36 * x ^ 3 + -1 / 48 * x ^ 4 + 1 / 80 * x ^ 5 + -31 / 4320 * x ^ 6 + 1 / 240 * x ^ 7 + -101 / 40320 * x ^ 8 + 857 / 544320 * x ^ 9 + -209 / 201600 * x ^ 10 + 113 / 158400 * x ^ 11 + -20381 / 39916800 * x ^ 12 + 5449 / 14414400 * x ^ 13 + -19373 / 67267200 * x ^ 14 + 1020473 / 4540536000 * x ^ 15 + -96307 / 538137600 * x ^ 16 + 2983909 / 20583763200 * x ^ 17 + -132441653 / 1111523212800 * x ^ 18 + 994603 / 10027987200 * x ^ 19 + -217640447 / 2607276672000 * x ^ 20 + 582617647 / 8212921516800 * x ^ 21 + -15854533 / 260727667200 * x ^ 22 + 192502439 / 3664672211200 * x ^ 23 + -108509804233 / 2374707592857600 * x ^ 24 + 98945425471 / 2473653742560000 * x ^ 25 + -3109808431 / 88304344128000 * x ^ 26 + 48713603345471 / 1562854434549408000 * x ^ 27 + -4992093221933 / 180081992458368000 * x ^ 28 + 4618926518431 / 186513492189024000 * x ^ 29 + -372902687177539 / 16786214297012160000 * x ^ 30 + 115662301113083 / 5781918257859744000 * x ^ 31 + -371643690809519 / 20557931583501312000 * x ^ 32 + 37530909745825099 / 2289639630112458624000 * x ^ 33 + -11723613013608371 / 786340883068925184000 * x ^ 34 + 561460485694698467 / 41282896361118572160000 * x ^ 35

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.dB (x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.dB x = 1 / 12 * x ^ 2 + -1 / 12 * x ^ 3 + 1 / 16 * x ^ 4 + -31 / 720 * x ^ 5 + 7 / 240 * x ^ 6 + -101 / 5040 * x ^ 7 + 857 / 60480 * x ^ 8 + -209 / 20160 * x ^ 9 + 113 / 14400 * x ^ 10 + -20381 / 3326400 * x ^ 11 + 5449 / 1108800 * x ^ 12 + -19373 / 4804800 * x ^ 13 + 1020473 / 302702400 * x ^ 14 + -96307 / 33633600 * x ^ 15 + 2983909 / 1210809600 * x ^ 16 + -132441653 / 61751289600 * x ^ 17 + 994603 / 527788800 * x ^ 18 + -217640447 / 130363833600 * x ^ 19 + 582617647 / 391091500800 * x ^ 20 + -15854533 / 11851257600 * x ^ 21 + 192502439 / 159333574400 * x ^ 22 + -108509804233 / 98946149702400 * x ^ 23 + 98945425471 / 98946149702400 * x ^ 24 + -3109808431 / 3396320928000 * x ^ 25 + 48713603345471 / 57883497575904000 * x ^ 26 + -4992093221933 / 6431499730656000 * x ^ 27 + 4618926518431 / 6431499730656000 * x ^ 28 + -372902687177539 / 559540476567072000 * x ^ 29 + 115662301113083 / 186513492189024000 * x ^ 30 + -371643690809519 / 642435361984416000 * x ^ 31 + 37530909745825099 / 69383019094316928000 * x ^ 32 + -11723613013608371 / 23127673031438976000 * x ^ 33 + 561460485694698467 / 1179511324603387776000 * x ^ 34

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.D (x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.D x = 1 / 576 * x ^ 4 + -1 / 720 * x ^ 5 + 7 / 8640 * x ^ 6 + -13 / 30240 * x ^ 7 + 31 / 138240 * x ^ 8 + -13 / 108864 * x ^ 9 + 103 / 1555200 * x ^ 10 + -289 / 7484400 * x ^ 11 + 34073 / 1437004800 * x ^ 12 + -541 / 35380800 * x ^ 13 + 112243 / 10897286400 * x ^ 14 + -1177457 / 163459296000 * x ^ 15 + 235493 / 45287424000 * x ^ 16 + -3571081 / 926269344000 * x ^ 17 + 97492141 / 33345696384000 * x ^ 18 + -59667793 / 26398676304000 * x ^ 19 + 7503960929 / 4223788208640000 * x ^ 20 + -142800211 / 100794945888000 * x ^ 21 + 18606705181 / 16261584603264000 * x ^ 22 + -15888576559 / 17000747539776000 * x ^ 23 + 13843209331597 / 17952789402003456000 * x ^ 24 + -1500743677031 / 2337602786719200000 * x ^ 25 + 13102201899587 / 24311068981879680000 * x ^ 26 + -212503304071 / 466192373942295000 * x ^ 27 + 2378186584388413 / 6126389383433679360000 * x ^ 28 + -40594133889601 / 122022865466742240000 * x ^ 29 + 89782826505979 / 313084983763351800000 * x ^ 30 + -97772587134372487 / 393401718264776981760000 * x ^ 31 + 10900613168899714417 / 50355419937891453665280000 * x ^ 32 + -1229627483809823321 / 6491128351368820199040000 * x ^ 33 + 24496306015856387543 / 147132242631026591178240000 * x ^ 34 + -94577488609855608571 / 643703561510741336404800000 * x ^ 35 + 98488038567669650177 / 756680104959565326059520000 * x ^ 36

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.dD (x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.dD x = 1 / 144 * x ^ 3 + -1 / 144 * x ^ 4 + 7 / 1440 * x ^ 5 + -13 / 4320 * x ^ 6 + 31 / 17280 * x ^ 7 + -13 / 12096 * x ^ 8 + 103 / 155520 * x ^ 9 + -289 / 680400 * x ^ 10 + 34073 / 119750400 * x ^ 11 + -541 / 2721600 * x ^ 12 + 112243 / 778377600 * x ^ 13 + -1177457 / 10897286400 * x ^ 14 + 235493 / 2830464000 * x ^ 15 + -3571081 / 54486432000 * x ^ 16 + 97492141 / 1852538688000 * x ^ 17 + -59667793 / 1389404016000 * x ^ 18 + 7503960929 / 211189410432000 * x ^ 19 + -142800211 / 4799759328000 * x ^ 20 + 18606705181 / 739162936512000 * x ^ 21 + -15888576559 / 739162936512000 * x ^ 22 + 13843209331597 / 748032891750144000 * x ^ 23 + -1500743677031 / 93504111468768000 * x ^ 24 + 13102201899587 / 935041114687680000 * x ^ 25 + -212503304071 / 17266384220085000 * x ^ 26 + 2378186584388413 / 218799620836917120000 * x ^ 27 + -40594133889601 / 4207685016094560000 * x ^ 28 + 89782826505979 / 10436166125445060000 * x ^ 29 + -97772587134372487 / 12690378008541192960000 * x ^ 30 + 10900613168899714417 / 1573606873059107927040000 * x ^ 31 + -1229627483809823321 / 196700859132388490880000 * x ^ 32 + 24496306015856387543 / 4327418900912546799360000 * x ^ 33 + -94577488609855608571 / 18391530328878323897280000 * x ^ 34 + 98488038567669650177 / 21018891804432370168320000 * x ^ 35

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.H (x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.H x = 1 / 2880 * x ^ 4 + -1 / 2880 * x ^ 5 + 1 / 4320 * x ^ 6 + -1 / 7560 * x ^ 7 + 23 / 322560 * x ^ 8 + -1661 / 43545600 * x ^ 9 + 101 / 4838400 * x ^ 10 + -5699 / 479001600 * x ^ 11 + 731 / 102643200 * x ^ 12 + -41869 / 9340531200 * x ^ 13 + 966541 / 326918592000 * x ^ 14 + -664291 / 326918592000 * x ^ 15 + 15131239 / 10461394944000 * x ^ 16 + -26939389 / 25406244864000 * x ^ 17 + 85024057 / 106706228428800 * x ^ 18 + -632443223 / 1034397112320000 * x ^ 19 + 4841489963 / 10137091700736000 * x ^ 20 + -26884355657 / 70959641905152000 * x ^ 21 + 237769952183 / 780556060956672000 * x ^ 22 + -3178149392359 / 12823421001431040000 * x ^ 23 + 5081282911361 / 24934429725004800000 * x ^ 24 + -2530705855963 / 14960657835002880000 * x ^ 25 + 27543358264843 / 194488551855037440000 * x ^ 26 + -627461578041301 / 5251190900086010880000 * x ^ 27 + 196435268974943 / 1934649278979056640000 * x ^ 28 + -462866186864747929 / 5329958763587301043200000 * x ^ 29 + 26551053670700459 / 355330584239153402880000 * x ^ 30 + -799262649507103 / 12362792493169198080000 * x ^ 31 + 1524505674539146487 / 27114456889633859665920000 * x ^ 32 + -571501077072899446831 / 11632102005652925796679680000 * x ^ 33 + 42638553595550275453919 / 988728670480498692717772800000 * x ^ 34 + -442140179059502329927 / 11632102005652925796679680000 * x ^ 35 + 19952754273817524913009 / 593237202288299215630663680000 * x ^ 36

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.G (x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.G x = 8 / 13 * x ^ 0 + 64 / 169 * x ^ 1 + 512 / 2197 * x ^ 2 + 4096 / 28561 * x ^ 3 + 32768 / 371293 * x ^ 4 + 262144 / 4826809 * x ^ 5 + 2097152 / 62748517 * x ^ 6 + 16777216 / 815730721 * x ^ 7 + 134217728 / 10604499373 * x ^ 8 + 1073741824 / 137858491849 * x ^ 9 + 8589934592 / 1792160394037 * x ^ 10 + 68719476736 / 23298085122481 * x ^ 11 + 549755813888 / 302875106592253 * x ^ 12 + 4398046511104 / 3937376385699289 * x ^ 13 + 35184372088832 / 51185893014090757 * x ^ 14 + 281474976710656 / 665416609183179841 * x ^ 15 + 2251799813685248 / 8650415919381337933 * x ^ 16 + 18014398509481984 / 112455406951957393129 * x ^ 17 + 144115188075855872 / 1461920290375446110677 * x ^ 18 + 1152921504606846976 / 19004963774880799438801 * x ^ 19 + 9223372036854775808 / 247064529073450392704413 * x ^ 20 + 73786976294838206464 / 3211838877954855105157369 * x ^ 21 + 590295810358705651712 / 41753905413413116367045797 * x ^ 22 + 4722366482869645213696 / 542800770374370512771595361 * x ^ 23 + 4722366482869645213696 / 542800770374370512771595361 * x ^ 24

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.K (x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.K x = ⋯ + -26783361149 / 16280680022006400 * x ^ 11 + 3209893097993 / 952419781287374400 * x ^ 12 + -564978984907 / 825430477115724480 * x ^ 13 + 7876771691869393 / 5633563006314819576000 * x ^ 14 + -816113767825969 / 2092466259488361556800 * x ^ 15 + 1800475262617030873 / 2769664430740958569728000 * x ^ 16 + -339988450722463988551 / 1346610846226254056601753600 * x ^ 17 + 17591947509441659105197 / 52517823002823908207468390400 * x ^ 18 + -6129864781041490906078367 / 36033061893604181464568590080000 * x ^ 19 + 72520879285415794790474321 / 383260749231971748304956821760000 * x ^ 20 + -44773622266961765947251370949 / 383644009981203720053261778581760000 * x ^ 21 + 906280876868454016143107092169 / 7837299061044590281088062048170240000 * x ^ 22 + -38128880385610382861651465348443 / 468670483850466498809066110480580352000 * x ^ 23 + 40165659033382719885933891336402473 / 533112675379905642395312700671660150400000 * x ^ 24 + -3306729954502240154078496614876741 / 57276568429246060753215414121748611200000 * x ^ 25 + 4650993294970404840349774269724913357 / 90096042139204053564807846413510565417600000 * x ^ 26 + -440245979214421218626282468643801044861 / 10541236930286874267082518030380736153859200000 * x ^ 27 + 71790912285085339158050094935127172307 / 1892016884923285124860964774683721873769600000 * x ^ 28 + -14171107033886272571048106987215701141001 / 427974219369647095243550232033457887846683520000 * x ^ 29 + 2417175927167815282457043751981917980017 / 85594843873929419048710046406691577569336704000 * x ^ 30 + -319588935156882967219891399145287757298587 / 13267200800459059952550057193037194523247189120000 * x ^ 31 + 1759582118348152470164693008828708643103833 / 84910085122937983696320366035438044948782010368000 * x ^ 32 + -1333673527213749381683090293630453261125701 / 74127852091453795290438414792842737653698580480000 * x ^ 33 + 6248298926273757545376626752777360106348333867 / 396954647949735073780297711215672860135555898470400000 * x ^ 34 + -1833406012057624157343232908606437030553264421 / 132318215983245024593432570405224286711851966156800000 * x ^ 35 + 189774979517205025631871282395121447139845792293 / 15481231270039667877431610737411241545286680040345600000 * x ^ 36 + 14495264583690450527104539474974406216700349561 / 1935153908754958484678951342176405193160835005043200000 * x ^ 37 + 86401426177700180708982523991229606710329169 / 18607249122643831583451455213234665318854182740800000 * x ^ 38 + 85717226709274885333959075970252086076882769 / 30236779824296226323108614721506331143138046953800000 * x ^ 39 + 511772560720450506741221241018477598993001 / 290738267541309868491428987706791645607096605325000 * x ^ 40 + 506437744936889098182315905221333296605801 / 472449684754628536298572105023536424111531983653125 * x ^ 41 + 315595718614498108254654350444628494976616 / 472449684754628536298572105023536424111531983653125 * x ^ 42 + 10064774624286621982598540906808825861824 / 24865772881822554542030110790712443374291157034375 * x ^ 43 + 119981997279616996714411935939098793150976 / 472449684754628536298572105023536424111531983653125 * x ^ 44 + 72028070427530610527195367641378505199616 / 472449684754628536298572105023536424111531983653125 * x ^ 45 + 45764848759630633073375105526264191942656 / 472449684754628536298572105023536424111531983653125 * x ^ 46 + 27000674213850791927015138351480100356096 / 472449684754628536298572105023536424111531983653125 * x ^ 47 + 17564853026366575495904169155340110135296 / 472449684754628536298572105023536424111531983653125 * x ^ 48 + 130341389743465247775068812526421851242496 / 6141845901810170971881437365305973513449915787490625 * x ^ 49 + 88682903641571486719153170057089511325696 / 6141845901810170971881437365305973513449915787490625 * x ^ 50 + 47461600731902214502790172060922639548416 / 6141845901810170971881437365305973513449915787490625 * x ^ 51 + 35222957873055726990120662615485239525376 / 6141845901810170971881437365305973513449915787490625 * x ^ 52 + 16552185015938022490204606439352776523776 / 6141845901810170971881437365305973513449915787490625 * x ^ 53 + 14577209650392451462503471607492145840128 / 6141845901810170971881437365305973513449915787490625 * x ^ 54 + 5184868918903864373386170845488341843968 / 6141845901810170971881437365305973513449915787490625 * x ^ 55 + 6472071494500249796829281959408197173248 / 6141845901810170971881437365305973513449915787490625 * x ^ 56 + 50018875081963704033839488176226304 / 273250251448599500461869349348488388728474253125 * x ^ 57 + 3193701439602228155415827065235600048128 / 6141845901810170971881437365305973513449915787490625 * x ^ 58 + -46772491663892703768830942310104563712 / 1228369180362034194376287473061194702689983157498125 * x ^ 59 + 359436866850318706846891350231252729856 / 1228369180362034194376287473061194702689983157498125 * x ^ 60

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.T (x : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.T x = ⋯ + -26783361149 / 195368160264076800 * x ^ 12 + 3209893097993 / 12381457156735867200 * x ^ 13 + -564978984907 / 11556026679620142720 * x ^ 14 + 7876771691869393 / 84503445094722293640000 * x ^ 15 + -816113767825969 / 33479460151813784908800 * x ^ 16 + 1800475262617030873 / 47084295322596295685376000 * x ^ 17 + -339988450722463988551 / 24238995232072573018831564800 * x ^ 18 + 17591947509441659105197 / 997838637053654255941899417600 * x ^ 19 + -6129864781041490906078367 / 720661237872083629291371801600000 * x ^ 20 + 72520879285415794790474321 / 8048475733871406714404093256960000 * x ^ 21 + -44773622266961765947251370949 / 8440168219586481841171759128798720000 * x ^ 22 + 906280876868454016143107092169 / 180257878404025576465025427107915520000 * x ^ 23 + -38128880385610382861651465348443 / 11248091612411195971417586651533928448000 * x ^ 24 + 40165659033382719885933891336402473 / 13327816884497641059882817516791503760000000 * x ^ 25 + -3306729954502240154078496614876741 / 1489190779160397579583600767165463891200000 * x ^ 26 + 4650993294970404840349774269724913357 / 2432593137758509446249811853164785266275200000 * x ^ 27 + -440245979214421218626282468643801044861 / 295154634048032479478310504850660612308057600000 * x ^ 28 + 71790912285085339158050094935127172307 / 54868489662775268620967978465827934339318400000 * x ^ 29 + -14171107033886272571048106987215701141001 / 12839226581089412857306506961003736635400505600000 * x ^ 30 + 2417175927167815282457043751981917980017 / 2653440160091811990510011438607438904649437824000 * x ^ 31 + -319588935156882967219891399145287757298587 / 424550425614689918481601830177190224743910051840000 * x ^ 32 + 1759582118348152470164693008828708643103833 / 2802032809056953461978572079169455483309806342144000 * x ^ 33 + -1333673527213749381683090293630453261125701 / 2520346971109429039874906102956653080225751736320000 * x ^ 34 + 6248298926273757545376626752777360106348333867 / 13893412678240727582310419892548550104744456446464000000 * x ^ 35 + -1833406012057624157343232908606437030553264421 / 4763455775396820885363572534588074321626670781644800000 * x ^ 36 + 189774979517205025631871282395121447139845792293 / 572805556991467711464969597284215937175607161492787200000 * x ^ 37 + 14495264583690450527104539474974406216700349561 / 73535848532688422417800151002703397340111730191641600000 * x ^ 38 + 86401426177700180708982523991229606710329169 / 725682715783109431754606753316151947435313126891200000 * x ^ 39 + 85717226709274885333959075970252086076882769 / 1209471192971849052924344588860253245725521878152000000 * x ^ 40 + 511772560720450506741221241018477598993001 / 11920268969193704608148588495978457469890960818325000 * x ^ 41 + 506437744936889098182315905221333296605801 / 19842886759694398524540028410988529812684343313431250 * x ^ 42 + 315595718614498108254654350444628494976616 / 20315336444449027060838600516012066236795875297084375 * x ^ 43 + 2516193656071655495649635226702206465456 / 273523501700048099962331218697836877117202727378125 * x ^ 44 + 119981997279616996714411935939098793150976 / 21260235813958284133435744726059139085018939264390625 * x ^ 45 + 36014035213765305263597683820689252599808 / 10866342749356456334867158415541337754565235624021875 * x ^ 46 + 45764848759630633073375105526264191942656 / 22205135183467541206032888936106211933242003231696875 * x ^ 47 + 1687542138365674495438446146967506272256 / 1417349054263885608895716315070609272334595950959375 * x ^ 48 + 17564853026366575495904169155340110135296 / 23150034552976798278630033146153284781465067199003125 * x ^ 49 + 65170694871732623887534406263210925621248 / 153546147545254274297035934132649337836247894687265625 * x ^ 50 + 88682903641571486719153170057089511325696 / 313234140992318719565953305630604649185945705162021875 * x ^ 51 + 11865400182975553625697543015230659887104 / 79843996723532222634458685748977655674848905237378125 * x ^ 52 + 35222957873055726990120662615485239525376 / 325517832795939061509716180361216596212845536737003125 * x ^ 53 + 8276092507969011245102303219676388261888 / 165829839348874616240798808863261284863147726262246875 * x ^ 54 + 14577209650392451462503471607492145840128 / 337801524599559403453479055091828543239745368311984375 * x ^ 55 + 648108614862983046673271355686042730496 / 42992921312671196803170061557141814594149410512434375 * x ^ 56 + 6472071494500249796829281959408197173248 / 350085216403179745397241929822440490266645199886965625 * x ^ 57 + 25009437540981852016919744088113152 / 7924257292009385513394211131106163273125753340625 * x ^ 58 + 3193701439602228155415827065235600048128 / 362368908206800087341004804553052437293545031461946875 * x ^ 59 + -11693122915973175942207735577526140928 / 18425537705430512915644312095917920540349747362471875 * x ^ 60 + 359436866850318706846891350231252729856 / 74930520002084085856953535856732876864088972607385625 * x ^ 61

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L_deriv (x : ℝ) : HasDerivAt L (dL x) x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.A_deriv (x : ℝ) : HasDerivAt A (dA x) x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.B_deriv (x : ℝ) : HasDerivAt B (dB x) x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.D_deriv (x : ℝ) : HasDerivAt D (dD x) x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.T_deriv (x : ℝ) : HasDerivAt T (K x) x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L_zero : L 0 = 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.A_zero : A 0 = 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.B_zero : B 0 = 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.D_zero : D 0 = 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.T_zero : T 0 = 0

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.dA_residual (x : ℝ) : (2 + x) * dA x - L x = 282654114997 / 9025222055850 * x ^ 34

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.dA_dominates {x : ℝ} (_hx : 0 ≤ x) : L x / (2 + x) ≤ dA x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.dB_residual (x : ℝ) : (3 + x) * dB x - A x = 561460485694698467 / 1179511324603387776000 * x ^ 35

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.dB_dominates {x : ℝ} (_hx : 0 ≤ x) : A x / (3 + x) ≤ dB x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.dD_residual (x : ℝ) : (4 + x) * dD x - B x = 98488038567669650177 / 21018891804432370168320000 * x ^ 36

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.dD_dominates {x : ℝ} (_hx : 0 ≤ x) : B x / (4 + x) ≤ dD x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.H_residual (x : ℝ) : (5 + x) * H x - D x = 19952754273817524913009 / 593237202288299215630663680000 * x ^ 37

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.H_dominates {x : ℝ} (_hx : 0 ≤ x) : D x / (5 + x) ≤ H x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L_residual (x : ℝ) : (1 + x) * dL x - 1 = x ^ 33

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.H_nonneg {x : ℝ} (_hx : 0 ≤ x) (hxu : x ≤ 5 / 8) : 0 ≤ H x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.K_product (x : ℝ) : K x = H x * G x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.G_residual (x : ℝ) : (13 / 8 - x) * G x - 1 = (8 / 13 * x) ^ 24 * (5 / 8 - x)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.K_dominates {x : ℝ} (hx : 0 ≤ x) (hxu : x ≤ 5 / 8) : D x / ((5 + x) * (13 / 8 - x)) ≤ K x

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.final_rational_evaluation : 53 * (T (5 / 8) - T 0) ≤ 1972364 / 10 ^ 10