noncomputable def G12AnalyticCertificate.lowQ (x : ℝ) : ℝ

Equations

• G12AnalyticCertificate.lowQ x = -1809510726609895988793184077301978828901765089329094633616623 / 2551169745882295562347385812285819815260913240800923898604600 * x ^ 0 + 62396921607237792717006347493171683755233278942382573572987 / 77308174117645320071132903402600600462451916387906784806200 * x ^ 1 + -818718432703970092463444682478323569793355887876868316203 / 2342671942958949093064633436442442438256118678421417721400 * x ^ 2 + 14768038237154433688023187692112063106344923269194207907 / 70990058877543911911049498074013407219882384194588415800 * x ^ 3 + -305248275771003713635714811009572844989243376539488733 / 2151213905380118542759075699212527491511587399836012600 * x ^ 4 + 6816813120758544361991759518929188634953931260265107 / 65188300163033895235123506036743257318532951510182200 * x ^ 5 + -160133440758301650143252045438083220379408030227323 / 1975403035243451370761318364749795676319180348793400 * x ^ 6 + 27300008486236884685375100825572986089746878854909 / 419024886263762411979673592522683931340432195198600 * x ^ 7 + -341679676405635200246715533777525643376044649223 / 6348861913087309272419296856404301990006548412100 * x ^ 8 + 17482830256818414890176457447871211047000638249 / 384779509884079349843593748872987999394336267400 * x ^ 9 + -455431116179914938801642690205142143615218841 / 11659985148002404540714962087060242405888977800 * x ^ 10 + 12049353489588789569738474556584762818741409 / 353332883272800137597423093547280072905726600 * x ^ 11 + -323192731805882989970756412727771321621771 / 10707057068872731442346154349917577966840200 * x ^ 12 + 8777853468798632845511018133425010655649 / 324456274814325195222610737876290241419400 * x ^ 13 + -241211264969122012629858765139647915481 / 9832008327706824097654870844736067921800 * x ^ 14 + 6703178541183710764304674849686370169 / 297939646294146184777420328628365694600 * x ^ 15 + -376673334364926551337845297498954927 / 18056948260251283925904262341113072400 * x ^ 16 + 5349784399531486944598735964668019 / 273590125155322483725822156683531400 * x ^ 17 + -9037929053158019603344808021483 / 487682932540681789172588514587400 * x ^ 18 + 262481226420584887595415994027 / 14778270683050963308260258017800 * x ^ 19 + -405791361910265039535761867 / 23569809701835667158309821400 * x ^ 20 + 12057681633864995849483593 / 714236657631383853282115800 * x ^ 21 + -362472925601899106521817 / 21643535079738904644912600 * x ^ 22 + 11024108305494210389473 / 655864699386027413482200 * x ^ 23 + -7373274076612205747 / 432058431743101062900 * x ^ 24 + 458839771749910619 / 26185359499581882600 * x ^ 25 + -2886583470958727 / 158699148482314440 * x ^ 26 + 7057072434691 / 369928085040360 * x ^ 27 + -6567749570881 / 325088317156680 * x ^ 28 + 30381253697 / 1407308732280 * x ^ 29 + -34201733 / 1470542040 * x ^ 30 + 224969 / 8912376 * x ^ 31 + -961 / 34848 * x ^ 32 + 1 / 33 * x ^ 33

noncomputable def G12AnalyticCertificate.lowH (x : ℝ) : ℝ

Equations

• G12AnalyticCertificate.lowH x = -1809510726609895988793184077301978828901765089329094633616623 / 2551169745882295562347385812285819815260913240800923898604600 * x ^ 1 + 62396921607237792717006347493171683755233278942382573572987 / 154616348235290640142265806805201200924903832775813569612400 * x ^ 2 + -818718432703970092463444682478323569793355887876868316203 / 7028015828876847279193900309327327314768356035264253164200 * x ^ 3 + 14768038237154433688023187692112063106344923269194207907 / 283960235510175647644197992296053628879529536778353663200 * x ^ 4 + -305248275771003713635714811009572844989243376539488733 / 10756069526900592713795378496062637457557936999180063000 * x ^ 5 + 6816813120758544361991759518929188634953931260265107 / 391129800978203371410741036220459543911197709061093200 * x ^ 6 + -160133440758301650143252045438083220379408030227323 / 13827821246704159595329228553248569734234262441553800 * x ^ 7 + 27300008486236884685375100825572986089746878854909 / 3352199090110099295837388740181471450723457561588800 * x ^ 8 + -341679676405635200246715533777525643376044649223 / 57139757217785783451773671707638717910058935708900 * x ^ 9 + 17482830256818414890176457447871211047000638249 / 3847795098840793498435937488729879993943362674000 * x ^ 10 + -455431116179914938801642690205142143615218841 / 128259836628026449947864582957662666464778755800 * x ^ 11 + 12049353489588789569738474556584762818741409 / 4239994599273601651169077122567360874868719200 * x ^ 12 + -323192731805882989970756412727771321621771 / 139191741895345508750500006548928513568922600 * x ^ 13 + 8777853468798632845511018133425010655649 / 4542387847400552733116550330268063379871600 * x ^ 14 + -241211264969122012629858765139647915481 / 147480124915602361464823062671041018827000 * x ^ 15 + 6703178541183710764304674849686370169 / 4767034340706338956438725258053851113600 * x ^ 16 + -376673334364926551337845297498954927 / 306968120424271826740372459798922230800 * x ^ 17 + 5349784399531486944598735964668019 / 4924622252795804707064798820303565200 * x ^ 18 + -9037929053158019603344808021483 / 9265975718272953994279181777160600 * x ^ 19 + 262481226420584887595415994027 / 295565413661019266165205160356000 * x ^ 20 + -405791361910265039535761867 / 494966003738549010324506249400 * x ^ 21 + 12057681633864995849483593 / 15713206467890444772206547600 * x ^ 22 + -362472925601899106521817 / 497801306833994806832989800 * x ^ 23 + 11024108305494210389473 / 15740752785264657923572800 * x ^ 24 + -7373274076612205747 / 10801460793577526572500 * x ^ 25 + 458839771749910619 / 680819346989128947600 * x ^ 26 + -2886583470958727 / 4284877009022489880 * x ^ 27 + 7057072434691 / 10357986381130080 * x ^ 28 + -6567749570881 / 9427561197543720 * x ^ 29 + 30381253697 / 42219261968400 * x ^ 30 + -34201733 / 45586803240 * x ^ 31 + 224969 / 285196032 * x ^ 32 + -961 / 1149984 * x ^ 33 + 1 / 1122 * x ^ 34

theorem G12AnalyticCertificate.lowH_deriv (x : ℝ) : HasDerivAt lowH (lowQ x) x

noncomputable def G12AnalyticCertificate.highH (x : ℝ) : ℝ

Equations

• G12AnalyticCertificate.highH x = 1 / 2 * x ^ 2 + -1 / 6 * x ^ 3 + 1 / 12 * x ^ 4 + -1 / 20 * x ^ 5 + 1 / 30 * x ^ 6 + -1 / 42 * x ^ 7 + 1 / 56 * x ^ 8 + -1 / 72 * x ^ 9 + 1 / 90 * x ^ 10 + -1 / 110 * x ^ 11 + 1 / 132 * x ^ 12 + -1 / 156 * x ^ 13 + 1 / 182 * x ^ 14 + -1 / 210 * x ^ 15 + 1 / 240 * x ^ 16 + -1 / 272 * x ^ 17 + 1 / 306 * x ^ 18 + -1 / 342 * x ^ 19 + 1 / 380 * x ^ 20 + -1 / 420 * x ^ 21 + 1 / 462 * x ^ 22 + -1 / 506 * x ^ 23 + 1 / 552 * x ^ 24 + -1 / 600 * x ^ 25 + 1 / 650 * x ^ 26 + -1 / 702 * x ^ 27 + 1 / 756 * x ^ 28 + -1 / 812 * x ^ 29 + 1 / 870 * x ^ 30 + -1 / 930 * x ^ 31 + 1 / 992 * x ^ 32 + -1 / 1056 * x ^ 33 + 1 / 1122 * x ^ 34

theorem G12AnalyticCertificate.highH_deriv (x : ℝ) : HasDerivAt highH (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L x) x

noncomputable def G12AnalyticCertificate.lowF (x : ℝ) : ℝ

Equations

• G12AnalyticCertificate.lowF x = 33 / 4 * (G12AnalyticCertificate.lowH x + 52475811071686983675002338241757386038151187590543744374882067 / 84188601614115753557463731805432053903610136946430488653951800 * Real.log (x + 29 / 33))

noncomputable def G12AnalyticCertificate.highF (x : ℝ) : ℝ

Equations

• G12AnalyticCertificate.highF x = 33 / 4 * (G12AnalyticCertificate.highH x - x + Real.log (1 + x))

theorem G12AnalyticCertificate.low_division (x : ℝ) (hx : x + 29 / 33 ≠ 0) : ((1 + x) * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L x - x) / (x + 29 / 33) = lowQ x + 52475811071686983675002338241757386038151187590543744374882067 / 84188601614115753557463731805432053903610136946430488653951800 / (x + 29 / 33)

theorem G12AnalyticCertificate.lowF_deriv (x : ℝ) (hx : 0 ≤ x) : HasDerivAt lowF (33 / 4 * ((1 + x) * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L x - x) / (x + 29 / 33)) x

theorem G12AnalyticCertificate.highF_deriv (x : ℝ) (hx : 0 ≤ x) : HasDerivAt highF (33 / 4 * (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.S3Correction.L x - x / (1 + x))) x