noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.Q1 (u : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.Q1 u = 2877606340315596112131 / 5348279736800 * u ^ 0 + 2877606725391737161731 / 5348279736800 * u ^ 1 + 2877594402955223574531 / 5348279736800 * u ^ 2 + 2877875989883366094531 / 5348279736800 * u ^ 3 + 2872895800151171617731 / 5348279736800 * u ^ 4 + 2943782926652428283331 / 5348279736800 * u ^ 5 + 2109575153870332571331 / 5348279736800 * u ^ 6 + 10383829637573552983731 / 5348279736800 * u ^ 7 + -59783149991646402097869 / 5348279736800 * u ^ 8 + 454486319565088525777971 / 5348279736800 * u ^ 9 + -2830385515407099703572429 / 5348279736800 * u ^ 10 + 15573268921620622666134771 / 5348279736800 * u ^ 11 + -75309618155383743146134029 / 5348279736800 * u ^ 12 + 321745419062393213085107571 / 5348279736800 * u ^ 13 + -1216945191418565482641618189 / 5348279736800 * u ^ 14 + 4081168435554664274222451711 / 5348279736800 * u ^ 15 + -714214061031714190314493617 / 314604690400 * u ^ 16 + 1884301532778627584156808783 / 314604690400 * u ^ 17 + -231740521439330956241532843 / 16558141600 * u ^ 18 + 478548591158874008366290197 / 16558141600 * u ^ 19 + -870436617773273334321498603 / 16558141600 * u ^ 20 + 1388228819773724533783435797 / 16558141600 * u ^ 21 + -83895631809731253807222861 / 719919200 * u ^ 22 + 100825664926679066928025539 / 719919200 * u ^ 23 + -20735670042279641789346393 / 143983840 * u ^ 24 + 1384044232346431030110339 / 11075680 * u ^ 25 + -994512325879346313408381 / 11075680 * u ^ 26 + 82335240492193284597477 / 1582240 * u ^ 27 + -1276159150445091608727 / 54560 * u ^ 28 + 83568122150236609365 / 10912 * u ^ 29 + -572583238355218869 / 352 * u ^ 30 + 1853020188851841 / 11 * u ^ 31

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.H1 (u : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.H1 u = 2877606340315596112131 / 5348279736800 * u ^ 1 + 2877606725391737161731 / 10696559473600 * u ^ 2 + 959198134318407858177 / 5348279736800 * u ^ 3 + 2877875989883366094531 / 21393118947200 * u ^ 4 + 2872895800151171617731 / 26741398684000 * u ^ 5 + 981260975550809427777 / 10696559473600 * u ^ 6 + 2109575153870332571331 / 37437958157600 * u ^ 7 + 10383829637573552983731 / 42786237894400 * u ^ 8 + -6642572221294044677541 / 5348279736800 * u ^ 9 + 454486319565088525777971 / 53482797368000 * u ^ 10 + -2830385515407099703572429 / 58831077104800 * u ^ 11 + 5191089640540207555378257 / 21393118947200 * u ^ 12 + -75309618155383743146134029 / 69527636578400 * u ^ 13 + 321745419062393213085107571 / 74875916315200 * u ^ 14 + -405648397139521827547206063 / 26741398684000 * u ^ 15 + 4081168435554664274222451711 / 85572475788800 * u ^ 16 + -42012591825394952371440801 / 314604690400 * u ^ 17 + 209366836975403064906312087 / 629209380800 * u ^ 18 + -231740521439330956241532843 / 314604690400 * u ^ 19 + 478548591158874008366290197 / 331162832000 * u ^ 20 + -290145539257757778107166201 / 115906991200 * u ^ 21 + 1388228819773724533783435797 / 364279115200 * u ^ 22 + -83895631809731253807222861 / 16558141600 * u ^ 23 + 33608554975559688976008513 / 5759353600 * u ^ 24 + -20735670042279641789346393 / 3599596000 * u ^ 25 + 1384044232346431030110339 / 287967680 * u ^ 26 + -36833789847383196792903 / 11075680 * u ^ 27 + 11762177213170469228211 / 6328960 * u ^ 28 + -1276159150445091608727 / 1582240 * u ^ 29 + 5571208143349107291 / 21824 * u ^ 30 + -572583238355218869 / 10912 * u ^ 31 + 1853020188851841 / 352 * u ^ 32

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.primitive1 (u : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.primitive1 u = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.H1 u + 14606816124167 / 20629078984800 * Real.log u - -2427980359983876276224 / 4512611027925 * Real.log (1 - u) + 0 / 1 / (1 - u)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.H1_deriv (u : ℝ) : HasDerivAt H1 (Q1 u) u

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.partial_fraction1 (u : ℝ) (hu : u ≠ 0) (hv : 1 - u ≠ 0) : S3Correction.L (1 - 3 * u) / (u * (1 - u) ^ 1) = Q1 u + 14606816124167 / 20629078984800 / u + -2427980359983876276224 / 4512611027925 / (1 - u) + 0 / 1 / (1 - u) ^ 2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.primitive1_deriv (u : ℝ) (hu : u ≠ 0) (hv : 1 - u ≠ 0) : HasDerivAt primitive1 (S3Correction.L (1 - 3 * u) / (u * (1 - u) ^ 1)) u

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.integral_eq_primitive1 {a b : ℝ} (ha : 4 / 53 ≤ a) (hab : a ≤ b) (hb : b ≤ 1 / 3) : ∫ (u : ℝ) in a..b, S3Correction.L (1 - 3 * u) / (u * (1 - u) ^ 1) = primitive1 b - primitive1 a

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.Q2 (u : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.Q2 u = -66034453321886027755869 / 2674139868400 * u ^ 0 + -129191299918380318350007 / 5348279736800 * u ^ 1 + -31578426378856273693869 / 1337069934200 * u ^ 2 + -24687165905108345736189 / 1069655947360 * u ^ 3 + -60281466862695278531607 / 2674139868400 * u ^ 4 + -16802735828391161254269 / 764039962400 * u ^ 5 + -14438696955608474526069 / 668534967100 * u ^ 6 + -105125746007294243224821 / 5348279736800 * u ^ 7 + -16490889599894064532269 / 534827973680 * u ^ 8 + 26325220324195261859571 / 486207248800 * u ^ 9 + -635202022960237955779287 / 1337069934200 * u ^ 10 + 1002496986906128526385971 / 411406133600 * u ^ 11 + -4448368380400290878794029 / 382019981200 * u ^ 12 + 51893652347357828156398233 / 1069655947360 * u ^ 13 + -59842308105111021366226689 / 334267483550 * u ^ 14 + 183746559168993407786048511 / 314604690400 * u ^ 15 + -265233750931360391264222553 / 157302345200 * u ^ 16 + 71254422679784568506755983 / 16558141600 * u ^ 17 + -8024304937977319386738843 / 827907080 * u ^ 18 + 45437498914189660090216191 / 2365448800 * u ^ 19 + -25107914789724805167726603 / 752642800 * u ^ 20 + 36341508452164296525802197 / 719919200 * u ^ 21 + -5944265419695869660177583 / 89989900 * u ^ 22 + 2130861662764484385864195 / 28796768 * u ^ 23 + -387744681863739225385593 / 5537840 * u ^ 24 + 608554868618952579339153 / 11075680 * u ^ 25 + -13784194902156919073901 / 395560 * u ^ 26 + 937877961502262355237 / 54560 * u ^ 27 + -33828118894282925349 / 5456 * u ^ 28 + 513286592311959957 / 352 * u ^ 29 + -1853020188851841 / 11 * u ^ 30

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.H2 (u : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.H2 u = -66034453321886027755869 / 2674139868400 * u ^ 1 + -129191299918380318350007 / 10696559473600 * u ^ 2 + -10526142126285424564623 / 1337069934200 * u ^ 3 + -24687165905108345736189 / 4278623789440 * u ^ 4 + -60281466862695278531607 / 13370699342000 * u ^ 5 + -5600911942797053751423 / 1528079924800 * u ^ 6 + -14438696955608474526069 / 4679744769700 * u ^ 7 + -105125746007294243224821 / 42786237894400 * u ^ 8 + -1832321066654896059141 / 534827973680 * u ^ 9 + 26325220324195261859571 / 4862072488000 * u ^ 10 + -635202022960237955779287 / 14707769276200 * u ^ 11 + 334165662302042842128657 / 1645624534400 * u ^ 12 + -4448368380400290878794029 / 4966259755600 * u ^ 13 + 51893652347357828156398233 / 14975183263040 * u ^ 14 + -19947436035037007122075563 / 1671337417750 * u ^ 15 + 183746559168993407786048511 / 5033675046400 * u ^ 16 + -15601985348903552427307209 / 157302345200 * u ^ 17 + 7917158075531618722972887 / 33116283200 * u ^ 18 + -8024304937977319386738843 / 15730234520 * u ^ 19 + 45437498914189660090216191 / 47308976000 * u ^ 20 + -8369304929908268389242201 / 5268499600 * u ^ 21 + 36341508452164296525802197 / 15838222400 * u ^ 22 + -5944265419695869660177583 / 2069767700 * u ^ 23 + 710287220921494795288065 / 230374144 * u ^ 24 + -387744681863739225385593 / 138446000 * u ^ 25 + 608554868618952579339153 / 287967680 * u ^ 26 + -510525737116922928663 / 395560 * u ^ 27 + 937877961502262355237 / 1527680 * u ^ 28 + -33828118894282925349 / 158224 * u ^ 29 + 171095530770653319 / 3520 * u ^ 30 + -1853020188851841 / 341 * u ^ 31

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.primitive2 (u : ℝ) : ℝ

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.primitive2 u = MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.H2 u + 14606816124167 / 20629078984800 * Real.log u - 113861120333519197084801 / 4512611027925 * Real.log (1 - u) + -2427980359983876276224 / 4512611027925 / (1 - u)

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.H2_deriv (u : ℝ) : HasDerivAt H2 (Q2 u) u

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.partial_fraction2 (u : ℝ) (hu : u ≠ 0) (hv : 1 - u ≠ 0) : S3Correction.L (1 - 3 * u) / (u * (1 - u) ^ 2) = Q2 u + 14606816124167 / 20629078984800 / u + 113861120333519197084801 / 4512611027925 / (1 - u) + -2427980359983876276224 / 4512611027925 / (1 - u) ^ 2

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.primitive2_deriv (u : ℝ) (hu : u ≠ 0) (hv : 1 - u ≠ 0) : HasDerivAt primitive2 (S3Correction.L (1 - 3 * u) / (u * (1 - u) ^ 2)) u

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.integral_eq_primitive2 {a b : ℝ} (ha : 4 / 53 ≤ a) (hab : a ≤ b) (hb : b ≤ 1 / 3) : ∫ (u : ℝ) in a..b, S3Correction.L (1 - 3 * u) / (u * (1 - u) ^ 2) = primitive2 b - primitive2 a

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.endpointExpression : ℝ

An exact elementary expression; its scalar upper bound is not asserted.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.endpointExpression = 36 / 5 * (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.primitive2 (1 / 10) - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.primitive2 (4 / 53)) + 8 * (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.primitive1 (1 / 3) - MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.primitive1 (1 / 10))

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.envelope_eq_endpoints : envelope = endpointExpression

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.G9Analytic.actual_le_endpoints : goldbachB9PaperSplitIntegral ≤ endpointExpression