noncomputable def G67CenteredEvaluation.W4 (s : ℝ) : ℝ

Equations

• G67CenteredEvaluation.W4 s = 2449478844784766596667305979547050351513803646558130920094824194917654921274849835585873910841237635979804399865268010409373556042449231094181549651058889747746644063142493161433684251005329585677005263311327263535281020 / 849520488924865017179601590000788679160794411633732449667845940521202711805376596961492089682627468900265416871139383481778735101023606354933899223941458021329623207533855188543342672134611489944822862128039065389 * s ^ 0 + -7978711161525033880225679962039262709660591826487393403887643474627332949468593830517874389874068480 / 26016531848676609019733212304201985278528371719929018837564202498970513101376639717306762443 * s ^ 1 + 137499054162663730913898359646288443458607673276952922426324939280693499495594056908549955304168990720 / 8672177282892203006577737434733995092842790573309672945854734166323504367125546572435587481 * s ^ 2 + -657285725940155438415933028277676898763918001724292410619185949820903978994629487018742966970201221120 / 1238882468984600429511105347819142156120398653329953277979247738046214909589363796062226783 * s ^ 3 + 12439406227878599024766265708952706023465539883506140436484685288277548858016171246723149008193569812480 / 963575253654689222953081937192666121426976730367741438428303796258167151902838508048398609 * s ^ 4 + -92928024595628876266412899312091176848074061215970363671731680883530208572088300343394789303337041920 / 381916469938442022573556059133042457957580947430733824188784699269983017004692234660483 * s ^ 5 + 5846569220122950598433488552841486954080160140235789920015219444952902844405897762245184371446003957760 / 1582225375459259807804732244979747325824263925070182985924965182689929641876582115022001 * s ^ 6 + -6349667608763516792692130235143233916492937943053948951148407803513249506458447900093785862216138506240 / 136735526274257020427569453269854707169998116981373838289811805911475401149828084014247 * s ^ 7 + 22434954707351113270522580077286103632988144356357635520559642568305264479059339640252565213290892328960 / 45578508758085673475856484423284902389999372327124612763270601970491800383276028004749 * s ^ 8 + -87180438502779629172535476574792217493507585858508099164707344948304355736274206414344264230080218398720 / 19533646610608145775367064752836386738571159568767691184258829415925057307118297716321 * s ^ 9 + 531545383178867478302564663470766550307421151840586038050129323513273321725035224960181292091313244078080 / 15192836252695224491952161474428300796666457442374870921090200656830600127758676001583 * s ^ 10 + -1210621812802760890314467921532166754778711564831764729526575830456649215219361526076757868917690773012480 / 5064278750898408163984053824809433598888819147458290307030066885610200042586225333861 * s ^ 11 + 7254673231335996786190024449653853979790986144675759858551247177066414694092274717687263306717082487357440 / 5064278750898408163984053824809433598888819147458290307030066885610200042586225333861 * s ^ 12 + -7904697321059464046914833136760898015444780913341901569230507150592967253871713282713714426748888909086720 / 1045009900979036605266550789246391060088169030427901174466521738300517469105094116511 * s ^ 13 + 6624105148614957482216176866862573273493120505021118999345233969961778636677642674147248464367033652346880 / 187565879662904006073483474992941985144030338794751492852965440207785186762452790143 * s ^ 14 + -3915615006142110791345201635497175651134331015776508830212957181630159310166392703338927700964843318149120 / 26795125666129143724783353570420283592004334113535927550423634315397883823207541449 * s ^ 15 + 3727894328485507439255075791820057670995028843439020345398954102162319324366838623528316410592866923970560 / 6946884431959407632351239814553406857186308844250055290850571859547599509720473709 * s ^ 16 + -4051642796733218554867945702917595943770631572277554971786312430166027366329075704648576233891133191618560 / 2315628143986469210783746604851135619062102948083351763616857286515866503240157903 * s ^ 17 + 35173425957281493305206159882191331286940960721718522663166178292686090701077760948220524837504403992739840 / 6946884431959407632351239814553406857186308844250055290850571859547599509720473709 * s ^ 18 + -345643028436877124167893654465649666424384703828302929349622678948617329710565021860198910819925774827520 / 26616415448120335756135018446564777230598884460728181190998359615124902336093769 * s ^ 19 + 1082544729080822191835734105177382851299175056080658552639479264018680667094697649721294639280619037655040 / 36756002285499511282281692140494216175588935683862726406616782325648674654605681 * s ^ 20 + -2163677352275329147645574316281071048243124179322251281852490315800626473568749582422561499921753487441920 / 36756002285499511282281692140494216175588935683862726406616782325648674654605681 * s ^ 21 + 2950352200348626320791681036978336146868229770401215312040566116501366727294430261243608729657907693486080 / 28588001777610730997330204998162168136569172198559898316257497364393413620248863 * s ^ 22 + -1503018498215195931903288686430693174251059953069352150303100550625281666038835196094448888136343832494080 / 9529333925870243665776734999387389378856390732853299438752499121464471206749621 * s ^ 23 + 1986238141381071224035399462656656166810325980771411979016734713396000576931265247251883570308875697520640 / 9529333925870243665776734999387389378856390732853299438752499121464471206749621 * s ^ 24 + -83168988025045208741061973890641578614288376009475488919468468204966147621911633538331751795923510886400 / 352938293550749765399138333310644051068755212327899979213055523017202637287023 * s ^ 25 + 26437971933402858721012762152983691513203940226317069489051588906704205055808330981860340411480135434240 / 117646097850249921799712777770214683689585070775966659737685174339067545762341 * s ^ 26 + -3832259643821101016953131217607194908616609374787675132118056891689736767667191895037680917492908687360 / 21608466952086720330559489794529227616454400754769386482431970796971590037981 * s ^ 27 + 13266361075532164706166284925802813159543463157347425392175720654284143493400827508726955398401055784960 / 117646097850249921799712777770214683689585070775966659737685174339067545762341 * s ^ 28 + -63149175429585152896634328893744646131653374858195497449932247024569606655295030687715224120451965911040 / 1137245612552415910730556851778741942332655684167677710797623351944319609035963 * s ^ 29 + 22604564215705536240183205280201333309824823511133151769020986859225010819497593250091166735548138127360 / 1137245612552415910730556851778741942332655684167677710797623351944319609035963 * s ^ 30 + -581574360017708013991558651159791875524698121204266863972736228974470164163177335158607112934575308800 / 126360623616935101192284094642082438036961742685297523421958150216035512115107 * s ^ 31 + 21800858504441329185473634054085109367040604704201098324777702716098126070222304221023497626803240960 / 42120207872311700397428031547360812678987247561765841140652716738678504038369 * s ^ 32

theorem G67CenteredEvaluation.weight4_eq (s : ℝ) : G67Centered.rectangleMiddle s = W4 s

noncomputable def G67CenteredEvaluation.D4 (s : ℝ) : ℝ

Equations

• G67CenteredEvaluation.D4 s = ⋯ + 4368583430482356035938610380430908822351953307463326967692976658935981453261878454719023706670673612858528502678974958351693467173605998792791393520098098280717915052662284656561156550918602257222890086834046716463185418050297963476265188745605948380435027366031159613621045627191445882650656278946742886880584176997424735065026494951144213514290916921255743886003725170330509918492686872317874238007304104160460854525952 / 17906414991965716917983565853133414962827771217544432802533178832211939508764116096248495120963167859354774933244798974462750485804933307688838181845667459804206795111298650342249394704574291459788204904844474260187867927480152229027587224728884104568315844812146264991948647149540812030073558873555002849415059848197196549969322558114757375328415871617669 * s ^ 46 + -3597369592800123853676132618105154568602943581196310052850949821550975852160731011272770396931421087307434967107920175425211282561162682141931064155835608463988363528058464762470311878972909001609414260545917082759223124735770254722009334000505160869800980912039287164473905248290176814777931242292309032149103990674622657760362601260263384411507294350979473237321922155583083812188678967013850309305159136663333502976 / 3745641758767877864281380130764635184459643395712762582632552155003961743037299940645210877497211199296066379375977696201888985860547485187808681304787570556877127371312941961730618479808871576745221291227978550848819798242930224036227089639142388940366448732825642177121835574936370336374839742617036114591277213780110561429385967894146629152912996615 * s ^ 47 + 183895646510051112615475426671716070941485089215041910988833508199410976826601502837392901355100383019674050238786049584117092450075652460668088578143647803382486806582025754843986329334380517434900298451125713971309957905793054120606241698998800053869026775417031451982275636018992299407091998155693419133252247930713788947903889996454308084307467748494952673705684611368015336150803387610958869739549143905723219968 / 50672958970642616815877326663312549665275794806564955597902661364453512496920006996160125558725807687630138797689232414046012917272307520763767443634975982276497118650812515365525060275183762219518697013643049057588197168538306717471230687441977904793630751972413973119415299645928038566909221703221144304546480589580042091509526097737052816629083645 * s ^ 48 + -20244592721866938451158033197271789831117019604250572255156376397332238387528847323580579593144874026835574262677680089065514225822373543565866106436476784931349620040500365526923745317878492645450743513822871859141481716780326104924298119945040669206090071423138719926726174327437635365891430800354053496635386631791667833945668847651774928432539887653365675738666106621846394427610049894820640526527042091348918272 / 1538063561865280411966744123496771400832817397738230809780474545106464284155898489629142449280438789534302818305579654897212861311792763140491710758403700856628706636653045995508143749123707302807376365467426427506778749168102828996255566394875457323514633160770563581147141990893632015566563743247893633526021149970846232474038117814824408708183835 * s ^ 49 + 1609639595467798036068595170550235897802578500810236905060371592712913612792742330841188052379738653865154372505503299142733791115137585890789141889252962255935709292807769187666591172040941277571698011417436145388848049530400323686184921274140625152659028153514159467185644169419510739323214596991183811064172102537881194164448079200052726476521455454859739538070367587141659249172431094827418831714534742831398912 / 35129555037637983590104384151366178966390069660356810948312725459234040253809002245750026150397310982412080259213835216123034568193876417310138378791742919267587142644508498407832478877701358455381982528054426844742712245150312876776442926595963772036580499203299863323122408928057136403208506548859536813404653872223896074382201300636505859273315 * s ^ 50 + -20293116657188756253277934845390147332785065291241036480247520251149571169406251219373919552604511568391060193730298963639335470078035204940468439614805609398264685352523914978508702235501040897410897145620406765953634982246977789382546633583396560220537544600495486032475248280420838186154775254259869385668815975277123172158240529266548716349696484279038540889147771174901703329750885658633878255173202905923584 / 132564358632596164490959940193834637609019130793799286597406511166920906618147178285849155284518154650611623619674849872162394596958024216264673127516011016104102425073616975123896146708307013039177292558695950357519668849623822176514878968286655743534266034729433446502348712936064665672484930373054855899640203291410928582574344530703795695371 * s ^ 51 + 876805149246863161341048214574456940630335579729704306020037607436652936625290862960063302127290475181731247066723085684871798029805925710978142644912392365813812393481175732583761315141251737448523804796226026324714816587559597077246947172308578707798143914925155346617861850240985594276607800565955112324672886507005799646937796075881530481462942829573624424636961080369424514797710133876223796462781487644672 / 1786581652730406529527761997221491072897831951398912218293888290659311409948075179054570825936902353781827811585914418762296423139596013696289395249541927440756097372959797508408303863993355970878400169254662403740157262124310271920685700381221775519329730926272687958252678071914618135747775341954917195412940745167263188444398174268245225005 * s ^ 52 + -18747953002762928487849192160028215794876273362166708163586868824584611600364064602682996893038573088255359695944750562873990828445237981028143696024724256047330139006691105611797148378821097957865425271184777549842340904095474222609147931273678205802829167006229306213662471093119228040149900948781678106450419979012746125850953529228502586815896763080674285609544616392610049071335251393561162584617822191616 / 12419137605871743502179080417627048173073310486387671825280256240928679115825746031163848839680552608215287667429395165179816248239495626488605528050440409220747449464467311379203701139973676063702881017659023660557200431847241214940218374050201021484913720440823054327476411622047991013142430381017299272979727126286834477766422264029510005 * s ^ 53 + 1425180923155649367817912193152802722920200915045710158152829028022916518394959599762495032584107642762674580283703352412526087411515321193936817982269030639259770939416417317308602694498022456976582178650261599608363420272477254839341506553521190725752980919143908820071776528672229921901242054876691555839377943912198344768976142096921348009837564868721049687951812636186167592529579714890909750646538240 / 319952832916240959655865501372773937841467263156178366877504076065118954298929721004363592911044142070238395760186181788915868875789553696341676937414311656613538450870689179187479673298801815890758227968354293318038506301869955842228285082548111388163120683361430290675939254935846113193589349404848420920297514423080637940002336309481 * s ^ 54 + -46037249910534303627430820618592478752627645936837081756395342960507342672311352051606795705642931665324010200450605994234930269167965902373724371638845357214046772120989149237972500815562044407958484932699961948937707170337838007366593484749135151492123707903793453657450100762707148764864851853674951635008115528012826880883991404504682655987144402772083010900151990568786523850958785864054568400636084224 / 3652291771968410954562238270387325139511088569990337961526225773950886176431178890710188183229843508537626970470049810986681144714201509175221029191238840608513033259938999120913683063127832049319032602280270706743647100238326854425436084432860516789409207800635194827527231117663903744945689743206288578429811249546486527428328555985585 * s ^ 55 + 785582781320160885751283126355756180523821982856251737040197505924038379813636041775649548486184050601234783223689297582058480907321993663936580538682543699927898779163263127084957179189038907297495318312850029948968792138636080241619265094923559087483861487298701226281911437828837919902750381705733638970292449153914415587464442357023510414617746221925573541089305119167241604396996855285812417450213376 / 22970388502945980846303385348347956852270997295536716739158652666357774694535716293774768447986437160614006103585218937023151853548437164624031630133577613890019077106534585666123792849860578926534796240756419539268220756215892166197711222848179350876787470444246508349227868664552853741796790837775399864338435531738908977536657584815 * s ^ 56 + -16519715666461119684255953796824733974582456672589726036424839777693577007291980361777567431348895198230892021377926250794881425201846889439671889847518273385529370656287291938759254814610493012063982725127495363234591237837880696597648584240375557417135767659822956922776439841170399943330903546899331034341361414467986032111866395864949812659870787187303710174840287027170091806450316308149198280196096 / 185744381425439198218086673975859489371463589990862938591579401614752895104062395906534515751911890786636167953519290595874543290149087584560902669543754290215787685497584250669464632209115193476022611111237893848530086977486998648499012583678000141860815124886090364009928857125764315971402621329720214536429397830772848874959495295 * s ^ 57 + 604051717426503051687375307165145601010981412065697397724609789960195685757021323880557018666643807364248918183091314624404164829015470087667965811455415829921938830753214540888176064587271066385162935400623959969913548226206279356681227038284752956761241373337131055293115086544905091715656398385191344402000354364804795322474787286872747159940406250158376659085708210394775900433751513702842796867584 / 2725808532448793265254940708241124581971163794415179392329257466044591752051230128607424759462019361648748795963595459478242773649986610255610730999593878472768372743151131561187112003068776424176432448173302425450127062562702286246316746510997905645756196801263380603919291404361321198741757545719164573909865376971509312630432845 * s ^ 58 + -460990824148918423080171425043488308959925329583741023852367462302621388158549327046086608322213332306924740788413223588453410903502154908491450154616959489636611720083005501894432041817390162802309241361240197125741441103109851967534476184607296053076203862070167019089487869440383120337126718556502698821905184124300397607336730344522538249358276929576274850005271325194883483567416217591970004992 / 871700841844833151664515736565757781250771920183939684147507984024493684698186801601351058350501874527901757583497108883352342069071509515705382475085986080194554762760195574412251999702199048345517252373937456172090522085929736567418211228333196560843043428609971411550780749715804668609452365116458130447670411567479792974235 * s ^ 59 + 55828278954375224282239579668792066110242768587409113920962269318059583288790444173710717923352700307089924828241308745799724182804999633670357942124053996296246958316968018152984840714480577188084293829045684067345360859165698406995182391938897905956759732708463778445204327205684897215617321252453772329824118003624010411199550322705347961657738327470598874159987547340872252986269679350928375808 / 46208759810283158983114490976980870704218816972913244712221896727264265406283038000431008483988868461047802064174599662280133137533889543060752530125851912606899129382615937906848937989604441915889953180648975664109021386405978847688835995032936744914411107176988601331083615663281649099692443433846387867396724422714562251105 * s ^ 60 + -48355401693518404462206623280573228423985886823881149503881208099173050157507470929872985393762039752140391284337833549575036203152222067255511396294108935395713234176723554192253450537147134873527500532615332901688320232138022327367317947509975599271307597797741282457317723545577446277871856560107953945052378437157767566322309325238537145476154546097855620350544182782879689668792783106845179904 / 18309131245583893181988760575784873297898021819456191301069053420236784406263090528472663738938985616641581949955973451092128224305880762344826474200809248391412862585564805585732598071352703400635641826294877149929989605934444449084255771616823993267974212277674728829297281677904049643274364379448568777647758733528411457985 * s ^ 61 + 20508586200428800865357427332876516654934097639054479679136457013448464612975523446263185890009675908813077994536617405223881705352171117121610953202494525943134451570237318975575725005856478642760458033089426805655397984327998611237365096515024743308250729631059175485184786925331745844838652185311923895971952786269067003766265927703644998989448199355183682088459644058362940555740359923073024 / 3714573188391944244672095876604762284012583043103305193968158535247876730830409926653005424820244596600036914172443386303941615805615898223742437451979965183893865405876406083532683723139116129161217655973803438817202192317801673581711457012948669764247152014135672312699793401887614048138438705507926309119042145167054465 * s ^ 62 + -14951820067043151622072185726239143498106759944599204400142029166991433934798551289793253782719203854052954514463154429243301529423017723296956069201507514782310933388765562116176195030775518135777314421739111453786424882774618565489087662426331008309197082060403797797315393448475973649425623200624724718459379534618738550968092832183615488 / 1355439753611597402847761302116312568734634944781831582587373392299139831775209997156007831765166146181357558466133343628991226488967066109538108997371473109570929990480655932675065885172111257113155841020893724071224166369388990230165666428892750522294319328877543915 * s ^ 63 + 181402994507465033568830471332285412076416663807246688719090153183677692225845187417333405544763383668255435027281840981823033074645753006642218970228713863165626544560465533694548627142938751681159884506836727027569822531584 / 8617817636781731632835694698402962953339339746404203760726209303650954952046318628067650771810192050391783650074722745748494171303700456189327854779703 * s ^ 64 + -221900378448804752940437751673382519826078809272784432264407491293079509532938396890564465411644212482464584244033491329447527150924981901833841793417819467402708202489506730532948588308009460686193864351113566084888274736775168 / 5788300846038396413387974939093990116992923196334823525954437248952224742791110678518772101732512327179814684966855444227738585058985473073831875793700515 * s ^ 65 + 385383962326864351083986173595092854662378060718369931516510995374788584374159037365865523223522636893073730685746234163978906486317737295205849802115842437870733686994463964555028219216656097827571840911483948430262063425650688 / 5788300846038396413387974939093990116992923196334823525954437248952224742791110678518772101732512327179814684966855444227738585058985473073831875793700515 * s ^ 66 + -10122323119130970386195893492330815749972911810375218626467065619759033408350259667688756404185476429249662288830789352616685917343506186051200983690525198844129454822426959882698141336896446832313073534350295601749105261412352 / 91877791206958673228380554588793493920522590418013071840546622999241662583985883786012255583055751225076423570902467368694263254904531318632251996725405 * s ^ 67 + 37201000347432955621057758870089718822167500542247940904805991658173102595111912084224725321634196435996674395949027506434515891664662419408957100400907567667590187963873900069363435269423102705685287101609357438856327061307392 / 214381512816236904199554627373851485814552710975363834294608786998230546029300395500695263027130086191844988332105757193619947594777239743475254659025945 * s ^ 68 + -11142727659209036449143575275624008541616657960002560120343317666943217696844892762348950002288829909794400241609264342171234865404782212058034458505056555446254456568354507220454323210681034123198766485302551430634562570420224 / 42876302563247380839910925474770297162910542195072766858921757399646109205860079100139052605426017238368997666421151438723989518955447948695050931805189 * s ^ 69 + 75256433526269922873137885598421904588495816620712679977350878945288381370699767142639013943598706793823701370908383028970626760763384855946444332136028875894836739311852066618418987142807836782106574200815323204507941208064 / 203591180262333242354752732548766843128730019919623774258887736940389882269041211301704903159667698187886978473034907116448193347366799376519710027565 * s ^ 70 + -770004029409496632113686502312879006833491572908077350776675453096979874582517360601215478106398829072360774713131029771977044756125302472306527466358682062972745979991724266562629200183906986181581479321247622193217536 / 1544006706120425927352344038319468850277417695565898226582089481494550104801653366866917716346003672012429780849505207201997537880363110417337535 * s ^ 71 + 129748034352375754932657865755059375417473766716152736423890422562919345537011440088473724556455967764817078387894012126113757759289937555299427390117130015190055442220734019924711436571243937346672470825667824080895573229568 / 203591180262333242354752732548766843128730019919623774258887736940389882269041211301704903159667698187886978473034907116448193347366799376519710027565 * s ^ 72 + -2489005460462146685802772589516371475412006379586420251892711756158247430926563481131361475344057972083853136261464529004717652819832138256873570991794954017148549098186852816933328164319927418476735045802700948843249270784 / 3231606035910051465948456072202648303630635236819424988236313284768093369349860496852458780312185685522015531318014398673780846783599990103487460755 * s ^ 73 + 946667027938802016088199628920276808969196872674985948954095564038189204352667884634598392681912115467530752395761188324713164296068763235884888290528126212639454087998888784874541319788339630817293432607065645573992349696 / 1077202011970017155316152024067549434543545078939808329412104428256031123116620165617486260104061895174005177106004799557926948927866663367829153585 * s ^ 74 + -1425036081808992570282506435617557661655355421743982860210814857522003786030911035898629219117725443373100158296707650433998756711430321453058081743220424996025707874270896276481439961882809382016851356499957838613646934016 / 1508082816758024017442612833694569208360963110515731661176946199558443572363268231864480764145686653243607247948406719381097728499013328714960815019 * s ^ 75 + 800484689106486977673632992588317315998656543574608627809918892779320535944944807708787754048547715463706500053947607074176928883571686659267840893201237958120424048119594123017290294061094640902349414167255639914564288512 / 837823787087791120801451574274760671311646172508739811764970110865801984646260128813600424525381474024226248860225955211720960277229627063867119455 * s ^ 76 + -253115427710608776423010361167874079532047458140074864766158375537382359860446788480390256714042300524193204361900756151954435386456583874214599617558118066313531106445318701205514783083170478775546277136597538982741409792 / 279274595695930373600483858091586890437215390836246603921656703621933994882086709604533474841793824674742082953408651737240320092409875687955706485 * s ^ 77 + 4585272507903908299252699095694617708408416565821230411748200913313569520852945829387596145430206938346324734367862362853569733638767498173579377222835124493874609706975493768856728447924094419190849997323449954371371008 / 5699481544814905583683344042685446743616640629311155182074626604529265201675238971521091323301914789280450672518543913004904491681834197713381765 * s ^ 78 + -459445101095648382744376923667896784937700345209283385692608786551502779153992710698255294416742244070194122047139833990775591935377013249169550395954232382959812599611989272656255932179484850155233119018037126501498880 / 689566902952914502717244094053300964042507137867275565238658527461565419461942492850699937880972406604301439391132473425284740968913273303594337 * s ^ 79 + 104071393016387393845388593142998784438584218886022402398677259433329915204033596089674390201490007395208106364519582585411486123348160848364746784691047070442025293363339768044184408681185646459948038435546746759151616 / 202813794986151324328601204133323812953678569960963401540781919841636888077041909661970569964991884295382776291509551007436688520268609795174805 * s ^ 80 + -222764958359654394226995929820846199522590015867718761876202968404080809107211770047773412389193858523648795809566079626398678069317268896227458210345888813151243649810436513421048938577320352196287019823089103392473088 / 608441384958453972985803612399971438861035709882890204622345759524910664231125728985911709894975652886148328874528653022310065560805829385524415 * s ^ 81 + 9422220378404974292592721154967696422209190373003069970451503098288015996100161710949768503504925469734078351210323243820588107958472221315485036234811108473686247372964289968559166053970290009786044840903983497216 / 39100403891681381208521535402607251388794788887789358307457474424838420681905130067856288792171174917174238729807123772399592928526818931015 * s ^ 82 + -24666776901157328276524453000565078467021316532569065094450169090507718584243978933888265024903517348930505916215291572853120521329254825245846582452816043138187671623789796066684043822034305558990285675284161101824 / 169435083530619318570259986744631422684777418513753885998982389174299822954922230294043918099408424641088367829164203013731569356949548701065 * s ^ 83 + 1046129271305245064608391383563483906949207246446723154234045347555565493745283661863447471482701548556447433823134562729421149822828211226257031336521414119522021229598311275900361316057872201146985967474360451072 / 13033467963893793736173845134202417129598262962596452769152491474946140227301710022618762930723724972391412909935707924133197642842272977005 * s ^ 84 + -5285856933559441947148587311151664815887340014758027602585148091644399923257142027690620793637077329938074546876836380599791779777057109484727697928398281252048299069613601814405581629430287801814322273857797357568 / 131782842746037247776868878579157773199271325510697466888097413802233195631606179117589714077317663609735397200461046788457887277627426767495 * s ^ 85 + 983333567619624958455300787072265627886665104901369840497307557727693423514632880212892106924096903280259075307194512122415161712442339393841298762467585690459931919517432042633740563996314379152651111351975936 / 54568464905191406946943635022425578964501584062400607407079674452270474381617465473122034814624291349786913954642255398947365332350901353 * s ^ 86 + -474612832045814768597346748442178461999575865312215980954582247565050725486683012249585384286804061969576870820844785186903163143563215054766301697345523177436459458599880384306534555088253996057198982523256832 / 65858492126955146315276800889134319439915704902897284801647882959636779426090044536526593741787937835949723738361342722867509883871777495 * s ^ 87 + 107552996851187846491432181763291907531758055056485545991644933141413778260666092459347931150889061502415897067902694894491409765578350391233706636242012638605150518607389605675288518199674412366554906805403648 / 42442139370704427625400605017442116972390120937422694649950857907321480074591362034650471522485559938723155298055087532514617480717367719 * s ^ 88 + -839463534312652588491945479369164772562781494582574506239041525456280024559294605336465644197100553622624456959421260164405540047636503322089736605907371058387287428719229181882062710987219695092212640514048 / 1088259983864216092958989872242105563394618485574940888460278407880037950630547744478217218525270767659568084565515064936272243095317121 * s ^ 89 + 17571644825715738721351876622235531904032484708210880066863294754186955282755664720796459295868392371070228429616046123697591016895102480364114863907348466033040688630947878285403294635251977133777267720192 / 88237295988990494023701881533143694329293390722292504469752303341624698699774141444179774475021954134559574424230951211049100791512199 * s ^ 90 + -2197008496959570405275750163448542031967281795173417052650185606916805117629129970928331198858731390316999041152670952826275275724567698051345551910879157826535839140947066036778024332434344445916091514880 / 51821903993534099664713803440100264923553261217854328021918019422858950030026083070391296120250988936169908788834050711251059195015101 * s ^ 91 + 4256594274913768364216773952455309242577653348677142953465491474550755612025461869143403101953961621158321703879976998409173772874436298026193740863212661415244983535176128607401525240169584508341846016 / 595654068891196547870273602759773160040842082963842850826643901412171839425587161728635587589091826852527687227977594382196082701323 * s ^ 92 + -532631857534377633654948980660321663739079362138090604829593831455135336188771024516622778735310650552478350761955645375777031030110502488046317987559495894786347271142027933065310260376504590946795520 / 595654068891196547870273602759773160040842082963842850826643901412171839425587161728635587589091826852527687227977594382196082701323 * s ^ 93 + 157652751149058049784708409888690766366196815539685062910713833858074038751666941400883076721140600698210624840889314122140369936606595174014446760030857116910025596315320898708383781170263967662080 / 2134960820398553935018901802006355412332767322451049644539942298968357847403538214081131138312157085492930778594901771979197429037 * s ^ 94 + -2148246160075879605664016155751213659696299485709428699681070163986033383506897826897853122645176957409381740728832108665803747408536459054233525391089653696973026695665191444764542194888181022720 / 711653606799517978339633934002118470777589107483683214846647432989452615801179404693710379437385695164310259531633923993065809679 * s ^ 95

theorem G67CenteredEvaluation.density4_eq (s : ℝ) : G67Centered.densityPolynomial G67Centered.rectangleMiddle s = D4 s

noncomputable def G67CenteredEvaluation.H4 (s : ℝ) : ℝ

Equations

• G67CenteredEvaluation.H4 s = ⋯ + 4368583430482356035938610380430908822351953307463326967692976658935981453261878454719023706670673612858528502678974958351693467173605998792791393520098098280717915052662284656561156550918602257222890086834046716463185418050297963476265188745605948380435027366031159613621045627191445882650656278946742886880584176997424735065026494951144213514290916921255743886003725170330509918492686872317874238007304104160460854525952 / 841601504622388695145227595097270503252905247224588341719059405113961156911913456523679270685268889389674421862505551799749272832831865461375394546746370610797719370231036566085721551114991698610045630527690290228829792591567154764296599562257552914710844706170874454621586416028418165413457267057085133922507812865268237848558160231393596640435545966030443 * s ^ 47 + -224835599550007740854758288631572160537683973824769378303184363846935990760045688204548149808213817956714685444245010964075705160072667633870691509739725528999272720503654047654394492435806812600588391284119817672451445295985640920125583375031572554362561307002455447779619078018136050923620702643269314509318999417163916110022662578766461525719205896936217077332620134723942738261792435438365644331572446041458343936 / 11236925276303633592844140392293905553378930187138287747897656465011885229111899821935632632491633597888199138127933088605666957581642455563426043914362711670631382113938825885191855439426614730235663873683935652546459394728790672108681268917427166821099346198476926531365506724809111009124519227851108343773831641340331684288157903682439887458738989845 * s ^ 48 + 183895646510051112615475426671716070941485089215041910988833508199410976826601502837392901355100383019674050238786049584117092450075652460668088578143647803382486806582025754843986329334380517434900298451125713971309957905793054120606241698998800053869026775417031451982275636018992299407091998155693419133252247930713788947903889996454308084307467748494952673705684611368015336150803387610958869739549143905723219968 / 2482974989561488223977989006502314933598513945521682824297230406858222112349080342811846152377564576693876801086772388288254632946343068517424604738113823131548358813889813252910727953484004348756416153668509403821821661258377029156090303684656917334887906846648284682851349682650473889778551863457836070922777548889422062483966778789115588014825098605 * s ^ 49 + -10122296360933469225579016598635894915558509802125286127578188198666119193764423661790289796572437013417787131338840044532757112911186771782933053218238392465674810020250182763461872658939246322725371756911435929570740858390163052462149059972520334603045035711569359963363087163718817682945715400177026748317693315895833916972834423825887464216269943826682837869333053310923197213805024947410320263263521045674459136 / 38451589046632010299168603087419285020820434943455770244511863627661607103897462240728561232010969738357570457639491372430321532794819078512292768960092521415717665916326149887703593728092682570184409136685660687669468729202570724906389159871886433087865829019264089528678549772340800389164093581197340838150528749271155811850952945370610217704595875 * s ^ 50 + 1609639595467798036068595170550235897802578500810236905060371592712913612792742330841188052379738653865154372505503299142733791115137585890789141889252962255935709292807769187666591172040941277571698011417436145388848049530400323686184921274140625152659028153514159467185644169419510739323214596991183811064172102537881194164448079200052726476521455454859739538070367587141659249172431094827418831714534742831398912 / 1791607306919537163095323591719675127285893552678197358363948998420936052944259114533251333670262860103016093219905596022274762977887697282817057318378888882646944274869933418799456422762769281224481108930775769081878324502665956715598589256394152373865605459368293029479242855330913956563633833991836377483637347483418699793492266332461798822939065 * s ^ 51 + -5073279164297189063319483711347536833196266322810259120061880062787392792351562804843479888151127892097765048432574740909833867519508801235117109903701402349566171338130978744627175558875260224352724286405101691488408745561744447345636658395849140055134386150123871508118812070105209546538693813564967346417203993819280793039560132316637179087424121069759635222286942793725425832437721414658469563793300726480896 / 1723336662223750138382479222519850288917248700319390725766284645169971786035913317716039018698736010457951107055773048338111129760454314811440750657708143209353331525957020676610649907207991169509304803263047354647755695045109688294693426587726524665945458451482634804530533268168840653742304094849713126695322642788342071573466478899149344039823 * s ^ 52 + 876805149246863161341048214574456940630335579729704306020037607436652936625290862960063302127290475181731247066723085684871798029805925710978142644912392365813812393481175732583761315141251737448523804796226026324714816587559597077246947172308578707798143914925155346617861850240985594276607800565955112324672886507005799646937796075881530481462942829573624424636961080369424514797710133876223796462781487644672 / 94688827594711546064971385852739026863585093424142347569576079404943504727247984489892253774655824750436874014053464194401710426398588725903337948225722154360073160766869267945640104791647866456555208970497107398228334892588444411796342120204754102524475739092452461787391937811474761194632093123610611356885859493864948987553103236216996925265 * s ^ 53 + -9373976501381464243924596080014107897438136681083354081793434412292305800182032301341498446519286544127679847972375281436995414222618990514071848012362128023665069503345552805898574189410548978932712635592388774921170452047737111304573965636839102901414583503114653106831235546559614020074950474390839053225209989506373062925476764614251293407948381540337142804772308196305024535667625696780581292308911095808 / 335316715358537074558835171275930300672979383132467139282566918505074336127295142841423918671374920421812767020593669459855038702466381915192349257361891048960181135540617407238499930779289253719977787476793638835044411659875512803385896099355427580092670451902222466841863113795295757354845620287467080370452632409744530899693401128796770135 * s ^ 54 + 285036184631129873563582438630560544584040183009142031630565805604583303678991919952499006516821528552534916056740670482505217482303064238787363596453806127851954187883283463461720538899604491395316435730052319921672684054495450967868301310704238145150596183828781764014355305734445984380248410975338311167875588782439668953795228419384269601967512973744209937590362527237233518505915942978181950129307648 / 3519481162078650556214520515100513316256139894717962035652544836716308497288226931047999522021485562772622353362047999678074557633685090659758446311557428222748922959577580971062276406286819974798340507651897226498423569320569514264511135908029225269794327516975733197435331804294307245129482843453332630123272658653887017340025699404291 * s ^ 55 + -5754656238816787953428852577324059844078455742104635219549417870063417834038919006450849463205366458165501275056325749279366283645995737796715546454855669651755846515123643654746562601945255550994810616587495243617213396292229750920824185593641893936515463487974181707181262595338393595608106481709368954376014441001603360110498925563085331998393050346510376362518998821098315481369848233006821050079510528 / 25566042403778876681935667892711275976577619989932365730683580417656203235018252234971317282608904559763388793290348676906768012999410564226547204338671884259591232819572993846395781441894824345233228215961894947205529701668287980978052591030023617525864454604446363792690617823647326214619828202444020049008678746825405691998299891899095 * s ^ 56 + 785582781320160885751283126355756180523821982856251737040197505924038379813636041775649548486184050601234783223689297582058480907321993663936580538682543699927898779163263127084957179189038907297495318312850029948968792138636080241619265094923559087483861487298701226281911437828837919902750381705733638970292449153914415587464442357023510414617746221925573541089305119167241604396996855285812417450213376 / 1309312144667920908239292964855833540579446845845592854132043201982393157588535828745161801535226918154998347904357479410319655652260918383569802917613923991731087395072471382969056192442052998812483385723115913738288583104305853473269539702346222999976885815322050975905988513879512663282417077753197792267290825309117811719589482334455 * s ^ 57 + -8259857833230559842127976898412366987291228336294863018212419888846788503645990180888783715674447599115446010688963125397440712600923444719835944923759136692764685328143645969379627407305246506031991362563747681617295618918940348298824292120187778708567883829911478461388219920585199971665451773449665517170680707233993016055933197932474906329935393593651855087420143513585045903225158154074599140098048 / 5386587061337736748324513545299925191772444109735025219155802646827833958017809481289500956805444832812448870652059427280361755414323539952266177416768874416257842879429943269414474334064340610804655722225898921607372522347122960806471364926662004113963638621696620556287936856647165163170676018561886221556452537092412617373825363555 * s ^ 58 + 604051717426503051687375307165145601010981412065697397724609789960195685757021323880557018666643807364248918183091314624404164829015470087667965811455415829921938830753214540888176064587271066385162935400623959969913548226206279356681227038284752956761241373337131055293115086544905091715656398385191344402000354364804795322474787286872747159940406250158376659085708210394775900433751513702842796867584 / 160822703414478802650041501786226350336298663870495584147426190496630913371022577587838060808259142337276178961852132109216323645349210005081033128976038829893333991845916762110039608181057809026409514442224843101557496691199434888532688044148876433099615611274539455631238192857317950725763695197430709860682057241319049445195537855 * s ^ 59 + -115247706037229605770042856260872077239981332395935255963091865575655347039637331761521652080553333076731185197103305897113352725875538727122862538654239872409152930020751375473608010454347540700577310340310049281435360275777462991883619046151824013269050965517541754772371967360095780084281679639125674705476296031075099401834182586130634562339569232394068712501317831298720870891854054397992501248 / 13075512627672497274967736048486366718761578802759095262212619760367405270472802024020265875257528117918526363752456633250285131036072642735580737126289791202918321441402933616183779995532985725182758785609061842581357831288946048511273168424997948412645651429149571173261711245737070029141785476746871956715056173512196894613525 * s ^ 60 + 55828278954375224282239579668792066110242768587409113920962269318059583288790444173710717923352700307089924828241308745799724182804999633670357942124053996296246958316968018152984840714480577188084293829045684067345360859165698406995182391938897905956759732708463778445204327205684897215617321252453772329824118003624010411199550322705347961657738327470598874159987547340872252986269679350928375808 / 2818734348427272697969983949595833112957347835347707927445535700363120189783265318026291517523320976123915925914650579399088121389567262126705904337676966669020846892339572212317785217365870956869287144019587515510650304570764709709018995697009141439779077537796304681196100555460180595081239049464629659911200189785588297317405 * s ^ 61 + -24177700846759202231103311640286614211992943411940574751940604049586525078753735464936492696881019876070195642168916774787518101576111033627755698147054467697856617088361777096126725268573567436763750266307666450844160116069011163683658973754987799635653798898870641228658861772788723138935928280053976972526189218578883783161154662619268572738077273048927810175272091391439844834396391553422589952 / 567583068613100688641651577849331072234838676403141930333140656027340316594155806382652575907108554115889040448635176983855974953482303632689620700225086700133798740152508973157710540211933805419704896615141191647829677783967777921611928920121543791307200580607916593708215732015025538941505295762905632107080520739380755197535 * s ^ 62 + 20508586200428800865357427332876516654934097639054479679136457013448464612975523446263185890009675908813077994536617405223881705352171117121610953202494525943134451570237318975575725005856478642760458033089426805655397984327998611237365096515024743308250729631059175485184786925331745844838652185311923895971952786269067003766265927703644998989448199355183682088459644058362940555740359923073024 / 234018110868692487414342040226100023892792731715508227219993987720616234042315825379139341763675409585802325592863933337148321795753801588095773559474737806585313520570213583262559074557764316137156712326349616645483738116021505435647821791815766195147570576890547355700086984318919685032721638446999357474499655145524431295 * s ^ 63 + -233622188547549244094877901972486617157918124134362568752219205734241155231227363903019590354987560219577414288486787956926586397234651926514938581273554918473608334199461908065253047355867470871520537839673616465412888793353415085766994725411422004831204407193809340583053022632437088272275362509761323725927805228417789858876450502868992 / 1355439753611597402847761302116312568734634944781831582587373392299139831775209997156007831765166146181357558466133343628991226488967066109538108997371473109570929990480655932675065885172111257113155841020893724071224166369388990230165666428892750522294319328877543915 * s ^ 64 + 181402994507465033568830471332285412076416663807246688719090153183677692225845187417333405544763383668255435027281840981823033074645753006642218970228713863165626544560465533694548627142938751681159884506836727027569822531584 / 560158146390812556134320155396192591967057083516273244447203604737312071883010710824397300167662483275465937254856978473652121134740529652306310560680695 * s ^ 65 + -10086380838582034224565352348790114537549036785126565102927613240594523160588108949571112064165646021930208374728795060429433052314771904628810990609900884881941281931341215024224935832182248213008812015959707549313103397126144 / 17364902538115189240163924817281970350978769589004470577863311746856674228373332035556316305197536981539444054900566332683215755176956419221495627381101545 * s ^ 66 + 385383962326864351083986173595092854662378060718369931516510995374788584374159037365865523223522636893073730685746234163978906486317737295205849802115842437870733686994463964555028219216656097827571840911483948430262063425650688 / 387816156684572559696994320919297337838525854154433176238947295679799057767004415460757730816078325921047583892779314763258485198952026695946735678177934505 * s ^ 67 + -2530580779782742596548973373082703937493227952593804656616766404939758352087564916922189101046369107312415572207697338154171479335876546512800245922631299711032363705606739970674535334224111708078268383587573900437276315353088 / 1561922450518297444882469428009489396648884037106222221289292590987108263927760024362208344911947770826299200705341945267802475333377032416748283944331885 * s ^ 68 + 37201000347432955621057758870089718822167500542247940904805991658173102595111912084224725321634196435996674395949027506434515891664662419408957100400907567667590187963873900069363435269423102705685287101609357438856327061307392 / 14792324384320346389769269288795752521204137057300104566328006302877907676021727289547973148871975947237304194915297246359776384039629542299792571472790205 * s ^ 69 + -5571363829604518224571787637812004270808328980001280060171658833471608848422446381174475001144414954897200120804632171085617432702391106029017229252528277723127228284177253610227161605340517061599383242651275715317281285210112 / 1500670589713658329396882391616960400701868976827546840062261508987613822205102768504866841189910603342914918324740300355339633163440678204326782613181615 * s ^ 70 + 75256433526269922873137885598421904588495816620712679977350878945288381370699767142639013943598706793823701370908383028970626760763384855946444332136028875894836739311852066618418987142807836782106574200815323204507941208064 / 14454973798625660207187444010962445862139831414293287972381029322767681641101926002421048124336406571339975471585478405267821727663042755732899411957115 * s ^ 71 + -96250503676187079014210812789109875854186446613509668847084431637122484322814670075151934763299853634045096839141378721497130594515662809038315933294835257871593247498965533320328650022988373272697684915155952774152192 / 13896060355083833346171096344875219652496759260093084039238805333450950943214880301802259447114033048111868027645546864817977840923267993756037815 * s ^ 72 + 129748034352375754932657865755059375417473766716152736423890422562919345537011440088473724556455967764817078387894012126113757759289937555299427390117130015190055442220734019924711436571243937346672470825667824080895573229568 / 14862156159150326691896949476059979548397291454132535520898804796648461405640008425024457930655741967715749428531548219500718114357776354485938832012245 * s ^ 73 + -1244502730231073342901386294758185737706003189793210125946355878079123715463281740565680737672028986041926568130732264502358826409916069128436785495897477008574274549093426408466664082159963709238367522901350474421624635392 / 119569423328671904240092874671497987234333503762318724564743591536419454665944838383540974871550870364314574658766532750929891330993199633829036047935 * s ^ 74 + 946667027938802016088199628920276808969196872674985948954095564038189204352667884634598392681912115467530752395761188324713164296068763235884888290528126212639454087998888784874541319788339630817293432607065645573992349696 / 80790150897751286648711401805066207590765880920485624705907832119202334233746512421311469507804642138050388282950359966844521169589999752587186518875 * s ^ 75 + -356259020452248142570626608904389415413838855435995715052703714380500946507727758974657304779431360843275039574176912608499689177857580363264520435805106249006426968567724069120359990470702345504212839124989459653411733504 / 28653573518402456331409643840196814958858299099798901562361977791610427874902096405425134518768046411628537711019727668240856841481253245584255485361 * s ^ 76 + 72771335373316997970330272053483392363514231234055329800901717525392775994994982518980704913504337769427863641267964279470629898506516969024349172109203450738220368010872193001571844914644967354759037651568694537687662592 / 5864766509614537845610161019923324699181523207561178682354790776060613892523820901695202971677670318169583742021581686482046721940607389447069836185 * s ^ 77 + -126557713855304388211505180583937039766023729070037432383079187768691179930223394240195128357021150262096602180950378075977217693228291937107299808779059033156765553222659350602757391541585239387773138568298769491370704896 / 10891709232141284570418870465571888727051400242613617552944611441255425800401381674576805518829959162314941235182937417752372483603985151830272552915 * s ^ 78 + 4585272507903908299252699095694617708408416565821230411748200913313569520852945829387596145430206938346324734367862362853569733638767498173579377222835124493874609706975493768856728447924094419190849997323449954371371008 / 450259042040377541110984179372150292745714609715581259383895501757811950932343878750166214540851268353155603128964969127387454842864901619357159435 * s ^ 79 + -5743063763695604784304711545848709811721254315116042321157609831893784739424908883728191180209278050877426525589247924884694899192212665614619379949427904786997657495149865908203199152243560626940413987725464081268736 / 689566902952914502717244094053300964042507137867275565238658527461565419461942492850699937880972406604301439391132473425284740968913273303594337 * s ^ 80 + 104071393016387393845388593142998784438584218886022402398677259433329915204033596089674390201490007395208106364519582585411486123348160848364746784691047070442025293363339768044184408681185646459948038435546746759151616 / 16427917393878257270616697534799228849247964166838035524803335507172587934240394682619616167164342627926004879612273631602371770141757393409159205 * s ^ 81 + -2716645833654321880817023534400563408812073364240472705807353273220497672039167927411870882795047055166448729384952190565837537430698401173505587931047424550624922558663859919768889494845370148735207558818159797469184 / 608441384958453972985803612399971438861035709882890204622345759524910664231125728985911709894975652886148328874528653022310065560805829385524415 * s ^ 82 + 9422220378404974292592721154967696422209190373003069970451503098288015996100161710949768503504925469734078351210323243820588107958472221315485036234811108473686247372964289968559166053970290009786044840903983497216 / 3245333523009554640307287438416401865269967477686516739518970377261588916598125795632071969750207518125461814573991273109166213067725971274245 * s ^ 83 + -6166694225289332069131113250141269616755329133142266273612542272626929646060994733472066256225879337232626479053822893213280130332313706311461645613204010784546917905947449016671010955508576389747571418821040275456 / 3558136754143005689975459721637259876380325788788831605978630172660296282053366836174922280087576917462855724412448263288362956495940522722365 * s ^ 84 + 1046129271305245064608391383563483906949207246446723154234045347555565493745283661863447471482701548556447433823134562729421149822828211226257031336521414119522021229598311275900361316057872201146985967474360451072 / 1107844776930972467574776836407205456015852351820698485377961775370421919320645351922594849111516622653270097344535173551321799641593203045425 * s ^ 85 + -2642928466779720973574293655575832407943670007379013801292574045822199961628571013845310396818538664969037273438418190299895889888528554742363848964199140626024149534806800907202790814715143900907161136928898678784 / 5666662238079601654405361778903784247568666996959991076188188793496027412159065702056357705324659535218622079619825011903689152937979351002285 * s ^ 86 + 983333567619624958455300787072265627886665104901369840497307557727693423514632880212892106924096903280259075307194512122415161712442339393841298762467585690459931919517432042633740563996314379152651111351975936 / 4747456446751652404384096246951025369911637813428852844415931677347531271200719496161617028872313347431461514053876219708420783914528417711 * s ^ 87 + -5393327636884258734060758505024755249995180287638817965392980085966485516894125139199833912350046158745191713873236195305717762995036534713253428378926399743596130211362277094392438126002886318831806619582464 / 65858492126955146315276800889134319439915704902897284801647882959636779426090044536526593741787937835949723738361342722867509883871777495 * s ^ 88 + 107552996851187846491432181763291907531758055056485545991644933141413778260666092459347931150889061502415897067902694894491409765578350391233706636242012638605150518607389605675288518199674412366554906805403648 / 3777350403992694058660653846552348410542720763430619823845626353751611726638631221083891965501214834546360821526902790393800955783845726991 * s ^ 89 + -419731767156326294245972739684582386281390747291287253119520762728140012279647302668232822098550276811312228479710630082202770023818251661044868302953685529193643714359614590941031355493609847546106320257024 / 48971699273889724183154544250894750352757831850872339980712528354601707778374648501519774833637184544680563805448177922132250939289270445 * s ^ 90 + 17571644825715738721351876622235531904032484708210880066863294754186955282755664720796459295868392371070228429616046123697591016895102480364114863907348466033040688630947878285403294635251977133777267720192 / 8029593934998134956156871219516076183965698555728617906747459604087847581679446871420359477226997826244921272605016560205468172027610109 * s ^ 91 + -549252124239892601318937540862135507991820448793354263162546401729201279407282492732082799714682847579249760288167738206568818931141924512836387977719789456633959785236766509194506083108586111479022878720 / 1191903791851284292288417479122306093241725008010649544504114446725755850690599910618999810765772745531907902143183166358774361485347323 * s ^ 92 + 4256594274913768364216773952455309242577653348677142953465491474550755612025461869143403101953961621158321703879976998409173772874436298026193740863212661415244983535176128607401525240169584508341846016 / 55395828406881278951935445056658903883798313715637385126877882831331981066579606040763109645785539897285074912201916277544235691223039 * s ^ 93 + -266315928767188816827474490330160831869539681069045302414796915727567668094385512258311389367655325276239175380977822687888515515055251244023158993779747947393173635571013966532655130188252295473397760 / 27995741237886237749902859329709338521919577899300613988852263366372076453002596601245872616687315862068801299714946935963215886962181 * s ^ 94 + 31530550229811609956941681977738153273239363107937012582142766771614807750333388280176615344228120139642124968177862824428073987321319034802889352006171423382005119263064179741676756234052793532416 / 40564255587572524765359134238120752834322579126569943246258903680398799100667226067541491627930984624365684793303133667604751151703 * s ^ 95 + -67132692502371237677000504867225426865509358928419646865033442624563543234590557090557910082661779919043179397776003395806367106516764345444797668471551678030407084239537232648891943590255656960 / 2134960820398553935018901802006355412332767322451049644539942298968357847403538214081131138312157085492930778594901771979197429037 * s ^ 96

theorem G67CenteredEvaluation.primitive4_deriv (s : ℝ) : HasDerivAt H4 (D4 s) s

theorem G67CenteredEvaluation.integral4_eq : ∫ (s : ℝ) in 2 * G67Centered.b..G67Centered.a + G67Centered.c, G67Centered.densityPolynomial G67Centered.rectangleMiddle s = H4 (G67Centered.a + G67Centered.c) - H4 (2 * G67Centered.b)

theorem G67CenteredEvaluation.endpoint4_eq : H4 (G67Centered.a + G67Centered.c) - H4 (2 * G67Centered.b) = 23864279707709187724385225758724312218854734536029095088175935240939654266800114901408759002778556310084584284244123564966192288387857611007334123363670697765493451162331125352164997492418365688484887506900039695246075351065023598449268688713542573598036842856126716530754269508313202462153064617404356307153129700926968349151669342154292029033940080234673301437491702815115290169727327107710204435940299845596222024457533433200040042590218556034047885600417972095300120628616111493075648816798611797993194224232044705047935115775205682194054114420582752838605920 / 36977050014516061595484595557769036283856831939068512626959159178763157059271647062970008158792250999292177595055423470321783877674508316479414508840944197170148667885397825499692017368164063191938593908809111527233785291570843564742109529036612148924245464726566740756578709436133588279096405314147388735532814556842337238234760692497556156996824077430332938124041528353559066178644591219386875511217946922357081402975818825293766764519044042607662200618286900872616072044747374341935497723529871820139339584227738094768353002210942215372067560035933061149887891