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

Equations

• G67CenteredEvaluation.W3 s = -7578838387020257738567726937525956651194941568095381673200578278234870329210204782056236909529698655514244886141256020367390474179789213833737013614930988073463405841473633299964309436462865616681067910828528688894753960476200212202231566206500676764815923502002452779556686797079259852110772258036123632475625134335325736062357845856913632405179110055483397814387226763128829230465970338850581843145777795696177588902888651686271526216385724879 / 2600007567155875774643944498370204234570535076464701409277460796131512449806129127374393759022726164004227049760580056919566531912168784662348161630582931433325393572768519224359507958694723607770317323450524174894015321763877879251312139825627356088761256157054879357954539488104502205103862110868427079420115012763294115154925331734751561526960836232008140698337213600671495042532739961900146556355634037570934561901579926976318417240400 * s ^ 0 + 8078617182989746089920557240934366362321138229510250907822303058207017481330279510866283611033765532 / 26016531848676609019733212304201985278528371719929018837564202498970513101376639717306762443 * s ^ 1 + -139480152547460760035685504087028072912818627287976596401390585792818013986438518299075042236775440448 / 8672177282892203006577737434733995092842790573309672945854734166323504367125546572435587481 * s ^ 2 + 4677602020288785099112858884610014987447685584069262214773174646276169186432692107820546885417128089344 / 8672177282892203006577737434733995092842790573309672945854734166323504367125546572435587481 * s ^ 3 + -12679509716226014406942661880972976901615544884569280875369056066660899996998258787694994880889637648064 / 963575253654689222953081937192666121426976730367741438428303796258167151902838508048398609 * s ^ 4 + 13776904209087355277591923967977557732870096953883997991260261885918350497275813120181272446153347469824 / 55377888141074093273165628574291156403849237377456404507373781394147537465680374025770035 * s ^ 5 + -857059666783063086910063004567667995322493163036250796660639049101946920420002849805097084605933407232 / 226032196494179972543533177854249617974894846438597569417852168955704234553797445003143 * s ^ 6 + 6543470652493472945971075908778725725232303655070636180172008100568142006186783382623568291665525067776 / 136735526274257020427569453269854707169998116981373838289811805911475401149828084014247 * s ^ 7 + -23235839443405529689126904086773178181967266847251833069891843721241114085983823079675970433056121459456 / 45578508758085673475856484423284902389999372327124612763270601970491800383276028004749 * s ^ 8 + 635785687348050001790340544606910499496201283772813428971876334884229965992433755488760331128900420718592 / 136735526274257020427569453269854707169998116981373838289811805911475401149828084014247 * s ^ 9 + -2788156352406038704415841764274159982987893571895195003480166094754073965471080789943311667994065753325568 / 75964181263476122459760807372141503983332287211874354605451003284153000638793380007915 * s ^ 10 + 1280446754232681169482374500092872504480146913320977623254315963166451203889471889928333995309717623341056 / 5064278750898408163984053824809433598888819147458290307030066885610200042586225333861 * s ^ 11 + -5451944118823823869375241913950080107068056647871870459698896386720221009009260313092454741174265298944 / 3563883709288112712163303184243091906325699611159950954982453825200703759736963641 * s ^ 12 + 8537453446165095675558212783646541790111183166234097398810122029538565936249494554174872122173917953916928 / 1045009900979036605266550789246391060088169030427901174466521738300517469105094116511 * s ^ 13 + -7250366112585666803598359175967680821645614784009430755249496672414470599561512769660884402380878525497344 / 187565879662904006073483474992941985144030338794751492852965440207785186762452790143 * s ^ 14 + 152378039033501086182207577089917789647928833943860282106401443685061678433125241502660122883242364581707776 / 937829398314520030367417374964709925720151693973757464264827201038925933812263950715 * s ^ 15 + -4222396398862659733832894172322050283474990318793705979188221112434430547249845477846083132511782007324672 / 6946884431959407632351239814553406857186308844250055290850571859547599509720473709 * s ^ 16 + 79736822813405616277970220707414637917183076202458608499126566740600552289189388375349941484565732707008512 / 39365678447769976583323692282469305524055750117416979981486573870769730555082684351 * s ^ 17 + -5968805440899147106002772263356078446231487521893830088343364720440602505791885404380294809350322843025408 / 992412061708486804621605687793343836740901263464293612978653122792514215674353387 * s ^ 18 + 233222031668442917967568371362585786740094768921418935842483754292641008936219605981583207249381288686125056 / 14665644911914305001630395164057192254059985337861227836240096147933821187187666719 * s ^ 19 + -6871276635402816514865012599003024887709966904759022544673602923514991596970969647276425999093624651907072 / 183780011427497556411408460702471080877944678419313632033083911628243373273028405 * s ^ 20 + 20064252924276378107143113245044747534109399700653243107152149448671016954795879004867106611120854959915008 / 257292015998496578975971844983459513229122549787039084846317476279540722582239767 * s ^ 21 + -4111223541745591406223590571929765495625739267804574422084130370660980699968747135221421059595614046650368 / 28588001777610730997330204998162168136569172198559898316257497364393413620248863 * s ^ 22 + 51159287742265107998087146450626387918882585855340219331075829148728559631924376736629119843821863059849216 / 219174680295015604312864904985909955713696986855625887091307479793682837755241283 * s ^ 23 + -451213950671484280021112432315152410305106046337436002427225946900234135464711214689430626444823270260736 / 1361333417981463380825247857055341339836627247550471348393214160209210172392803 * s ^ 24 + 3604460453368309198709623193851957542306882077983251691824511837911715963884569020480977171430397645422592 / 8823457338768744134978458332766101276718880308197499480326388075430065932175575 * s ^ 25 + -22807950491929519166413356665398621443385937262400044186063187157536974295324088407310444349518470184960 / 52737905932870654599871245207337616826365721382329881951376112634754417065877 * s ^ 26 + 58669044482115533849392834485259942909255425741160561326091859041534846265163764053586248183647058264064 / 151259268664607042313916428561704593315180805283385705377023795578801130265867 * s ^ 27 + -34022543897461792170625078627553530073932155695694952443333074627163287586774307971017898988395290427392 / 117646097850249921799712777770214683689585070775966659737685174339067545762341 * s ^ 28 + 198522267738438232958656613086803401918601429766412515975964401596236756418892699915827136261883577761792 / 1137245612552415910730556851778741942332655684167677710797623351944319609035963 * s ^ 29 + -66626350680455314897770027273772454053239966292864879310495278971162938734031207558366542940124502556672 / 812318294680297079093254894127672815951896917262626936284016679960228292168545 * s ^ 30 + 110315109338624761075226032182003928858353577560921152156687555350859357463220044503142439479873974042624 / 3917179332124988136960806933904555579145814023244223226080702656697100875568317 * s ^ 31 + -264888946789315446997717729395436455805389847392255923200082204290715707583697176873021833469419847680 / 42120207872311700397428031547360812678987247561765841140652716738678504038369 * s ^ 32 + 28886137518384761170752565121662769911328801233066455280330456098830017043044553092856134355514294272 / 42120207872311700397428031547360812678987247561765841140652716738678504038369 * s ^ 33

theorem G67CenteredEvaluation.weight3_eq (s : ℝ) : G67Centered.rectangleEarly s = W3 s

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

Equations

• G67CenteredEvaluation.D3 s = ⋯ + 67714017920995425704140058703673674605978032895973730405179959173966760328539828731136477822022388122392906393059695641434702539833302673031571153004114984278801176996830084315642625814124314591374184740731741498848511268345647330929036631271404099066978025804683148884914056232815789242759627181483647814264231802954497525469258259486323566447955250833951451251798714017345772679718666764620391740999402596182327243165583880885404034163469688131859962202492647818804288021405753870618541137150304847125765493628341276614336815201460671770044673128907877166573176972926986615679089393740353093121001806763915246026171170408160773300467206180569088 / 62717501057417681179989235301137784372266794270319717590140857046542060801068803549063337762986906878205152980883593981173749268077496539782893264735306191006044880206636838686903436287807684036716682551482372313993708428036647597666071366048685053597102371842098983902020991101863523735908663796776026446800431458518459419045036032052051951703659436201320926710022745954655016517454066884984093038531028558739248472948704007444632390423639767816049549850350993981819199601810116182164696189015352929096781897084172737331229576420970549341346606778426106159218163602116174740780625 * s ^ 47 + -12140914089621779791688767500705756500790602132153334965737237812185153061067247134781795957750216781761260743048711715925293996223148970036751581391017243154888430718950209413620190440618534182302195590414037428264761884498642078318353868770686097401510641400501332005549973491977464011232965426915926485682267673185129941755797135440978982983937150435211559874570647471268432574087094097324411053665456382683656976744427213831200640461112583299323679253439908736095975759314207571906273286439793486233795777949975577909638011065087520236796073489573682212445554161696061947837468026106498655054838132394662102303660559059743271048808021098496 / 2956356993437555410247222469724825818138296517269601315961884596317102270800598387204679122694457791044085219724628292857405293769910146759335726978982460933867961733950716387865639633208423606562778843182847438727157695689487543117371882063839558746686976248025954957478524085724136463967514866641253566028328652606940609145117164337233924848582029397685669692663450758278897242840407851142767253132903869772032504434951058591659015913935341880864012308734014688955691426599836637986157200190131437913534943447331793976849083774916227969586828339865559793071618406075094263125 * s ^ 48 + 216697680055379988326857802847799398382125222047814083439606280020683054856343631153392755724347403500425147482445234380240714746646745903320078403513779811055911579615937714103724229755724587920453835269332918741920428422469037736820426426890424178784163449409030571105290520717273289679353954530513201666706774999313114855780806585331832214113493684344723120278836300015633186821452333378987399605986688422058498090250389023955211693804871137857380893238118082854781685486012209949025317421228871431198192419887626028388377664077422127405353310908522426353840880892399155752295906021514753140084615406170467396656910993557919361761738907189248 / 14447103043402393419887370182240186545241864112694844166681662461247726191270848722377582882601218261894680602050542034906942850686919396427697231840687875129656643190438406499192465377377013473580372082723726162836487607237307050328289008576121617271545789589409855358244108267972666871086534914341220256629002283494294674878968784214029934637410294603784687743393089554608195960295577989546730538894756646621819219785892908966786511730363274474410928074756788763009888292252031872422919148098944196596331138733187446037809673541571755549490349811795848800104701267423573851875 * s ^ 49 + -14339065333145543347054013312793973863191180911634857508381491533467505990978433352530972920699077496104311307402725546128266909397934195570520442807343194772742218546479149375911592045712000593105729045551087209013668427208591235716957534867611577226754668100907468927327051234544168312789226097576641188789609306706798554904669008863776879094762026254134175633811322599879681396568808074982345256032648972959369116794340044438094386910313869026189713911549747146704667690718988429361609929961206184821948426148201139926418460656854305644255524697406497593102819445170563196942827597478310238658609446264855707739464824306197909484908383830016 / 272586849875516856979006984570569557457393662503676305031729480400900494174921674007124205332098457771597747208500793111451751899753196159013155317748827832635031003593177481116838969384471952331705133636296720053518634098817114157137528463700407873048033765837921799212152986188163525869557262534740004842056646858382918393942807249321319521460571596297824297045152633105815018118784490368806236582919936728713570184639488848429934183591759895743602416504845071000186571551925129668356965058470645218798700730814857472411503274369278406594157543618789600001975495611765544375 * s ^ 50 + 911014767931784453888796525145569594108796277655421427670093268142980029517580704359175744475886291392684213378495892356876338346333518603395942283046511251150681005299447522205202459246803458886856836391445631907941576002057642820477599004512016304972244013579897664485458691112971014943212523840754098624087991792471815088444756259833098021550406015594537268313574200072815801488737106680218726742109945216322516168791001961908156153273365508508208549868255634608363040691282614356132192081489920247218571669900667709014900288175926027251586482894888659719154215470353616375703954068520702854064048397683837320297313295271950456236275662848 / 5143148110858808622245414803218293536931955896295779340221310950960386682545691962398569911926385995690523532235864020970787771693456531302135005995260902502547754784776933605978093761971168911918964785590504151953181775449379512398821291767932224019774221996941920739851943135625726903199193632730943487585974469026092799885713344326817349461520218798072156548021747794449339964505367742807664841187168617522897550653575261291130833652674715014030234273676322094343142859470285465440697453933408400354692466619148254196443458006967517105550142332429992452867462181354066875 * s ^ 51 + -55568378454309694975900408370093987971420968474189751338376211326507601726091144628906657805022960016221255054773808592721312816812422835461482155727225701225168477229444208757311564084620674842238371012552783256291604769527706219917872825634078483220434519303216568933118887565266126391681801565570251624928725383164426739497636141564789851811209598224255502119447945794377687765168004751333820504544607610421513429569102395231061570949800183421976614658211737603674289380022556811449501872949269677700235200532199370318942508209028080593233792920640293992786501972918866823574394333686040991894424168613398793006660290297448477460715798528 / 97040530393562426834819147230533840319470865967844893211722848131328050614069659667897545508045018786613651551620075867373354182895406250983679358401149103821655750656168558603360259659833375696584241237556682112324184442441122875449458335244004226788192867866828693204753644068409941569796106277942329954452348472190430186522893289185233008707928656567399180151353731970742263481233353637880468701644690896658444351954250213040204408541032358755287439125968341402700808669250669159258442527045441516126272955078268947102706754848443718972644194951509291563537022289699375 * s ^ 52 + 3253662520006361136120381493413563425339569261436792669793042736871273308161231669096829234995596976668529500992447518626990713884683141301660059721027084951147587483567466681222948917059052107748732949460821431985607094525512732875598437692330345104152298208128709940303514872311901017693657785366598055269768275797909000504929604379570729217213550179367630389837352615889754036337515635303263344673344348604419782922405182287344491469190761346830684670336168432928751936232273243735147997853792323584377055035406410509917446417435805569942459411176050324853080869982438714167128033735338626599638500161124997441115036391704337157799804928 / 1830953403652121261034323532651581892820205018261224400221185813798642464416408672979198971849906014841767010407925959761761399677271816056295836950965077430597278314267331294403023767166667465973287570519937398345739329102662695763197327080075551448833827695600541381221766869215281916411247288263062829329289593814913777104205533758211943560526955784290550568893466640957401197759119879960008843427258318804876308527438683264909517142283629410477121492942798894390581295646239040740725330698970594643891942548646583907598240657517806018351777263236024369123340043201875 * s ^ 53 + -1511136970124787117345027742436728735928663864503919816477159991928421537715824928680408669417326986265909779838380194036021449165275455790812869599290708399420343723921749165576776231986587260899284078531213406089614544429148626153861855384630152045883396325919613610775159526314749241961390857547028846037629502873842369663947326839929778198981769845763964828375247876416374125208283357564064397760890279333884582705905751370234304226789130555276161298332700641451181767046027649544635344918119953009553520933244555619239510054614158521998346608425252321804324544927792529469577950443230691991044320608846033554601477687073553233477632 / 285506534173104827855032517176295320882614223960895743056476814875821372901357971772836265686871357374359427788542953338805769480316827702525469663334644851176871715931285091907535282577057144234100665916098144136245022470398050173584488863258311468709469467581559547984058454579024156621120737293476193564523560551210631078154613091877739522926392606313823572258454177601341212811339447990021650308320336629483285284178806060332062551424236614763312255253827989145576375432128339426278704303597473045983462115803303275783290294326805865952249690197415307831489169375 * s ^ 54 + 580019575125488069839680303324073252104904405522525672665114716211849137453072599668237507182303440196954505772900719225471448862110712013302448020776767526308435118160692033730766413441617736148205769951324071807408538175675666429977235770376559447045950552528810629684241006702200095611438311481075115102103199707005779189207418222398938212865917628875037594273394701140057555160945980450709542641053688542182246503586491824833059967092628119602258773026091088629040293043880303655378366299828246016717416933980170682843191703669976482701446517169249194555958452281013794673309556369885684423453466645120868271958206575111961374097408 / 38342164966643378657557086102476952083014784793860582585830959600415522886863834167051263205451092388787448126985235687009431861396599502780889932589891261922754137211637620555839921411569272422115627720141926127065091807900293086574609492180084004121915433493195011438480658162110902276532307672042862842738458187232504284635636164392016073556152614166451334343255222519159030799303077920968501317765550202183659843935222567480776435873843096988191767908671683336975295701761963452363732764412091274765814557172252715171784823100492241709458615442716151218213306875 * s ^ 55 + -170041907006002531949412235350846433006068544149480100962400183816820447395653724707320235323513286656155187122603667882874343234958628526067814155091069783384514901244777601552203335050739317744693367903517720920741546483249538706462707834427717225300871755754131262114593865222319034129426433075525581727811680793621949279122547687172264751625844807736007053584187522693661286377271334420473186573922880886820921170932717361418193077823788891885901329045122951818361892878838968854710609493792164780495456147099114276488136340573393874231351135996467935701109872219172974809781594179282678249050400754394719781719679554152505293144064 / 4099476757439858095462078388315145820196549317582578012321549139667068484759026294590386632029362079304318353199679287290316614111586110360220936188856298444571197060363770751253324930796714661484060825423979523019538117825817499822442524321141057044481524335750410028013655275194247413214146103300180303940589869075173414080539715689712410380217575099557689835442382281922663670365737890921160518251662600233473065074835117277818864212926620432699748770109551048607421553018574708743292182358525482207665707370618214829687685488731874899753436871233802331507083125 * s ^ 56 + 25312033084282693882292527719128906942102169344341261723189921372194175153434210101975410674373938274304510983125549456049343953415060279710863846089238152227677483087113190540962045494199106843706319112623219074123460294731465113166636371748158660192814885815983748450987295556394094349584355407498780114209004041839411701948698623342236294907239588491416851755754844864496895948825725505185489834316798577550903801187504889586671381935900677198277378420308913150513978267938597361120865169830200913781225363316226253517910453065032475043971087371450415471662708914673779865597928686973372555640733863215798524070125041340167929987072 / 232045854194708948799740286131045989822446187787693095037068819226437838759944884599455847096001627130433114332057318148508487591221855303408732237105073496862520588322477589693584430045097056310418537288149784321860648178819858480515614584215531530819708924665117548755489921237410230936649779432085677581542822777840004570596587680549759078125523118842888103892965034825811151152777616467235501033112977371706022551405761355348237596958110590530174458685446285770231408661428757098676915982558046162698058907770842348850246348418785371684156804032102018764551875 * s ^ 57 + -2193472208914760552381670270064162765223832486046613278264313054172798570439364326637522090806446946519166542699865507750011034425239923033335007738784698889532335192504024918392988887763881080111408627943198913506950978119009526867666142256190693188509189167865769139596317872407126996453276009991463591844342977731377127703368359004859493554109222588714877352780947188055926983488890169761962442376340125605197846232793053389586250332767513211944192839334024113238874412784171142932104974777525839773415786363367168953179574581613814944604044627598020801385420284049884505090884973854862364727135368385156405374022025035695259648 / 7974906491896379310572921130393029859519750757387122213185854872544861626969958573030066573736179919937901307078300792126627748263458614407283645637181616553683217799858321809588082278073239726102984406919949971538668872351783980496807732213476699687930333871709026661012816484084621470826881789603246987027625623873251695040608574098696053824295395361820397425609686044121770325214888698739921676912155114675259392769211992829097075195316032255221310055519341711180926166320540162170564524953020798113140836092065929437751189071683863342755500705643262836875 * s ^ 58 + 6101159388738889824034824327563662510017331848956615554171756548581940458751126121776635747025437759348877417730998492560781775371173084210276907931278001057891064909198552183262263054104973866523316100666265569807053597532822592098153537496415456617176307261966494232057056538074853128672002281705796907514250181807486820585381413293116149907832736747479243376599562420434039199301971833226048000132455748228339596354355771450557189833112096972211852710837197644257659408013287141469220433368455310731056031943042781983895229326333136733495907379624954635520993441470241589528139689218855339033340750346801504549702798168438079488 / 9178665962371304489527324319886317385484996154728574622723342400476161495191839112355359641469942926720980749656157515466496087623980669412156648752227898297635401618704860950657981489857879684760038657021074495544505683272807977552929654057020352471014157852344351440033618972248337919253580927656567286956323831250346290518436283396612439307207907869264985716267751862102414902605815294776136269653612490475298546394753425708960784658759961652235847422390185743057292380104772639479328981549703182733992283049358899918921179874956899319020481944230925151875 * s ^ 59 + -88846572515956765068009981238310645405733313735513088616507813148269792081829165805840966598232971788920735365931094969869693474656516173987736110594264443796034012745616591723714649248356694094093176984963639445954081360679138474879304694204942705950071680681586974651505519572866765114809752664274717672724374052955263197063792592475563035948041816718265983182446147288144280798368678129662872001439647756628651128858347371443948378949726502343978058159185250671856232986617273292626392901042747143323378679641887407903825464463234428553518441348539579195920790743610140389168613340998096582572519385248845611756554894406844416 / 57727458882838393015895121508718977267201233677538205174360644028151959089256849763241255606729200796987300312302877455764126337257740059195953765737282379230411330935250697802880386728665909967044268283151411921663557756432754575804589019226543097301975835549335543648010182215398351693418747972682813125511470636794630757977586688029009052246590615529968463624325483409449150330854184243875070878324606858335210983614801419553212482130565796554942436618806199641869763396885362512448609946853479136691775365090307546659881634433691190685663408454282548125 * s ^ 60 + 655945585051734316002410301111061926626784734071819787155746719691936191728608987285916179923871735497348035558454337187959134758104832528758561650361878438273806503020426430815828639245421961186999037039328013492938315422492331491636786439847640507423423546625960049350743904755162717669693771412481999873907045426861974517815038568981844779143039274642768401209927129243994188529137380256595958971157857491553549144364716230704812199001295126488719301087585963347285691392426066933684280680419565783292591663087296722120890898374643683160490407376956020094156637814241103472156951728470448281189696804890882070835287906320384 / 192211294837419732572347796366433886572257159858617775275340657141460463116282518634543581376456828402843397266269292305540931200636204414636915979147444103985831290572421857279290965800219456050091903273534112946715508622972545757395967877557857149729109330352948536008912926355377419622925908899054871672069269600870024721346015609419563991942033126070927181878997170064758547161556662299251068407296138263047317370526530808723238009313759588973171265101463483824205649490184336889396037558890607558352193224496029567125022090234265895734728330036456875 * s ^ 61 + -21263865431049853293215179502302344211023745344854344789874170544935275127510691050473559388467621955366779263408929708491666396176193510067007348543697154875084678500287306910060903677117021741938102173247328369942417208135494552364059017509987559765929709294300079397697677246798245494564891919113153382516138408729844428554040369445713037949404481290399381109750538809376082352279484926481813138841582328470319145729512407651529422970723165425503687708590172117664489932469349986730739199338019566025131156008596058256144008662961362914813245284064547691245301834780993273722241608321559867132723491099693131191840919257088 / 2935841879816833291760927707304021627788294445279876172219938159393376345891107652099946885354686507500752698586323422456600027323284344158874727444300583798525725013235553974616304059841626911816318378841042156418835261986103574012337335057038249366931589053009995608402084230046195987052776685789697051594948412591905139499444982354117329616365285842952167198511187682929825068954594123169153785196796361609887147618105142630992853691225438465897494615206540184197211178196885648804791229560772981574112564974332886470013814495941168218769435409361875 * s ^ 62 + 17106386235373370010622804379651357289038571886603324202868047692700497003069512172902535298958262765009047430161877269352552536837753055381950893175654093512852612419473606621342469307410691760240847906837245904250499266117908029704720066668737717775322859948673246822839701306911887519022241993086896144296915982519741492097636992258191509454187480640413417779174032219189381663838325531205877120378762233636072124687629287970513160299712604347915943256698863789139839368563482982525522711131263356245686003869740425835159018142411333696468352520639082378825260762614798220526617001145179393385738806759977763739078196461568 / 1163258103323650926924141167044989701576494025488252822955069836740771759692703031964129897970724842594637861704014940973369822146961721270497533515666269052246041986376351574847969533144795568832880867087960099713123405692607076495454415777317042201991761700249243542951769223225851240152986988709125246858375786121320904329968766593140828715918320805698028512617640402670308046189556162010419424323258935732219435848683169721714149575768569958185799753195044223927196881927067898583030487184457219114271016310584728601326228385184236464040719690501875 * s ^ 63 + -14269834720641573262410032938185107574937273642324364028925608699399277527735924686650829850978884177526630008345404061650959681680357890088646637728153757494310655983107840879264220794315920223892681167485195514263537050053595824652288 / 499889961203173745852563965186902561232507457197267571201417853998668152265018749307073011096335946163944053299943190731326488150187235798786402686280038088994375 * s ^ 64 + 39918028542879705503846882995837218522924709017742581212275248921410994725773468385216747432051676105520513330391059921692969880209971926655692964546672520628957040316170847767608770520289730233678290594324577298955996708456238153728 / 753981841935405348193912466345252731874068562891806291404853475111113351832607465018209669828561004772162976319672987528395909728789194266646157897858277660625 * s ^ 65 + -918884443045053104585760024417472265296977563074416266309480283479847909345243658434120587781178977143570359433030735355182903185881261781308026468079457360928064625220992548576536487942320592853834431592923479683555031629893365399552 / 9801763945160269526520862062488285514362891317593481788263095176444473573823897045236725707771293062038118692155748837869146826474259525466400052672157609588125 * s ^ 66 + 172466435807102294015261705371225685883082479855656240940333184444148046895151649977045003982664058599549960506701215018134492723774593287647519846925695216649593471163508950930559935252553346482131085072365088078882362293296136454144 / 1089084882795585502946762451387587279373654590843720198695899464049385952647099671692969523085699229115346521350638759763238536274917725051822228074684178843125 * s ^ 67 + -92560775814147168559239812533191323062517127121977003910207250549605922470735975170411064812244512593790458419119488246212264692407443248689956039241027277876462124998200323475082518315609860018118919242726676150958477938830662959104 / 363028294265195167648920817129195759791218196947906732898633154683128650882366557230989841028566409705115507116879586587746178758305908350607409358228059614375 * s ^ 68 + 574532383616214929358729533292246283822471490074841619553060432834788811011373956541195268592508021990135796779006285853296107151103382452379043346075950692591578142173267313379188806170833837007917249415468870962765484057130172416 / 1469750179211316468214254320361116436401693105052253979346692933939792108835492134538420409022536071680629583469148123837029063798809345549017851652745180625 * s ^ 69 + -134475011576144872811407565409138886997640892549754469344122157616683501359808422056918779816782360462098899876007848415961704291129707389935335345351337114165080895756783152748877713160204816492393315703055140259520259638358441984 / 235885831231445852923275384749314983620024819329374095450703804212559227343967873444437843423369986812940550433320069257794788017092857927620149030687498125 * s ^ 70 + 20703864980319421067919040617705730261017246334532197995822046936989034785351206165901102564359507946073756121461139581908334837807236472940028565913553941216520261441995858666605367350433346509653894685159866482548066373293047808 / 26209536803493983658141709416590553735558313258819343938967089356951025260440874827159760380374442979215616714813341028643865335232539769735572114520833125 * s ^ 71 + -10652522204788861219795614125222412151440593425757205469257014509870472532017501443584972402078729289206826775945660761617782839457248505147426641083467089801098671017018557714212732634462697749739089470069694291854398473919004672 / 10255905705715037083620668902144129722609774753451047628291469748372140319302951019323384496668260296214806540579133445991077739873602518592180392638586875 * s ^ 72 + 33919851081594356125743294686478650689414381358178823485894375022248386394806352056210414315466989637626040254524240876055192209260162661461400368474754607205603005870608632402089038039167061470124600441606220307690202301760274432 / 26209536803493983658141709416590553735558313258819343938967089356951025260440874827159760380374442979215616714813341028643865335232539769735572114520833125 * s ^ 73 + -13329481235635277786236177181237096548859864891007603578121818762984613223131232389768639458131270925403563929403935912130560618609548223327934164315829450174727362633967050444915682580152435626830019454248415623591404633969393664 / 8736512267831327886047236472196851245186104419606447979655696452317008420146958275719920126791480993071872238271113676214621778410846589911857371506944375 * s ^ 74 + 2120438626162083871766327170374523093675365791836387750111114713739909553713123633571719874176242951222562243477443823040289444717866613874257524177716924834639323659373906522628034888252633321639936905164074059428446536103624704 / 1248073181118761126578176638885264463598014917086635425665099493188144060020994039388560018113068713295981748324444810887803111201549512844551053072420625 * s ^ 75 + -1731445510477726616270149621245641256813789532758829994207425292902522450131295039352475571458546138760318050238917070127388504753427693250089575173436474271186789730497834180957752773423121307558883217748584160672827353096781824 / 970723585314591987338581830244094582798456046622938664406188494701889824460773141746657791865720110341319137585679297357180197601205176656873041278549375 * s ^ 76 + 1906596118395452576255890841384556661545529996413411407062643869473986293852436465502460078437333535300725641958575499303478766823480493671613808918228222945881446716406483165636648012122540571707796685345833267876824115838976 / 1082189058321730197701874950104899200444209639490455590196419726534994230168085999717567215011951070614625571444458525481806240358088268290828362629375 * s ^ 77 + -22980197625882964171397677185072973587628961928859168848500412762588029751051794894665373790893182442208525127211296955669610649660455731367076757634826564213337338027682087705417190575924849331447018108178310964542531849682944 / 14068457758182492570124374351363689605774725313375922672553456444954924992185117996328373795155363917990132428777960831263481124655147487780768714181875 * s ^ 78 + 9850654974053678041663682251317063473667906867699896733281593766303183812347000758491386204084077969536881354413734984284205113905460413113288738532497717622932058379639336801548166797638801855078065742855604755096454299648 / 6947386547250613614876234247587007212728259414012801319779484664175271601079070615470801874150796996538337001865659669759743765261801228533712945275 * s ^ 79 + -199554691011053094440981113183265754845627080369240940672512161553446155781731891015743620705080124165209152225946343671525902741721464053012429869181870054045389694928667543817743934493592885838727837061283454939953379672064 / 173684663681265340371905856189675180318206485350320032994487116604381790026976765386770046853769924913458425046641491743993594131545030713342823631875 * s ^ 80 + 5310222865573342667302609486663704499187169512282467092166718518587190449875505421953717760254107107837877427340162361990810446963879168785003128327603689396307266319592200390170673645679079196969648287191172834126163083264 / 6130046953456423777831971394929712246524934777070118811570133527213474942128591719533060477191879702827944413410876179199773910525118731059158481125 * s ^ 81 + -412368480381295495859156354646369708538790086377753610329496380110116013210222914921602680267731239749326408660035345833042669495499137552753422820593985960965061047222320506792319909008220114450878392306271865582364131328 / 681116328161824864203552377214412471836103864118902090174459280801497215792065746614784497465764411425327157045652908799974878947235414562128720125 * s ^ 82 + 27614970321433895142630121621760920280387095903051057971764381539065360426293660333294640382389558741564891324559565811957046653445478440660708770605225215532127412324403542685250714838784859888098018925469082109083648 / 70706563704123831018743109853048112928070576572085756272652266251582810733111776872706788899176207975223415036401215488422597212419330900252125 * s ^ 83 + -42539673991601754306817351230231574119753564929418405316747031440467611134179328808344961654026202466254576696416459364637345271226351245671738958640950982109507072784479667011335783945146363734282364266352240825991168 / 183837065630721960648732085617925093612983499087422966308895892254115307906090619869037651137858140735580879094643160269898752752290260340655525 * s ^ 84 + 12786330150282911308996569028850641538553563898935080398480491403402675459463477061496430389765438879328734996499361502353706705118999735937722893635262763803003572927389113468536971566419867935973713489865639488126976 / 102131703128178867027073380898847274229435277270790536838275495696730726614494788816132028409921189297544932830357311261054862640161255744808625 * s ^ 85 + -418281597627085281142464385299697337774341406940527318220426896012976036818604573017934080793266150563179780469061924379581127166864496871492510036969222744562594597034442287336741263139862648913843142873140862910464 / 6808780208545257801804892059923151615295685151386035789218366379782048440966319254408801893994745953169662188690487417403657509344083716320575 * s ^ 86 + 8027999996544422806823089389135088646510246162067545676204390872227548111300909543105176210132472177715397450366884623872304425136898976685344521410564450724105479987568394441011805153062898515369693538999565549568 / 296033922110663382687169219996658765882421093538523295183407233903567323520274750191687038869336780572594008203934235539289456928003639840025 * s ^ 87 + -350738796734853961911809055515073898329080644510221120534738887048395599087864803768073515910015280898148870478319026157199869467599687647583570668874194913458066636143730331705085048767216274222304330128170156032 / 32892658012295931409685468888517640653602343726502588353711914878174147057808305576854115429926308952510445355992692837698828547555959982225 * s ^ 88 + 8089698165538962349773564508312429125342170796736147137070763707102803600836406457961972815777541375410034151649397250399342197320741831251309641676208808078560124244314426125510737111731756461051224135986839552 / 2192843867486395427312364592567842710240156248433505890247460991878276470520553705123607695328420596834029690399512855846588569837063998815 * s ^ 89 + -75606885942676820654835124869233558546847444172182725884321702774002347797407391512261392690451977474345323892257967178159472143716370083444963907537403319472837302630597961332441126914791696394343946018357248 / 68383904391467632868368958188186363105202377809776690964058035089759141492324959619239325218142014454283670178778987188563053113421954225 * s ^ 90 + 3162362759816341632712931208690656346020256475745461154816091261774089814146836065874251285348223697642294210630517970274232730986840403871578671062155324398214981317026917066068444234083026039322544221192192 / 11245353166596899627242895346501757488411057684274389180756210214760392156515660026274911258094464599148870207176989004341479845318276917 * s ^ 91 + -158039534576994707563336243401879930720434154594000103893311878998097972740179894997367029400015475745037008598983055512004042505289860148230144561004352090298950522573487992846199841210855089644134629113856 / 2677465039665928482676879844405180354383585162922473614465764336847712418218014291970216966212967761702111954089759286747971391742446885 * s ^ 92 + 29235436674509508975307669388940048134451547660168591457290868090536265120326495975336918540441209189504034631359978088502639406425254005986235340884345033644530436362471552168091983815375434514970968064 / 2978270344455982739351368013798865800204210414819214254133219507060859197127935808643177937945459134262638436139887971910980413506615 * s ^ 93 + -80265176336422968024027650681421790910058820704771105686079966324085245072121341243027332746965023053097423380865833501555111527696948264936679305084975521252521231090155410742460653717107655644807168 / 66183785432355171985585955862197017782315786995982538980738211268019093269509684636515065287676869650280854136441954931355120300147 * s ^ 94 + 70420935697003008862467085846253212305165589215432301693041361936117946286649845815049799715898157226702813128653319262137207725352838609040115664270373868659933961234445065725575482102235866857472 / 711653606799517978339633934002118470777589107483683214846647432989452615801179404693710379437385695164310259531633923993065809679 * s ^ 95 + -2846426162100540477504821406370358099097596818564993027077417967281494233146639620639655387504859468567430806465702543982189965316310808246859421143193791148489260371756378664313018408226839855104 / 711653606799517978339633934002118470777589107483683214846647432989452615801179404693710379437385695164310259531633923993065809679 * s ^ 96

theorem G67CenteredEvaluation.density3_eq (s : ℝ) : G67Centered.densityPolynomial G67Centered.rectangleEarly s = D3 s

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

Equations

• G67CenteredEvaluation.H3 s = ⋯ + 4232126120062214106508753668979604662873627055998358150323747448372922520533739295696029863876399257649556649566230977589668908739581417064473197062757186517425073562301880269727664113382769661960886546295733843678031954271602958183064789454462756191686126612792696805307128514550986827672476698842727988391514487684656095341828641217895222902997203177121965703237419626084110792482416672788774483812462662261395452697848992555337752135216855508241247637655790488675268001337859616913658821071894052945360343351771329788396050950091291985627792070556742322910823560807936663479943087108772068320062612922744702876635698150510048331279200386285568 / 188152503172253043539967705903413353116800382810959152770422571139626182403206410647190013288960720634615458942650781943521247804232489619348679794205918573018134640619910516060710308863423052110150047654447116941981125284109942792998214098146055160791307115526296951706062973305590571207725991390328079340401294375555378257135108096156155855110978308603962780130068237863965049552362200654952279115593085676217745418846112022333897171270919303448148649551052981945457598805430348546494088567046058787290345691252518211993688729262911648024039820335278318477654490806348524222341875 * s ^ 48 + -12140914089621779791688767500705756500790602132153334965737237812185153061067247134781795957750216781761260743048711715925293996223148970036751581391017243154888430718950209413620190440618534182302195590414037428264761884498642078318353868770686097401510641400501332005549973491977464011232965426915926485682267673185129941755797135440978982983937150435211559874570647471268432574087094097324411053665456382683656976744427213831200640461112583299323679253439908736095975759314207571906273286439793486233795777949975577909638011065087520236796073489573682212445554161696061947837468026106498655054838132394662102303660559059743271048808021098496 / 144861492678440215102113901016516465088776529346210464482132345219538011269229320973029277012028431761160175766506786350012859394725597191207450621970140585759530124963585103005416342027212756721576163315959524497630727088784889612751222221128138378587661836153271792916447680200482686734408228465421424735388103977740089848110741052524462317580519440486597814940509087155665964899179984705995595403512289618829592717312601870991291779782831752162336603127966719758828879903391995261321702809316440457763212228919257904865605104970895170509754588653412429860509301897679618893125 * s ^ 49 + 108348840027689994163428901423899699191062611023907041719803140010341527428171815576696377862173701750212573741222617190120357373323372951660039201756889905527955789807968857051862114877862293960226917634666459370960214211234518868410213213445212089392081724704515285552645260358636644839676977265256600833353387499656557427890403292665916107056746842172361560139418150007816593410726166689493699802993344211029249045125194511977605846902435568928690446619059041427390842743006104974512658710614435715599096209943813014194188832038711063702676655454261213176920440446199577876147953010757376570042307703085233698328455496778959680880869453594624 / 361177576085059835497184254556004663631046602817371104167041561531193154781771218059439572065030456547367015051263550872673571267172984910692430796017196878241416079760960162479811634434425336839509302068093154070912190180932676258207225214403040431788644739735246383956102706699316671777163372858530506415725057087357366871974219605350748365935257365094617193584827238865204899007389449738668263472368916165545480494647322724169662793259081861860273201868919719075247207306300796810572978702473604914908278468329686150945241838539293888737258745294896220002617531685589346296875 * s ^ 50 + -14339065333145543347054013312793973863191180911634857508381491533467505990978433352530972920699077496104311307402725546128266909397934195570520442807343194772742218546479149375911592045712000593105729045551087209013668427208591235716957534867611577226754668100907468927327051234544168312789226097576641188789609306706798554904669008863776879094762026254134175633811322599879681396568808074982345256032648972959369116794340044438094386910313869026189713911549747146704667690718988429361609929961206184821948426148201139926418460656854305644255524697406497593102819445170563196942827597478310238658609446264855707739464824306197909484908383830016 / 13901929343651359705929356213099047430327076787687491556618203500445925202921005374363334471937021346351485107633540448684039346887413004109670921205190219464386581183252051536958787438608069568916961815451132722729450339039672822014013951648720801525449722057734011759819802295596339819347420389271740246944888989777528838091083169715387295594489151411189039149302784288396565924058009008809118065728916773164392079416613931269926643363179754682923723241747098621009515149148181613086205217982002906158733737271557731092986666992833198736302034724558269600100750276200042763125 * s ^ 51 + 227753691982946113472199131286392398527199069413855356917523317035745007379395176089793936118971572848171053344623973089219084586583379650848985570761627812787670251324861880551300614811700864721714209097861407976985394000514410705119399751128004076243061003394974416121364672778242753735803130960188524656021997948117953772111189064958274505387601503898634317078393550018203950372184276670054681685527486304080629042197750490477039038318341377127052137467063908652090760172820653589033048020372480061804642917475166927253725072043981506812896620723722164929788553867588404093925988517130175713516012099420959330074328323817987614059068915712 / 66860925441164512089190392441837815980115426651845131422877042362485026873093995511181408855043017943976805919066232272620241032014934906927755077938391732533120812202100136877715218905625195854946542212676553975391363080841933661184676792983118912257064885960244969618075260763134449741589517225502265338617668097339206398514273476248625542999762844374938035124282721327841419538569780656499642935433192027797668158496478396784700837484771295182393045557792187226460857173113711050729066901134309204611002066048927304553764954090577722372151850321589901887277008357602869375 * s ^ 52 + -55568378454309694975900408370093987971420968474189751338376211326507601726091144628906657805022960016221255054773808592721312816812422835461482155727225701225168477229444208757311564084620674842238371012552783256291604769527706219917872825634078483220434519303216568933118887565266126391681801565570251624928725383164426739497636141564789851811209598224255502119447945794377687765168004751333820504544607610421513429569102395231061570949800183421976614658211737603674289380022556811449501872949269677700235200532199370318942508209028080593233792920640293992786501972918866823574394333686040991894424168613398793006660290297448477460715798528 / 5143148110858808622245414803218293536931955896295779340221310950960386682545691962398569911926385995690523532235864020970787771693456531302135005995260902502547754784776933605978093761971168911918964785590504151953181775449379512398821291767932224019774221996941920739851943135625726903199193632730943487585974469026092799885713344326817349461520218798072156548021747794449339964505367742807664841187168617522897550653575261291130833652674715014030234273676322094343142859470285465440697453933408400354692466619148254196443458006967517105550142332429992452867462181354066875 * s ^ 53 + 1626831260003180568060190746706781712669784630718396334896521368435636654080615834548414617497798488334264750496223759313495356942341570650830029860513542475573793741783733340611474458529526053874366474730410715992803547262756366437799218846165172552076149104064354970151757436155950508846828892683299027634884137898954500252464802189785364608606775089683815194918676307944877018168757817651631672336672174302209891461202591143672245734595380673415342335168084216464375968116136621867573998926896161792188527517703205254958723208717902784971229705588025162426540434991219357083564016867669313299819250080562498720557518195852168578899902464 / 49435741898607274047926735381592711106145535493053058805972016972563346539243034170438372239947462400727709281014000913567557791286339033519987597676057090626126514485217944948881641713500021581278764404038309755334961885771892785606327831162039889118513347781214617292987705468812611743103676783102696391890819033002671981813549411471722476134227806175844865360123599305849832339496236758920238772535974607731660330240844448152556962841657994082882280309455570148545694982448454099999583928872206055385082448813457765505152497752980762495497986107372657966330181166450625 * s ^ 54 + -1511136970124787117345027742436728735928663864503919816477159991928421537715824928680408669417326986265909779838380194036021449165275455790812869599290708399420343723921749165576776231986587260899284078531213406089614544429148626153861855384630152045883396325919613610775159526314749241961390857547028846037629502873842369663947326839929778198981769845763964828375247876416374125208283357564064397760890279333884582705905751370234304226789130555276161298332700641451181767046027649544635344918119953009553520933244555619239510054614158521998346608425252321804324544927792529469577950443230691991044320608846033554601477687073553233477632 / 15702859379520765532026788444696242648543782317849265868106224818170175509574688447505994612777924655589768528369862433634317321417425523638900831483405466814727944376220680054914440541738142932875536625385397927493476235871892759547146887479207130779020820716985775139123215001846328614161640551141190646048795830316584709298503720053275673760951593347260296474214979768073766704623669639451190766957618514621580690629834333318263440328333013811982174038960539403006700648767058668445328736697861017529090416369181680168080966187974322627373732960857841930731904315625 * s ^ 55 + 72502446890686008729960037915509156513113050690315709083139339526481142181634074958529688397787930024619313221612589903183931107763839001662806002597095940788554389770086504216345801680202217018525721243915508975926067271959458303747154471297069930880743819066101328710530125837775011951429788935134389387762899963375722398650927277799867276608239703609379699284174337642507194395118247556338692830131711067772780812948311478104132495886578514950282346628261386078630036630485037956922295787478530752089677116747521335355398962958747060337680814646156149319494806535126724334163694546235710552931683330640108533994775821888995171762176 / 268395154766503650602899602717338664581103493557024078100816717202908660208046839169358842438157646721512136888896649809066023029776196519466229528129238833459278960481463343890879449880984906954809394040993482889455642655302051606022266445260588028853408034452365080069364607134776315935726153704300039899169207310627529992449453150744112514893068299165159340402786557634113215595121545446779509224358851415285618907546557972365435051116901678917342375360701783358827069912333744166546129350884638923360701900205769006202493761703445691966210308099013058527493148125 * s ^ 56 + -170041907006002531949412235350846433006068544149480100962400183816820447395653724707320235323513286656155187122603667882874343234958628526067814155091069783384514901244777601552203335050739317744693367903517720920741546483249538706462707834427717225300871755754131262114593865222319034129426433075525581727811680793621949279122547687172264751625844807736007053584187522693661286377271334420473186573922880886820921170932717361418193077823788891885901329045122951818361892878838968854710609493792164780495456147099114276488136340573393874231351135996467935701109872219172974809781594179282678249050400754394719781719679554152505293144064 / 233670175174071911441338468133963311751203311102206946702328300961022903631264498791652038025673638520346146132381719375548047004360408290532593362764809011340558232440734932821439521055412735704591467049166832812113672716071597489879223886305040251535446887137773371596778350686072102553206327888110277324613622537284884602590763794313607391672401780674788320620215790069591829210847059782506149540344768213307964709265601684835675260136817364663885679896244409770623028522058758398367654394435952485836945320125238245292198072857716869285945901660326732895903738125 * s ^ 57 + 12656016542141346941146263859564453471051084672170630861594960686097087576717105050987705337186969137152255491562774728024671976707530139855431923044619076113838741543556595270481022747099553421853159556311609537061730147365732556583318185874079330096407442907991874225493647778197047174792177703749390057104502020919705850974349311671118147453619794245708425877877422432248447974412862752592744917158399288775451900593752444793335690967950338599138689210154456575256989133969298680560432584915100456890612681658113126758955226532516237521985543685725207735831354457336889932798964343486686277820366931607899262035062520670083964993536 / 6729329771646559515192468297800333704850939445843099756074995757566697324038401653384219565784047186782560315629662226306746140145433803798853234876047131409013097061351850101113948471307814633002137581356343745333958797185775895934952822942250414393771558815288408913909207715884896697162843603530484649864741860557360132547301042735943013265640170446443755012895986009948523383430550877549829529960276343779474653990767079305098890311785207125375059301877942287336710851181433955861630563494183338718243708325354428116657144104144775778840547316930958544172004375 * s ^ 58 + -2193472208914760552381670270064162765223832486046613278264313054172798570439364326637522090806446946519166542699865507750011034425239923033335007738784698889532335192504024918392988887763881080111408627943198913506950978119009526867666142256190693188509189167865769139596317872407126996453276009991463591844342977731377127703368359004859493554109222588714877352780947188055926983488890169761962442376340125605197846232793053389586250332767513211944192839334024113238874412784171142932104974777525839773415786363367168953179574581613814944604044627598020801385420284049884505090884973854862364727135368385156405374022025035695259648 / 470519483021886379323802346693188761711665294685840210577965437480146835991227555808773927850434615276336177117619746735471037147544058250029735092593715376667309850191640986765696854406321143840076080008277048320781463468755254849311656200595125281587889698430832572999756172560992666778786025586591572234629911808521850007395905871823067175633428326347403448110971476603184449187678433225655378937817151765840304173383507576916727436523645903058057293275641160959674643812911869568063306972228227088675309329431889836827320155229347937222574541632952507375625 * s ^ 59 + 1525289847184722456008706081890915627504332962239153888542939137145485114687781530444158936756359439837219354432749623140195443842793271052569226982819500264472766227299638045815565763526243466630829025166566392451763399383205648024538384374103864154294076815491623558014264134518713282168000570426449226878562545451871705146345353323279037476958184186869810844149890605108509799825492958306512000033113937057084899088588942862639297458278024243052963177709299411064414852003321785367305108342113827682764007985760695495973807331583284183373976844906238658880248360367560397382034922304713834758335187586700376137425699542109519872 / 137679989435569567342909864798294760782274942320928619340850136007142422427877586685330394622049143900814711244842362731997441314359710041182349731283418474464531024280572914259869722347868195271400579855316117433167585249092119663293944810855305287065212367785165271600504284583725068788803713914848509304344857468755194357776544250949186589608118618038974785744016277931536223539087229421642044044804187357129478195921301385634411769881399424783537711335852786145859385701571589592189934723245547741009884245740383498783817698124353489785307229163463877278125 * s ^ 60 + -88846572515956765068009981238310645405733313735513088616507813148269792081829165805840966598232971788920735365931094969869693474656516173987736110594264443796034012745616591723714649248356694094093176984963639445954081360679138474879304694204942705950071680681586974651505519572866765114809752664274717672724374052955263197063792592475563035948041816718265983182446147288144280798368678129662872001439647756628651128858347371443948378949726502343978058159185250671856232986617273292626392901042747143323378679641887407903825464463234428553518441348539579195920790743610140389168613340998096582572519385248845611756554894406844416 / 3521374991853141973969602412031857613299275254329830515635999285717269504444667835557716592010481248616225319050475524801611706572722143610953179709974225133055091187050292565975703590448620507989700365272236127221477023142398029124079930172819128935420525968509468162528621115139299453298543626333651600656199708844472476236632787969769552187042027547328076281083854487976398170182105238876379323577801018358447870000502886592745961409964513589851488633747178178154055567210007113259365206758062227338198297270508760346252779700455162631825467915711235435625 * s ^ 61 + 327972792525867158001205150555530963313392367035909893577873359845968095864304493642958089961935867748674017779227168593979567379052416264379280825180939219136903251510213215407914319622710980593499518519664006746469157711246165745818393219923820253711711773312980024675371952377581358834846885706240999936953522713430987258907519284490922389571519637321384200604963564621997094264568690128297979485578928745776774572182358115352406099500647563244359650543792981673642845696213033466842140340209782891646295831543648361060445449187321841580245203688478010047078318907120551736078475864235224140594848402445441035417643953160192 / 5958550139960011709742781687359450483739971955617151033535560371385274356604758077670851022670161680488145315254348061471768867219722336853744395353570767223560770007745077575658019939806803137552849001479557501348180767312148918479275004204293571641602389240941404616276300717016700008310703175870701021834147357626970766361726483892006483750203026908198742638248912272007514962008256531276783120626180286154466838486322455070420378288726547258168309218145367998550375134195714443571277164325608834308917989959376916580875684797262242767776578231130163125 * s ^ 62 + -21263865431049853293215179502302344211023745344854344789874170544935275127510691050473559388467621955366779263408929708491666396176193510067007348543697154875084678500287306910060903677117021741938102173247328369942417208135494552364059017509987559765929709294300079397697677246798245494564891919113153382516138408729844428554040369445713037949404481290399381109750538809376082352279484926481813138841582328470319145729512407651529422970723165425503687708590172117664489932469349986730739199338019566025131156008596058256144008662961362914813245284064547691245301834780993273722241608321559867132723491099693131191840919257088 / 184958038428460497380938445560153362550662550052632198849856104041782709791139782082296653777345249972547420010938375614765801721366913682009107828990936779307120675833839900400827155770022495444428057866985655854386621505124525162777252108593409710116690110339629723329331306492910347184324931204750914250481749993290023788465033888309391765831013008105986533506204824024578979344139429759656688467398170781422890299940623985752549782547202623351542160758012031604424304226403795874701847462328697839169091593382971847610870313244293597782474430789798125 * s ^ 63 + 267287284927708906415981318432052457641227685728176940669813245198445265672961127701602114046222855703266366096279332333633633388089891490342982705869595211138322069054275103458476082928292058753763248544331967253914051033092312964136251041699026840239419686698019481606870332920498242484722531141982752254639312226870960814025578004034242335221679385006459652799594253424834088497473836425091830005918159900563626948244207624539268129683009442936186613385919746705309990133804421601961292361425989941338843810464694153674359658475177089007318008134985662169144699415856222195728390642893428021652168855624652558423096819712 / 1163258103323650926924141167044989701576494025488252822955069836740771759692703031964129897970724842594637861704014940973369822146961721270497533515666269052246041986376351574847969533144795568832880867087960099713123405692607076495454415777317042201991761700249243542951769223225851240152986988709125246858375786121320904329968766593140828715918320805698028512617640402670308046189556162010419424323258935732219435848683169721714149575768569958185799753195044223927196881927067898583030487184457219114271016310584728601326228385184236464040719690501875 * s ^ 64 + -14269834720641573262410032938185107574937273642324364028925608699399277527735924686650829850978884177526630008345404061650959681680357890088646637728153757494310655983107840879264220794315920223892681167485195514263537050053595824652288 / 32492847478206293480416657737148666480112984717822392128092160509913429897226218704959745721261836500656363464496307397536221729762170326921116174608202475784634375 * s ^ 65 + 1814455842858168431993040136174419023769304955351935509648874950973227032989703108418943065093258004796386969563229996440589540009544178484349680206666932755861683650735038534891307750922260465167195027014753513588908941293465370624 / 2261945525806216044581737399035758195622205688675418874214560425333340055497822395054629009485683014316488928959018962585187729186367582799938473693574832981875 * s ^ 66 + -918884443045053104585760024417472265296977563074416266309480283479847909345243658434120587781178977143570359433030735355182903185881261781308026468079457360928064625220992548576536487942320592853834431592923479683555031629893365399552 / 656718184325738058276897758186715129462313718278763279813627376821779729446201102030860622420676635156553952374435172137232837373775388206248803529034559842404375 * s ^ 67 + 43116608951775573503815426342806421470770619963914060235083296111037011723787912494261250995666014649887490126675303754533623180943648321911879961731423804162398367790877237732639983813138336620532771268091272019720590573324034113536 / 18514443007524953550094961673588983749352128044343243377830290888839561195000694418780481892456886894960890862960858915975055116673601325880977877269631040333125 * s ^ 68 + -92560775814147168559239812533191323062517127121977003910207250549605922470735975170411064812244512593790458419119488246212264692407443248689956039241027277876462124998200323475082518315609860018118919242726676150958477938830662959104 / 25048952304298466567775536381914507425594055589405564570005687673135876910883292448938299030971082269652969991064691474554486334323107676191911245717736113391875 * s ^ 69 + 287266191808107464679364766646123141911235745037420809776530216417394405505686978270597634296254010995067898389503142926648053575551691226189521673037975346295789071086633656689594403085416918503958624707734435481382742028565086208 / 51441256272396076387498901212639075274059258676828889277134252687892723809242224708844714315788762508822035421420184334296017232958327094215624807846081321875 * s ^ 70 + -134475011576144872811407565409138886997640892549754469344122157616683501359808422056918779816782360462098899876007848415961704291129707389935335345351337114165080895756783152748877713160204816492393315703055140259520259638358441984 / 16747894017432655557552552317201363837021762172385560776999970099091705141421719014555086883059269063718779080765724917303429949213592912861030581178812366875 * s ^ 71 + 2587983122539927633489880077213216282627155791816524749477755867123629348168900770737637820544938493259219515182642447738541854725904559117503570739194242652065032680249482333325670918804168313706736835644983310318508296661630976 / 235885831231445852923275384749314983620024819329374095450703804212559227343967873444437843423369986812940550433320069257794788017092857927620149030687498125 * s ^ 72 + -10652522204788861219795614125222412151440593425757205469257014509870472532017501443584972402078729289206826775945660761617782839457248505147426641083467089801098671017018557714212732634462697749739089470069694291854398473919004672 / 748681116517197707104308829856521469750513557001926476865277291631166243309115424410607068256783001623680877462276741557348675010772983857229168662616841875 * s ^ 73 + 16959925540797178062871647343239325344707190679089411742947187511124193197403176028105207157733494818813020127262120438027596104630081330730700184237377303602801502935304316201044519019583530735062300220803110153845101150880137216 / 969752861729277395351243248413850488215657590576315725741782306207187934636312368604911134073854390230977818448093618059823017403603971480216168237270825625 * s ^ 74 + -13329481235635277786236177181237096548859864891007603578121818762984613223131232389768639458131270925403563929403935912130560618609548223327934164315829450174727362633967050444915682580152435626830019454248415623591404633969393664 / 655238420087349591453542735414763843388957831470483598474177233923775631511021870678994009509361074480390417870333525716096633380813494243389302863020828125 * s ^ 75 + 530109656540520967941581792593630773418841447959096937527778678434977388428280908392929968544060737805640560869360955760072361179466653468564381044429231208659830914843476630657008722063158330409984226291018514857111634025906176 / 23713390441256461404985356138820024808362283424646073087636890370574737140398886748382640344148305552623653218164451406868259112829440744046470008375991875 * s ^ 76 + -157404137316156965115468147385967386983071775705348181291584117536592950011935912668406870132595103523665277294447006375217136795766153931826325015766952206471526339136166743723432070311192846141716656158962196424802486645161984 / 6795065097202143911370072811708662079589192326360570650843319462913228771225411992226604543060040772389233963099755081500261383208436236598111288949845625 * s ^ 77 + 953298059197726288127945420692278330772764998206705703531321934736993146926218232751230039218666767650362820979287749651739383411740246835806904459114111472940723358203241582818324006061270285853898342672916633938412057919488 / 42205373274547477710373123054091068817324175940127768017660369334864774976555353988985121385466091753970397286333882493790443373965442463342306142545625 * s ^ 78 + -22980197625882964171397677185072973587628961928859168848500412762588029751051794894665373790893182442208525127211296955669610649660455731367076757634826564213337338027682087705417190575924849331447018108178310964542531849682944 / 1111408162896416913039825573757731478856203299756697891131723059151439074382624321709941529817273749521220461873458905669815008847756651534680728420368125 * s ^ 79 + 615665935878354877603980140707316467104244179231243545830099610393948988271687547405711637755254873096055084650858436517762819619091275819580546158281107351433253648727458550096760424852425115942379108928475297193528393728 / 34736932736253068074381171237935036063641297070064006598897423320876358005395353077354009370753984982691685009328298348798718826309006142668564726375 * s ^ 80 + -199554691011053094440981113183265754845627080369240940672512161553446155781731891015743620705080124165209152225946343671525902741721464053012429869181870054045389694928667543817743934493592885838727837061283454939953379672064 / 14068457758182492570124374351363689605774725313375922672553456444954924992185117996328373795155363917990132428777960831263481124655147487780768714181875 * s ^ 81 + 2655111432786671333651304743331852249593584756141233546083359259293595224937752710976858880127053553918938713670081180995405223481939584392501564163801844698153633159796100195085336822839539598484824143595586417063081541632 / 251331925091713374891110827192118202107522325859874871274375474615752472627272260500855479564867067815945720949845923347190730331529867973425497726125 * s ^ 82 + -412368480381295495859156354646369708538790086377753610329496380110116013210222914921602680267731239749326408660035345833042669495499137552753422820593985960965061047222320506792319909008220114450878392306271865582364131328 / 56532655237431463728894847308796235162396620721868873484480120306524268910741456969027113289658446148302154034789191430397914952620539408656683770375 * s ^ 83 + 6903742580358473785657530405440230070096773975762764492941095384766340106573415083323660095597389685391222831139891452989261663361369610165177192651306303883031853081100885671312678709696214972024504731367270527270912 / 1484837837786600451393605306914010371489482108013800881725697591283239025395347314326842566882700367479691715764425525256874541460805948905294625 * s ^ 84 + -42539673991601754306817351230231574119753564929418405316747031440467611134179328808344961654026202466254576696416459364637345271226351245671738958640950982109507072784479667011335783945146363734282364266352240825991168 / 15626150578611366655142227277523632957103597422430952136256150841599801172017702688868200346717941962524374723044668622941393983944672128955719625 * s ^ 85 + 6393165075141455654498284514425320769276781949467540199240245701701337729731738530748215194882719439664367498249680751176853352559499867968861446817631381901501786463694556734268485783209933967986856744932819744063488 / 4391663234511691282164155378650432791865716922643993084045846314959421244423275919093677221626611139794432111705364384225359093526933997026770875 * s ^ 86 + -418281597627085281142464385299697337774341406940527318220426896012976036818604573017934080793266150563179780469061924379581127166864496871492510036969222744562594597034442287336741263139862648913843142873140862910464 / 592363878143437428757025609213314190530724608170585113661997875041038214364069775133565764777542897925760610416072405314118203312935283319890025 * s ^ 87 + 91227272688004804622989652149262370983070979114403928138686259911676683082964881171649729660596274746765880117805507089458004831101124735060733197847323303683016818040549936829679604012078392220110153852267790336 / 296033922110663382687169219996658765882421093538523295183407233903567323520274750191687038869336780572594008203934235539289456928003639840025 * s ^ 88 + -350738796734853961911809055515073898329080644510221120534738887048395599087864803768073515910015280898148870478319026157199869467599687647583570668874194913458066636143730331705085048767216274222304330128170156032 / 2927446563094337895462006731078070018170608591658730363480360424157499088144939196340016273263441496773429636683349662555195740732480438418025 * s ^ 89 + 4044849082769481174886782254156214562671085398368073568535381853551401800418203228980986407888770687705017075824698625199671098660370915625654820838104404039280062122157213062755368555865878230525612067993419776 / 98677974036887794229056406665552921960807031179507765061135744634522441173424916730562346289778926857531336067978078513096485642667879946675 * s ^ 90 + -75606885942676820654835124869233558546847444172182725884321702774002347797407391512261392690451977474345323892257967178159472143716370083444963907537403319472837302630597961332441126914791696394343946018357248 / 6222935299623554591021575195124959042573416380689678877729281193168081875801571325350778594850923315339813986268887834159237833321397834475 * s ^ 91 + 790590689954085408178232802172664086505064118936365288704022815443522453536709016468562821337055924410573552657629492568558182746710100967894667765538831099553745329256729266517111058520756509830636055298048 / 258643122831728691426586592969540422233454326738310951157392834939489019599860180604322958936172685780424014765070747099854036442320369091 * s ^ 92 + -158039534576994707563336243401879930720434154594000103893311878998097972740179894997367029400015475745037008598983055512004042505289860148230144561004352090298950522573487992846199841210855089644134629113856 / 249004248688931348888949825529681772957673420151790046145316083326837254894275329153230177857806001838296411730347613667561339432047560305 * s ^ 93 + 14617718337254754487653834694470024067225773830084295728645434045268132560163247987668459270220604594752017315679989044251319703212627002993117670442172516822265218181235776084045991907687717257485484032 / 139978706189431188749514296648546692609597889496503069944261316831860382265012983006229363083436579310344006498574734679816079434810905 * s ^ 94 + -80265176336422968024027650681421790910058820704771105686079966324085245072121341243027332746965023053097423380865833501555111527696948264936679305084975521252521231090155410742460653717107655644807168 / 6287459616073741338630665806908716689319999764618341203170130070461813860603420040468931202329302616776681142961985718478736428513965 * s ^ 95 + 2200654240531344026952096432695412884536424662982259427907542560503685821457807681720306241121817413334462910270416226941787741417276206532503614508449183395622936288576408303924233815694870839296 / 2134960820398553935018901802006355412332767322451049644539942298968357847403538214081131138312157085492930778594901771979197429037 * s ^ 96 + -2846426162100540477504821406370358099097596818564993027077417967281494233146639620639655387504859468567430806465702543982189965316310808246859421143193791148489260371756378664313018408226839855104 / 69030399859553243898944491598205491665426143425917271840124800999976903732714402255289906805426412430938095174568490627327383538863 * s ^ 97

theorem G67CenteredEvaluation.primitive3_deriv (s : ℝ) : HasDerivAt H3 (D3 s) s

theorem G67CenteredEvaluation.integral3_eq : ∫ (s : ℝ) in G67Centered.a + G67Centered.b..2 * G67Centered.b, G67Centered.densityPolynomial G67Centered.rectangleEarly s = H3 (2 * G67Centered.b) - H3 (G67Centered.a + G67Centered.b)

theorem G67CenteredEvaluation.endpoint3_eq : H3 (2 * G67Centered.b) - H3 (G67Centered.a + G67Centered.b) = 18714380929485958043390106760213859805550025685232164283038465764768172870393209482659913138861424503487552745542794367203661606100227215797909917255607000566335492595303150985924537641774908943966814249726211345857002109002224830307564523545325837001849752244738460487436721695401130900764067164125303766596935545619619190678622143885506885991662185121233005259728711941304683039430434506794513886985281452309425825255085079854001270019264561959060179413117298018422973160804965515194671423382461451122765218781701043069895176298716430765879455697232879217725046254487690837405989025262620979051488689837654410866021030645482745208634903209298040764785404245666154597624731401746492859437131251372188512947982741641017103437973162053610459804776456554947594435318963820472512522373323875800 / 61940729646895325051912178183013348488403788467844115164839436877078925812989984860236205529862904209800211506836519334650241191635898618470789830005568921710162231011318407164029582200969651961917045969820439334234053758412056631079906909662877269367799617365872720624092499600047478496106548884313227210944125916922504457431821482105954871213558867445443468772819239728256855909404976501740856245371699463042405824106008048586922063638405297923737444853733247978663558531860398477674153171638628232488169507583370222545361968297560606647359940487810250549603266760074304807451305222041488409536301005742447701166617285821045394348577999378978809839323576936013290233009519419026318890445783868340216063803844078211633483691306264575255116153044652404382364147822956758464571365265318443251