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

Equations

• G67CenteredEvaluation.W5 s = 246235584506879001131798773349423118377943429044615434105492878301626816087181290333248649919204133859266109539912581300122979729133820684410075946875904558005237634139780703016605800640122451742320203055391659274794383944829288297082256469741529837095601925778549200774299718312391980272264334065153374024669495763258681046646149458718226135968800101523044346536783890734965191244046846219888593853416826373797132565043257033384416687663 / 150738821302424875938299854459851208357518582519452669814387919476640887565130633759716251610540227116044361814468839780401928391406274130469158851088603577546718573800338028553560861298276842900453713882896065283054695746565509750637656290416115229344326983762223712522540409508949546260070266009702995055389984283608157346063643731953453653488471711734327517143554322818709570038954776232853036799040152008240723216580158800 * s ^ 0 + -3074663444215706974508848195968826842678097620413441765584826698976241699625951801247128350627990493820252 / 26016531848676609019733212304201985278528371719929018837564202498970513101376639717306762443 * s ^ 1 + 35967180828296149344323513641390039664685329386666453803714704251909854644423241842609516692598292990147328 / 8672177282892203006577737434733995092842790573309672945854734166323504367125546572435587481 * s ^ 2 + -815546426574192556220496093001198472481400836649279172724890029042589640217101792772514216472543804092645504 / 8672177282892203006577737434733995092842790573309672945854734166323504367125546572435587481 * s ^ 3 + 1491942577771815302637226475474131048548295994164088448694722258636347377082636348777059643718039523517320384 / 963575253654689222953081937192666121426976730367741438428303796258167151902838508048398609 * s ^ 4 + -1092169734241263419739860795638678551247126368265556906729409726573043261563597743410093082685319536137767424 / 55377888141074093273165628574291156403849237377456404507373781394147537465680374025770035 * s ^ 5 + 319930241986581213774664390939141440322200069952762357354415968223533951788670188639717462643815970909003264 / 1582225375459259807804732244979747325824263925070182985924965182689929641876582115022001 * s ^ 6 + -234380139912702487222186069122940744335232613365037974449618899631365703395032782606455120067500496011764736 / 136735526274257020427569453269854707169998116981373838289811805911475401149828084014247 * s ^ 7 + 558243858442364256403417272009275261640843821392872370540583452465394356659683112727830252078611464154442496 / 45578508758085673475856484423284902389999372327124612763270601970491800383276028004749 * s ^ 8 + -10231344284013639072556910925529391533409568905889007101053998426296555194805532987329345334898675021790973952 / 136735526274257020427569453269854707169998116981373838289811805911475401149828084014247 * s ^ 9 + 30012760324976942776299569258839276677098709079488484348182332288570576357451994208182043111307718129305223168 / 75964181263476122459760807372141503983332287211874354605451003284153000638793380007915 * s ^ 10 + -9207155639093585388769259571634921381982740295942177209660253336684999126928740472447624233232243677452926976 / 5064278750898408163984053824809433598888819147458290307030066885610200042586225333861 * s ^ 11 + 37160516921055035883909063845425498994275556231252659119984241644087359535826506545344290617064647334736707584 / 5064278750898408163984053824809433598888819147458290307030066885610200042586225333861 * s ^ 12 + -27278118302108599123743935635213114336479652073874118039515172139155210882160704606479600758079071805487710208 / 1045009900979036605266550789246391060088169030427901174466521738300517469105094116511 * s ^ 13 + 15407968201235190146628445465198101743123479883871370908396504941275974681274418327729125193822858892921995264 / 187565879662904006073483474992941985144030338794751492852965440207785186762452790143 * s ^ 14 + -215041025773123181444254404881442727379535489489091662082339339650856672565666480585031849061008436660814872576 / 937829398314520030367417374964709925720151693973757464264827201038925933812263950715 * s ^ 15 + 3950423428165401886191990552136690103600670900453499500225591590524283175453984934602250112263956221315366912 / 6946884431959407632351239814553406857186308844250055290850571859547599509720473709 * s ^ 16 + -49369074392236903535043131534638891394874387485866821919799071497590534447220144111032432933175599589180833792 / 39365678447769976583323692282469305524055750117416979981486573870769730555082684351 * s ^ 17 + 17087197463640755652128946505730494497694273298646615956981354203436880069823620216286247577159080568753750016 / 6946884431959407632351239814553406857186308844250055290850571859547599509720473709 * s ^ 18 + -62875046811302363105995882272450403960692253049239082062232402683902859547018263545159614644387981128405876736 / 14665644911914305001630395164057192254059985337861227836240096147933821187187666719 * s ^ 19 + 1218630493413220670833616803835666944797024361239357048912514960085306623457789069096539658302356954516815872 / 183780011427497556411408460702471080877944678419313632033083911628243373273028405 * s ^ 20 + -2336035923888344635228342716375281033503234884159482154801587914964972975844193596767129075366799355326496768 / 257292015998496578975971844983459513229122549787039084846317476279540722582239767 * s ^ 21 + 313605482429407595595812437291784035216539822973557050234542076494752916656713062575234698297033405379903488 / 28588001777610730997330204998162168136569172198559898316257497364393413620248863 * s ^ 22 + -2552338484733477487366956032685112610486272223217768518567820771608658327225330936149123357270544262287589376 / 219174680295015604312864904985909955713696986855625887091307479793682837755241283 * s ^ 23 + 102935637388729056450066069700458884339619830379715774792780171618291928487826169668486531584810876940582912 / 9529333925870243665776734999387389378856390732853299438752499121464471206749621 * s ^ 24 + -76711883912205459666434409139143570577588098124360332082252800578938029766768655971889045451800519578222592 / 8823457338768744134978458332766101276718880308197499480326388075430065932175575 * s ^ 25 + 9203440005068460738543423491722422334569409238440508098953363669924090060705521664381616613838250175365120 / 1529399272053248983396266111012790887964605920087566576589907266407878094910433 * s ^ 26 + -535550447540094216331598554824923805249663811638192774213153589000573088800463775501663839771974323666944 / 151259268664607042313916428561704593315180805283385705377023795578801130265867 * s ^ 27 + 205101425687617688376806696511764227077652861554273238440691536838575901921777258529135124862520558354432 / 117646097850249921799712777770214683689585070775966659737685174339067545762341 * s ^ 28 + -799100401446176636908112261112737139735829063710312870686223861358328702813911006116899698578838784049152 / 1137245612552415910730556851778741942332655684167677710797623351944319609035963 * s ^ 29 + 1274294614177071689939448687742584871034489205612954140117317119798338859527452832398904785987144100347904 / 5686228062762079553652784258893709711663278420838388553988116759721598045179815 * s ^ 30 + -209260711748492102617417121741514082006697954667728464587087960011762879200332773010235664901102343553024 / 3917179332124988136960806933904555579145814023244223226080702656697100875568317 * s ^ 31 + 358905149089718679110072776253678489950752455179123159725686047253888876261530863826185666985008824320 / 42120207872311700397428031547360812678987247561765841140652716738678504038369 * s ^ 32 + -28886137518384761170752565121662769911328801233066455280330456098830017043044553092856134355514294272 / 42120207872311700397428031547360812678987247561765841140652716738678504038369 * s ^ 33

theorem G67CenteredEvaluation.weight5_eq (s : ℝ) : G67Centered.rectangleLate s = W5 s

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

Equations

• G67CenteredEvaluation.D5 s = ⋯ + -54698495376672828671378681077454840622938024744704489273445955813078676946816684296068867862478395071240564108165975722551202346097080897588928673611136765121878163018107534105506396834594114789876487825488304276812916529080953064105625820412461284003589739677350835694750792308329802217671081834056452270506233318059584566854951798039050513451602263973049771959964218632209830687380508925667304895954782545674351454824482414748427449999912373488918738429245140724508684960361617561098521501733514780686962588532101003057003739161510433407353614295567656762239608614201810824686476108264101782721860080725880099303366083106492645376 / 24826600384759624508612852189582895058631250155735392803005842479643332316713938198363250560965413375775333513092775843514730911280896196944139681209663146952202465545290602054836347136948054593332215597924263856743063589210251197403746823631532180585154485668618895450572387234270828321490175459524168654843361028957526694358734311610229599212400472180873354596600969829626000944035399001109562871356653858931828093275785974820761779962763521308360013516760607600832784069430802953104963558507463735901858748594777435300665058731889474873122761313650729733733125 * s ^ 47 + 8105389767314047681817228573931863655962308689210393728530097192557423567213102009497200791135075608448084428844009051492035008957823884184714124443646848550314068158308252961801866004269062843146643644538357364379161666879171212283046890939507344961137856490219360428457072708858411970244992083598821803496798896406107544995935424381234454358970335649898423644642550597170519336833600103223720676345433994077753765380829633552554047618966084926242096146856845944751329602843551360346638697055352280299930551063038033392007982564897496348264069450928939762055677843653231844252347611659930113693096788638539030102333655058583912448 / 1110856625733169636647134130798195783549158673642892651420621226423328069814424164491592381278210033642070767701564736282877503507498800458596575278441932253959891162581756360102196764200811284947670854345412847402151001768085549230984864930822799442000259412351305012096457870745868093604146342146089303448928538622401340296425703043124607495326150416119388149057498655967872366517386246115370429344646834312699825622066820238828483282135440697039269606142307229082718763492314309762046268589218370735833794557215650100084309934364514885574424278505321244326875 * s ^ 48 + -278750903912093315503241191155695535054625435584715495922924761029224666383878122520586032066515439919540478989776314313325111942894116134593128165791807019115214226202981279808235951719005057355320250461679293108678134865435547164719093357242698323828080826776512130843385753036006788102397201138619648971317424920800843281505337582900269074388559708965501003015269469040594025021548205120882105973616910040340645202483390126529454681502622982027677015660017628515457079997708034967095497115725316485746733332816079521901465662169812352920584484270648900313790469013948563957776090619222397258541124539489184491892997883231731712 / 12025480826170640692292867217576015973618323930664576940784848309776313093745952178392201611316891069031799844954987075002606727135862607281992469622853215413115601519147400941168512079714026456951767578629179216139609331308126943957548327231858922032689973566200533951006433141388157617757464705852445629944037891992464617787515010251217947492763135845286737646377673942429253346822537525393479938540325601939901765438346256693425939496611436078285066533571098677072073380891698704022042834376272736704417714895863068465010560768420164680639516000666576623125 * s ^ 49 + 1083999430580460597237715422739327514368313843770612656213139784800103028603025186284051745060047231662872617767769826758910255936462942970409528827558377083782332325898615649603508434557760495493695902810622836762118141430894562099736717561969594987418698084917951356791658113603724382981203532027078498131754910485643239982542226126271346156150016737706644174937861289038647707096048330309295611051135685054599532674176631098025369490153737239860378661136096892705144511815948680884959971149447416934719690434299208321951741078190653471985215988170112410007021636309757035397769095105477295194061382053098639330611182652476096512 / 15345908113654480736184132901214124387870967445804358884857977157390573496989197142513380151027031262966028978398609829260114337021512659913927804079232382117151202490840194574256918544430278584964220660625271038359473849846956288814671657346500133822664195443660414471302733134408357604252853027762923024314227829956329675621159283675392254209586827288992233545055356577246350451329450785971523179738758810022709431919251803870625922790659692703674408420429202315472093642527694664635584344098207224519719430927854711851575832954822419079343478080924259998125 * s ^ 50 + -188543160843250220068032135501472680097326618404411592901377713845608612678446103037984814974866802937083707083290510509811902876520500975950547184846747641681974465943329069704289105659029019111550670862848729694984862254960847464003829784935756154166582946139976297678900582090586309737620370862980300405755002984244381044345261145330524891384248152381556640970804061181213021457952194539915138843225376728355190537796869253262176781796885579499591799297502357505247744552428761749591821599731328127707650961299023362874573301448599132464153417615374193015313480715408064745596988654405516977247965891454623788899440470735716352 / 913181760028786226681494120391551668944426219561652705775293270613952849603130744329533506810026533790431332531702471697626542551352712708956516643321520561397967056784394742444896459102527462965940561807889858596137050571444423572426034762273592868982920193309255432980278749652746969193566000200696435409119508023526149057282337635255562296942031812552513171766719331882583989121200990166665385151363006111656149069215274250646825594219226996880480036629313925884406152893520292090071056760560952402479675860728654841675775255657067027943516112217553933125 * s ^ 51 + 129641709898718867428974642259687215630967490367372356819332339355427072026169313546417522093331314143288832166208760520741068060483078308944157141469491508279184947809917839381317773292154959380648481350852914232688914662825148656198419881825114917388821862101749087896465400000058127819192499904224546407830286766543510926636346092253760998946993591506360019529916558782633498254342690837874288730588271729908371396073200165060317518371633852153396709442703114376188848255324935835449499653545350173326162654919031758843586816688001207387485027534207061246453882363509271160940901666201608050326897271940520124378012525826932736 / 223987978874985300884140067265852296156180016118895946699600236188328057449824522194036520538308395080671836281360983623946133078633684249366692761569429571663652296947115691543087810723261453180325043462312606825467578442052405781915819847350126552769395519113590955259313655575202086783327509483189691704123652911430942221597554514307968110570687048361937193074855685178747016199539865512578302018258850555689244111316954061479410051412263225649929065588322283707495848822938939569262712035609290211928977097914575715882737326859280591759730367147701908125 * s ^ 52 + -6575436887962246697303819843176592640292469081387875160383559068324197732306020263459112771063995559129272153916168377820691789474892483355047872105950171146512721834805881153393992519243742287314932849656265105669428157244106378208598897417444478582548631276156471405471987763885686485195093633640467836702290595916011392860535191620981126725833746284923005152373577676670465141084324195679199941552881239844904208131779778701824692718050792895668526306755508314732048634961410149837664889039982454050041795458654963422096070729569016765710001222389082681069465339816439198470564442325247066173212305227841460077580997976129536 / 4226188280660100016681888061619854644456226719224451824520759173364680329241972116868613595062422548691921439270961955168794963747805363195597976633385463616295326357492748897039392655155876475100472518156841638216369404567026524187090940516040123637158406021011150099232333124060416731760896405343201730266484017196810230596180273854867322840956359403055418737261428022240509739613959726652420792797336802937532907760697246443007736819099306144338284256383439315235770732508281878665334189351118683243942964111595768224202591072816614938862837115994375625 * s ^ 53 + 1254204455116215349534706792471483098656857318181025303080227068950667996417023301384216083842060083963167047655125330617227596152505420592716948781308005818315676582869905794421355596810895345197236539247781036760932502132778203319149538827124435810480769417345727584976668606288914810375311051267746516789164296391625935007375276193861373703099175802384230285034878414907583122522243672002785410792210314690732683849491468057285788169963635182655613643607195599297299875032359781811542276639962262551393405282207394279236229732567633523170773793063921218988006113141720340250895006331925720447044595257125094640909811712 / 312768542174995899383148747795220970785287650183782321055168563955666429614706609525325211511769079395926348234047457971012618438253675010632840864474566975577486016700973875890252931974975522111881967784265456151143023701117496354742982874949008908855596107323464425512659873151616694269707733212415494294484441286894940324347122820782160557155857210947907614483944759383619558043100465842469277765340706250935389217092716232549387202941351713007778254198999948656422243624907454214148851903523172758876999600701009053543025781149527485132709944375 * s ^ 54 + -317129476561953279036815510676718417782098578812781550995575979269206388603649272926054016679648335338638883381456788054024355088482747856493814974499971315737150162158152743034633279286427954301614702448996046485099642616476203564542335451467692746182280585259079218383837900735701639255627953752592028460264735053644409090938516775255913777700333277339014356202212205548807431729512181616344670672409616558551001505033267113558950173221504471794282976027011122184468786962350338242294995732159227396447202701538514693372177933445566767187966353479166686702331444736751392654843344176770863251066397365907316026744300896256 / 32011000209509706768380419030167884720512537355040044723425154506144234938169653142775225491485745276898127138990645229761442807297253987529430301033800653039965205740611476008266685768054630443941377776272631573410461848064553329246350564038388187188280875461178356038207987426890895766350532902170089531873113148442394360044691257242051179271462998137108070088253016688308171603538472286286637879743202343057898303785683149474013897723118745554473722430057181818590478420489474399652592270673433289986918674106752370603626573194190519370585709429375 * s ^ 55 + 221944669927031960784593940321340532390991814145591164124078105936500804334221323264769042289447182296783162750080099382345271309055573490985054977885039642838029025922143648204932265002695361511117267557269504708856653534781549897198103356041377647266968377069158539903836252831500400946445167680624620070948398087082751150146357776636161831108143551762935717537517297021767774522714637105623579792633858698238747783965143892604608110714262327595933735972030546957360900497199472451436042520188277001453642849598243797455091897004238874276219688989597114459570354777587513577494134714676639168441147372352382508151989075968 / 9462371131112932189395469776213148313610624249603032088056492212508044289899205645977582377986352377447874059953209596218791270081578222728825309110620318823134368992507794794896441705022437929970092801791281031133910106031660418079109915156001539609114472620599891407520600057005484912065880794981095647786391936960959339132707478555826449218608559197761504994640828832392981543184328285883471574515286227193215221873755396385400334547085415352580282730897405946375801797251605640148879476236801035404938224421492839109248106541678958556085083919375 * s ^ 56 + -313146382475288271683644045232089663386054156264705036017974881172260663814302495436142764546264209858810718894179447684614633309036631640400494439320967058747084930757722383499545472439592219070149433466592145004200875048330498909264882556736059403683290069618187819752073808333982677494970959170915869679439837875475346625520679479094687043591942994917664838167748503584838706285569759213262624862279234986858998071563873976693657147828824858160359244565914745188202034044516615905980638505803906462066796916322376466926928005725953380023869931081451529169306114747330337704091185818546818791830804685047718549445935104 / 5885779264635869079035125301397355368200678571181649650460185908671808598320053273467291547576001893498573953941453201048387686138240652744448668325080024148746238228804350898753747691284949987541007340944193052747611511112374301106641041979681654328704834721501072822426249257934160218991839598785670110586600831615774003192644087843143136565586912210923598379415817229354954308428982968619202721033767091349708825548676381745013685183756219377512097904352522877695916523274894654871789016941821087749287719938726626026901165172099704679298206875 * s ^ 57 + 9983338655133152971455324317631016141838740217563935036949827006045634802758131172951046490530289587500583087320855120802348123797667901840519774404092293890887595226127890859589764643238563186143305236631897712694992361088439885227428646142158030192587897605916688000454928921115566929069122324270417654612929254422144579733794128687299240617496451446783182552707070768306412571498578394877041813399533380662476524948892765701067509413382199638906575237377590092003056493983428719860658995175744048653597217425488804245939024433936854289401915204019542152902794805596441650004726993528441474831932954461092056422940672 / 86374119187528477050829931047759932028102201254238045184950317318034927019371850973314551012645730093270477311509795403225815100561183583251867250053585260044494062057925484887371559410890251389490673766476627608455514838127086179762027869722791572957932585011546142048183951374295852270320497256812768918461647424130855392764169003987425484191002904562820102004005703575439581046127632663174882698608741382490485909519359899822003765799357517070408145346892369274363554848897825123904660625980602964874243269541061597879052738374628789842950625 * s ^ 58 + -7995458867840879012555150920066964049919726431731189041098015208646930452026929092995913530119251235887819320337670159013313710445436628505855375494804431458341871801998974374418294893993355654364665614258092210435483446544984902645015977120442159877846073586960027676095918262936722326362126508953983292216382265157284184500255917531936828993870724454524945700752918863502625335672007410637271528562559391948374283849057488491647075978240380230387688059908723999562528044097145212262348251413033702383503379641723074385456577156957157588878190788720706700022204910326942267413069249654382603357556265850139404402688 / 33259191061813044686495930322587574904929611572675412085079059421653803241960666528037948021811986943885436007512435657768892992129835804101604639989828748573159053545600879818009841898687043276661791977850068389855800861812509118121689591729992904488999840204676989621942222323564055552684057472781197119161204244948346319893788603768742966573354988279869118984984868531166569521034898984664952906664898491525023453800292606785523205929671743192301942759681312774109955659952955380787316375040663444310451778799022563680805829177754636058125 * s ^ 59 + 4904498204615186519436576691159724553250088737907863164385015153213359483878088040821690841245428345161966998219304848846830728025833003658951646737413885874658727544185441774223451256767338771115302350972909580778635478898453747855106361985977700204914456334906620797155739055336246692972279286669427866320605421304169052905486295003247994064949343770850020954522646670870351312186789265521814519741293789273573802764125064289620331460825455474709149797834883272030083822969417022011874607443705700624237839335642430011940484248468434976709525639662103530993912033887612587845732817830101841295954658242614981033984 / 10249687811502133268165412489350887863783339415478586114269647243151172068277186540087166371501807297172241285334021051765256330907936820131941052575481815598017569960593981830707435553683428431172501930280838686181976366218949350867690503111758819622396177169994795543868986753802759258374332177146406659364144704418043834432676991098543429950279210224613753649460745647969571739186855661940771650481635384180667605259209671273526019437446008908319466636631347961832627844891162350053952845138317665227749290321711356102889846727735705451875 * s ^ 60 + -528575437701850526771939116428204562565793301872802275243265910296254250233547704175619334103515375686554957837886259357508522715283800485952485072134839006952297329510132448243616671474071724510395528620635950691284722055301274811050171314303481304494201573323006648908622092209520531593409071630493241330649214266707652785523355645078898186328970555351190209932177640915094816629754474393243251403595286235275018027187393269525161146730787454149030974314051789355182025585164713875066971000879455560065917146864622936871570454374800070434656246467091860436239746171600437770204230892709082133401864641697831452672 / 580171008198233958575400706944389879082075815970486006468093240178368230279840747552103756877460790405975921811359682175391867787241706799921191655215951826302881318524187650794760503038684628179575580959292755821621303748242416086850405836514650167305443990754422389275603023800156184436282953423381509020611964401021349118830773081049628110393162842902665300912872395168088966369067301619288961348017097217773638033540170072086378458723358994810535847356491394065997802541009189625695444064433075390249959829530831477522066795909568233125 * s ^ 61 + 123502787007746470698766275387691462405139002626605163332044237114579646254825160728845396884001301154507132155958762228979494780342551044338813428478375840203404176157148218749137996670528534979649256486348731544604864035378116510377267101011311410744535584824106977010583578859882761308821471615927841982188813843819421151055159816959990138052433594272489382087305619745184567928247611904884506684100285372712674638329665018647909493719886686260757927672750684301180098860873480398197150400147548318706558504149190248394235949071866725016947641857765738194438910436666426280680485958923912635394307872591446016 / 74466821742810160258683186618455895145947351555703504873327331559282278305716948729573065957830931896544207651310445664920018968969542651767576903506090595084441190928531337542646708129724634601408751246219067619255718617410141969817790506547895028533621356790453393566371842356585314393053902377535811708460013400208105393252570027088901053830466287113678000373876574915683348269678770583915923674498408062864027471895799008097340323286273776769418026871581490702861994935311152563944993462255560953696567812800774159610071466552376875 * s ^ 62 + -595848998771031481554040453748438693824634100524576768708342646796859818394394075177350275724516294512996413107124878964914514924979465550458882034539681702666319532881052788496965739492575738251817753662527173307218881105633137139358703386474615128205325343376030110649459325902464595587274669929898979446911164349913253456584739235480347402654505838265545172484523172228826244046347568252774468202325237563516787101463546606751578104942300368604885526958209155735132364462650165219276282510558605168178449085053810193031205160786883605852685895540660000778102757615536653089432812288578810659752648111273541632 / 206540052758360255811819404394585218612344541107328588988285240362537639829063989872589447090587679033811292919672368164966845064877788109619505751233873914668167076726303898467340869718292854460511064777249112076048879938854544708739909518161142814989478102796163185929370958989019645580734408481089892851766452260954556468077882905322046319114689513315295585942638802124631173502693948600672467550023886513981359214503442531892623160812872550662348112266461870440013457650768668432073849791539008682894254122296486820050575577041498125 * s ^ 63 + 2395602720455461304380095021214950154484725915396148559744831980343199163058645107734125360932454034411529734300799582328132381294333591638297910329507233226215790728523195875211010805353086324293336375577439379519256103264935291322892288 / 499889961203173745852563965186902561232507457197267571201417853998668152265018749307073011096335946163944053299943190731326488150187235798786402686280038088994375 * s ^ 64 + -2012574951168622416639374147133318667324726620518790917941986955302456588606454131126048017481448698160810194401771120958927266016047745312172435683746711179607197921759157450409944915532008034186290728312989158340835654772599105257472 / 264912539058385662878942217905088797685483549124148156439543112876877664157402622844235829939764677352381586274479698320787752066871879066659460883031286745625 * s ^ 65 + 112576273164284036502461108269673862613295753311923673274067153952825335089617744583048295462007550716154390527500050860593318532903843546742609301793010730526188558079167379220953997066304226825537551740682237195336416275399147941527552 / 9801763945160269526520862062488285514362891317593481788263095176444473573823897045236725707771293062038118692155748837869146826474259525466400052672157609588125 * s ^ 66 + -18019195303350090072558282845988140149807282216288818747652803466097124452367037534691370620831540921929548175647184236791768968738939877729886364165510470167010208111049719560280544575078344671552413108857438007401814729654485221638144 / 1089084882795585502946762451387587279373654590843720198695899464049385952647099671692969523085699229115346521350638759763238536274917725051822228074684178843125 * s ^ 67 + 1176813265188896067563723768815947149641741899623203330860426289490739583831118427140336931579174253747905958961200974269395608859618832802144408893979517761395852718869599839050315186506796604993087046425972864220313587267218672975872 / 51861184895027881092702973875599394255888313849700961842661879240446950126052365318712834432652344243587929588125655226820882679757986907229629908318294230625 * s ^ 68 + -80796763772256385896202514101749355886400795374434050942476254573958940493890622666978725680792115077537958299018920943848095892910723060554990860660488209448226745933449234874922856624884138377691468379871211042854128915948549177344 / 2729536047106730583826472309242073381888858623668471675929572591602471059265913964142780759613281275978312083585560801411625404197788784591033153069383906875 * s ^ 69 + 8654583369293343801774374450278997100233623612516460432092965666384436826901427040893674185784997059142665774744589171523440998919505611827819071516797302970012056360814941028652803388172214813159647175278784088377429261095727529984 / 235885831231445852923275384749314983620024819329374095450703804212559227343967873444437843423369986812940550433320069257794788017092857927620149030687498125 * s ^ 70 + -1131231313844559919436072100323724131109815687905347414985222610432109419351846689718635187315891246761492760268062782979368085775517397200180730994143991945954501738040034339512510364313499210564534003697770568151734653630501879808 / 26209536803493983658141709416590553735558313258819343938967089356951025260440874827159760380374442979215616714813341028643865335232539769735572114520833125 * s ^ 71 + 493612766944976557752224261722958854736849750570184530488311776853390443618874225728924211280307688086541867220225172099221931076250936729376486308774485255023127875616429839372385347632762862004084860208954587873754383892371996672 / 10255905705715037083620668902144129722609774753451047628291469748372140319302951019323384496668260296214806540579133445991077739873602518592180392638586875 * s ^ 72 + -190230424461059942927901559863232725391609166873100197593422990356338190709626204592575736570601546829170517887240950197818345786377320211002555513970579830686422539069443288066210052287459125634664500228579798690725932435060555776 / 3744219543356283379734529916655793390794044751259906276995298479564432180062982118165680054339206139887945244973334432663409333604648538533653159217261875 * s ^ 73 + 442900563162350863037590510046736961756594508444694583671211646734442396750600137748250685414902713539178187557599855885699792982739142637914912963661290686281532762581754330552401448969290352250367348600147042813538160805270257664 / 8736512267831327886047236472196851245186104419606447979655696452317008420146958275719920126791480993071872238271113676214621778410846589911857371506944375 * s ^ 74 + -417054414406524977981557250477132515150721425841755044646336105944621382430124261365925341230818064121455873149916754386086076034179474449498068085861906835957410500825227801238340962358852930168914325145763115918007909393710972928 / 8736512267831327886047236472196851245186104419606447979655696452317008420146958275719920126791480993071872238271113676214621778410846589911857371506944375 * s ^ 75 + 41105125022125994488949776273899280328408119687281214203420182590295032410357097677485743020581457149319987122296099344821253866998363115708327051282494703582586803233831165684934108266671184852813369237166048632809889542988365824 / 970723585314591987338581830244094582798456046622938664406188494701889824460773141746657791865720110341319137585679297357180197601205176656873041278549375 * s ^ 76 + -38216348643078948865032099321847771624938310366089343232507343534806017474566918284955666920202284389663664478071521592815105737093472289048647053910455276674166842998295202359364344006838914692769746175329150696560069995134976 / 1082189058321730197701874950104899200444209639490455590196419726534994230168085999717567215011951070614625571444458525481806240358088268290828362629375 * s ^ 77 + 388673489619618804502422855749560584405860420556229366896806275361362570776393891451255639284347517774785660835857513799190859916943492037143429484510813688848559282639141220385397525422541157387627643103581457657319355731410944 / 14068457758182492570124374351363689605774725313375922672553456444954924992185117996328373795155363917990132428777960831263481124655147487780768714181875 * s ^ 78 + -140519631695164332372982076252395752728197243471046833582183337871549468005113607023475052621035604134675501802635186159274483007055541663709665106843255059401154885307853105248686521441634546037394956659557071845728293224448 / 6947386547250613614876234247587007212728259414012801319779484664175271601079070615470801874150796996538337001865659669759743765261801228533712945275 * s ^ 79 + 2400211042189660210904602384015301536241758069592985154274418317771936763229549565726732513742864642277159470982307699861140448649132870514387401700639454647029277459797153499002649460203024241970222253786251105722078345560064 / 173684663681265340371905856189675180318206485350320032994487116604381790026976765386770046853769924913458425046641491743993594131545030713342823631875 * s ^ 80 + -53849186061269546737610750211886118371408994069339956859231405761324176163721898189053964319890985094682272242936367545582331091658468656256016771286105597452358342331303648543393387963707763256649004675491485505677021937664 / 6130046953456423777831971394929712246524934777070118811570133527213474942128591719533060477191879702827944413410876179199773910525118731059158481125 * s ^ 81 + 503732249997682482194405634960072931554490502856230041153448395931285987530603283868002732579577795543914603724095266546959399274409857167940355024668906369986730315723507516001224624139588694048610942527449149102310293504 / 97302332594546409171936053887773210262300552016986012882065611543071030827437963802112071066537773060761022435093272685710696992462202080304102875 * s ^ 82 + -2589606416607027908992710495598423033990782268635437131934558707477715771624561614725390457486750089332380025481849925306305173660321705364274489358914226485458376711852325038179468859630132977110379826559578591905972224 / 919185328153609803243660428089625468064917495437114831544479461270576539530453099345188255689290703677904395473215801349493763761451301703277625 * s ^ 83 + 259059620824242263822259382084710064574102212072858218145053859161010347640547627551175573210619306110609225970054485283332579499543364686960842883001057849282408541097797680771682075578061292621648845722755342226423808 / 183837065630721960648732085617925093612983499087422966308895892254115307906090619869037651137858140735580879094643160269898752752290260340655525 * s ^ 84 + -65810519927957567961375455890808523945471668933157090720484214492427844439712760873112624224461656990764351384390129758045347447671033390863324185886888082621380740521835964350821431796995450900970210036483353032523776 / 102131703128178867027073380898847274229435277270790536838275495696730726614494788816132028409921189297544932830357311261054862640161255744808625 * s ^ 85 + 1822315570228832052820273445049422538882953721241590859568412351605217556541307285986355198731100738571871445974318479471904820768129095064857683020896639155307233527741461895461070115968291024739301931839333140004864 / 6808780208545257801804892059923151615295685151386035789218366379782048440966319254408801893994745953169662188690487417403657509344083716320575 * s ^ 86 + -29663742130375531558562917937640408747978344193557531316544256216140987992895001829196479806505893523460865000113750539739515577236134352931238329078688647104636978797190421349286548513662659198462605385974444720128 / 296033922110663382687169219996658765882421093538523295183407233903567323520274750191687038869336780572594008203934235539289456928003639840025 * s ^ 87 + 1101891992676802190863865041676851732121918316121519094289116268011763815259653482785910035733382876370473244407257847646376935491142803617776982840000394765414564352188294278085306081996783284265288002074765688832 / 32892658012295931409685468888517640653602343726502588353711914878174147057808305576854115429926308952510445355992692837698828547555959982225 * s ^ 88 + -21673382059221089367370700923333779704618209416685481689582253777575048690566080089137675528093747881713433793174378904342083676195557480480031672862798259782244175083744894638381207814213852610800289252724703232 / 2192843867486395427312364592567842710240156248433505890247460991878276470520553705123607695328420596834029690399512855846588569837063998815 * s ^ 89 + 916307609639420314774556006349806755818688149428991704253295621363601390732709644769867500649277691715600154504000835474298707672912636001049380107521024143035124331799416444911119446140858853499294746167738368 / 361457780354900345161378778994699347841783996994533937952878185474441176459431929415979290438750647829785113802117503710976137885230329475 * s ^ 90 + -6230993737679935189132771362371652633037486572824710214719985757160166068076973716900477376145063530260699248837405804517146683735238196081854657479077787717102363876478630524928558090718023281992405501345792 / 11245353166596899627242895346501757488411057684274389180756210214760392156515660026274911258094464599148870207176989004341479845318276917 * s ^ 91 + 268849747401465481415524974249553863752195441005292189520678564799113619948376348049593027885733492447365751802691272395769376062437983583486626062118081485996487382593872971865208176900043516039172913627136 / 2677465039665928482676879844405180354383585162922473614465764336847712418218014291970216966212967761702111954089759286747971391742446885 * s ^ 92 + -125839021334010374449645321345013520683305902807844864934198510399902891295238176286818709600112201829960818317227577690668165873835766990322639053582947269982728336030521891273611981571375514462978048 / 8683003919696742680324688086877159767359214037373802490184313431664312528069783698668157253485303598433348210320373095950380214305 * s ^ 93 + 3566553781330096736625097402189143401929433402207594413218198392701198515491188847792505701799491366011997984010029216043971929931353493603370281421756463633394544133176482225002105309905045812150272 / 2282199497667419723640895029730931647666061620551122033818559009242037698948609815052243630609547229320029452980757066598452424143 * s ^ 94 + -11383606751761462808841879359704331601800840106793458994345139574043959321860477527649541615329354693647253126506629675822640912293164584101642534645635428604018591265643029118731795759670163931136 / 101664800971359711191376276286016924396798443926240459263806776141350373685882772099101482776769385023472894218804846284723687097 * s ^ 95 + 2846426162100540477504821406370358099097596818564993027077417967281494233146639620639655387504859468567430806465702543982189965316310808246859421143193791148489260371756378664313018408226839855104 / 711653606799517978339633934002118470777589107483683214846647432989452615801179404693710379437385695164310259531633923993065809679 * s ^ 96

theorem G67CenteredEvaluation.density5_eq (s : ℝ) : G67Centered.densityPolynomial G67Centered.rectangleLate s = D5 s

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

Equations

• G67CenteredEvaluation.H5 s = ⋯ + -3418655961042051791961167567340927538933626546544030579590372238317417309176042768504304241404899691952535256760373482659450146631067556099308042100696047820117385188631720881594149802162132174367280489093019017300807283067559566506601613775778830250224358729834427230921924519270612638604442614628528266906639582378724035428434487377440657090725141498315610747497763664513114417961281807854206555997173909104646965926530150921776715624994523343057421151827821295281792810022601097568657593858344673792935161783256312691062733697594402087959600893472978547639975538387613176542904756766506361420116255045367506206460380194155790336 / 74479801154278873525838556568748685175893750467206178409017527438929996950141814595089751682896240127326000539278327530544192733842688590832419043628989440856607396635871806164509041410844163779996646793772791570229190767630753592211240470894596541755463457005856686351717161702812484964470526378572505964530083086872580083076202934830688797637201416542620063789802909488878002832106197003328688614069961576795484279827357924462285339888290563925080040550281822802498352208292408859314890675522391207705576245784332305901995176195668424619368283940952189201199375 * s ^ 48 + 8105389767314047681817228573931863655962308689210393728530097192557423567213102009497200791135075608448084428844009051492035008957823884184714124443646848550314068158308252961801866004269062843146643644538357364379161666879171212283046890939507344961137856490219360428457072708858411970244992083598821803496798896406107544995935424381234454358970335649898423644642550597170519336833600103223720676345433994077753765380829633552554047618966084926242096146856845944751329602843551360346638697055352280299930551063038033392007982564897496348264069450928939762055677843653231844252347611659930113693096788638539030102333655058583912448 / 54431974660925312195709572409111593393908775008501739919610440094743075420906784060088026682632291648461467617376672077860997671867441222471232188643654680444034666966506061645007641445839752962435871862925229522705399086636191912318258381610317172658012711205213945592726435666547536586603170765158375868997498392497665674524859449113105767270981370389850019303817434142425745959351926059653151037887694881322291455481274191702595680824636594154924210700973054225053219411123401178340267160871700166055855933303566854904131186783861229393146789646760740972016875 * s ^ 49 + -139375451956046657751620595577847767527312717792357747961462380514612333191939061260293016033257719959770239494888157156662555971447058067296564082895903509557607113101490639904117975859502528677660125230839646554339067432717773582359546678621349161914040413388256065421692876518003394051198600569309824485658712460400421640752668791450134537194279854482750501507634734520297012510774102560441052986808455020170322601241695063264727340751311491013838507830008814257728539998854017483547748557862658242873366666408039760950732831084906176460292242135324450156895234506974281978888045309611198629270562269744592245946498941615865856 / 300637020654266017307321680439400399340458098266614423519621207744407827343648804459805040282922276725794996123874676875065168178396565182049811740571330385327890037978685023529212801992850661423794189465729480403490233282703173598938708180796473050817249339155013348775160828534703940443936617646311140748600947299811615444687875256280448687319078396132168441159441848560731333670563438134836998463508140048497544135958656417335648487415285901957126663339277466926801834522292467600551070859406818417610442872396576711625264019210504117015987900016664415578125 * s ^ 50 + 1083999430580460597237715422739327514368313843770612656213139784800103028603025186284051745060047231662872617767769826758910255936462942970409528827558377083782332325898615649603508434557760495493695902810622836762118141430894562099736717561969594987418698084917951356791658113603724382981203532027078498131754910485643239982542226126271346156150016737706644174937861289038647707096048330309295611051135685054599532674176631098025369490153737239860378661136096892705144511815948680884959971149447416934719690434299208321951741078190653471985215988170112410007021636309757035397769095105477295194061382053098639330611182652476096512 / 782641313796378517545390777961920343781419339736022303127756835026919248346449054268182387702378594411267477898329101292265831188097145655610318008040851487974711327032849923287102845765944207833175253691888822956333166342194770729548254524671506824955873967626681138036439389854826237816895504415909074240025619327772813456679123467445004964688928191738603910797823185439563873017801990084547682166676699311158181027881841997401922062323644327887394829441889318089076775768912427896414801549008568450505690977320590304430367480695943373046517382127137259904375 * s ^ 51 + -47135790210812555017008033875368170024331654601102898225344428461402153169611525759496203743716700734270926770822627627452975719130125243987636796211686910420493616485832267426072276414757254777887667715712182423746215563740211866000957446233939038541645736534994074419725145522646577434405092715745075101438750746061095261086315286332631222846062038095389160242701015295303255364488048634978784710806344182088797634449217313315544195449221394874897949824375589376311936138107190437397955399932832031926912740324755840718643325362149783116038354403843548253828370178852016186399247163601379244311991472863655947224860117683929088 / 11871362880374220946859423565090171696277540854301485175078812517981387044840699676283935588530344939275607322912132132069145053167585265216434716363179767298173571738197131651783653968332857018557227303502568161749781657428777506441538451909556707296777962513020320628743623745485710599516358002609053660318553604305839937744670389258322309860246413563182671232967351314473591858575612872166650006967719079451529937899798565258408732724849950959446240476181081036497279987615763797170923737887292381232235786189472512941785078323541871363265709458828201130625 * s ^ 52 + 129641709898718867428974642259687215630967490367372356819332339355427072026169313546417522093331314143288832166208760520741068060483078308944157141469491508279184947809917839381317773292154959380648481350852914232688914662825148656198419881825114917388821862101749087896465400000058127819192499904224546407830286766543510926636346092253760998946993591506360019529916558782633498254342690837874288730588271729908371396073200165060317518371633852153396709442703114376188848255324935835449499653545350173326162654919031758843586816688001207387485027534207061246453882363509271160940901666201608050326897271940520124378012525826932736 / 11871362880374220946859423565090171696277540854301485175078812517981387044840699676283935588530344939275607322912132132069145053167585265216434716363179767298173571738197131651783653968332857018557227303502568161749781657428777506441538451909556707296777962513020320628743623745485710599516358002609053660318553604305839937744670389258322309860246413563182671232967351314473591858575612872166650006967719079451529937899798565258408732724849950959446240476181081036497279987615763797170923737887292381232235786189472512941785078323541871363265709458828201130625 * s ^ 53 + -3287718443981123348651909921588296320146234540693937580191779534162098866153010131729556385531997779564636076958084188910345894737446241677523936052975085573256360917402940576696996259621871143657466424828132552834714078622053189104299448708722239291274315638078235702735993881942843242597546816820233918351145297958005696430267595810490563362916873142461502576186788838335232570542162097839599970776440619922452104065889889350912346359025396447834263153377754157366024317480705074918832444519991227025020897729327481711048035364784508382855000611194541340534732669908219599235282221162623533086606152613920730038790498988064768 / 114107083577822700450410977663736075400318121419060199262060497680846368889533247155452567066685408814681878860315972789557464021190744806281145369101407517639973811652304220220063601689208664827712757990234724231841973923309716153051455393933083338203276962567301052679272994349631251757544202944266446717195068464313876226096867394081417716705821703882496305906058556600493762969576912619615361405528093679313388509538825653961208894115681265897133674922352861511365809777723610723964023112480204447586460031013085742053469958966048603349296602131848141875 * s ^ 54 + 1254204455116215349534706792471483098656857318181025303080227068950667996417023301384216083842060083963167047655125330617227596152505420592716948781308005818315676582869905794421355596810895345197236539247781036760932502132778203319149538827124435810480769417345727584976668606288914810375311051267746516789164296391625935007375276193861373703099175802384230285034878414907583122522243672002785410792210314690732683849491468057285788169963635182655613643607195599297299875032359781811542276639962262551393405282207394279236229732567633523170773793063921218988006113141720340250895006331925720447044595257125094640909811712 / 17202269819624774466073181128737153393190820760108027658034271017561653628808863523892886633147299366775949152872610188405694014103952125584806247546101183656761730918553563173963911258623653716153508228134600088312866303561462299510864058122195489987057785902790543403196293023338918184833925326682852186196644270779221717839091755143018830643572146602134918796616961766099075692370525621335810277093738843801446406940099392790216296161774344215427803980944997176103223399369909981778186854693774501738234978038555497944866417963224011682299046940625 * s ^ 55 + -39641184570244159879601938834589802222762322351597693874446997408650798575456159115756752084956041917329860422682098506753044386060343482061726871812496414467143770269769092879329159910803494287701837806124505810637455327059525445567791931433461593272785073157384902297979737591962704906953494219074003557533091881705551136367314596906989222212541659667376794525276525693600928966189022702043083834051202069818875188129158389194868771652688058974285372003376390273058598370293792280286874466519903424555900337692314336671522241680695845898495794184895835837791430592093924081855418022096357906383299670738414503343037612032 / 224077001466567947378662933211175193043587761485280313063976081543009644567187571999426578440400216938286889972934516608330099651080777912706012107236604571279756440184280332057866800376382413107589644433908421013873232936451873304724453948268717310317966128228248492267455911988236270364453730315190626723111792039096760520312838800694358254900240986959756490617771116818157201224769306004006465158202416401405288126499782046318097284061831218881316057010400272730133348943426320797568145894714033029908430718747266594225386012359333635594099966005625 * s ^ 56 + 221944669927031960784593940321340532390991814145591164124078105936500804334221323264769042289447182296783162750080099382345271309055573490985054977885039642838029025922143648204932265002695361511117267557269504708856653534781549897198103356041377647266968377069158539903836252831500400946445167680624620070948398087082751150146357776636161831108143551762935717537517297021767774522714637105623579792633858698238747783965143892604608110714262327595933735972030546957360900497199472451436042520188277001453642849598243797455091897004238874276219688989597114459570354777587513577494134714676639168441147372352382508151989075968 / 539355154473437134795541777244149453875805582227372829019220056112958524524254721820722195545222085514528821417332946984471102394649958695543042619305358172918659032572944303309097177186278962008295289702103018774632876043804643830509265163892087757719524939374193810228674203249312639987755205313922451923824340406774682330564326277682107605460687874272405784694527243446399947961506712295357879747371314950013267646804057593967819069183868675097076115661152138943420702443341521488486130145497659018081478792025091829227142072875700637696849783404375 * s ^ 57 + -156573191237644135841822022616044831693027078132352518008987440586130331907151247718071382273132104929405359447089723842307316654518315820200247219660483529373542465378861191749772736219796109535074716733296072502100437524165249454632441278368029701841645034809093909876036904166991338747485479585457934839719918937737673312760339739547343521795971497458832419083874251792419353142784879606631312431139617493429499035781936988346828573914412429080179622282957372594101017022258307952990319252901953231033398458161188233463464002862976690011934965540725764584653057373665168852045592909273409395915402342523859274722967552 / 170687598674440203292018633740523305677819678564267839863345391351482449351281544930551454879704054911458644664302142830403242898008978929589011381427320700313640908635326176063858683047263549638689212887381598529680733822258854732092590217410767975532440206923531111850361228480090646350763348364784433207011424116857446092586678547451150960402020454116784353003058699651293674944440506089956878909979245649141555940911615070605396870328930361947850839226223163453181579174971944991281881491312811544729343878223072154780133789990891435699647999375 * s ^ 58 + 9983338655133152971455324317631016141838740217563935036949827006045634802758131172951046490530289587500583087320855120802348123797667901840519774404092293890887595226127890859589764643238563186143305236631897712694992361088439885227428646142158030192587897605916688000454928921115566929069122324270417654612929254422144579733794128687299240617496451446783182552707070768306412571498578394877041813399533380662476524948892765701067509413382199638906575237377590092003056493983428719860658995175744048653597217425488804245939024433936854289401915204019542152902794805596441650004726993528441474831932954461092056422940672 / 5096073032064180145998965931817835989658029874000044665912068721764060694142939207425558509746098075502958161379077928790323090933109831411860167753161530342625149661417603608354922005242524831979949752222121028898875375449498084605959644313644702804518022515681222380842853131083455283948909338151953366189237198023720468173085971235258103567269171369206386018236336510950935281721530327127318079217915741566938668661642234089498222182162093507154080575466649787187449736084971682310374976932855574927580352902922634274864111564103098600734086875 * s ^ 59 + -1998864716960219753138787730016741012479931607932797260274503802161732613006732273248978382529812808971954830084417539753328427611359157126463843873701107864585467950499743593604573723498338913591166403564523052608870861636246225661253994280110539969461518396740006919023979565734180581590531627238495823054095566289321046125063979382984207248467681113631236425188229715875656333918001852659317882140639847987093570962264372122911768994560095057596922014977180999890632011024286303065587062853258425595875844910430768596364144289239289397219547697180176675005551227581735566853267312413595650839389066462534851100672 / 498887865927195670297438954838813623573944173590131181276185891324807048629409997920569220327179804158281540112686534866533394881947537061524069599847431228597385803184013197270147628480305649149926879667751025847837012927187636771825343875949893567334997603070154844329133334853460833290260862091717956787418063674225194798406829056531144498600324824198036784774773027967498542815523484769974293599973477372875351807004389101782848088945076147884529141395219691611649334899294330711809745625609951664656776681985338455212087437666319540871875 * s ^ 60 + 4904498204615186519436576691159724553250088737907863164385015153213359483878088040821690841245428345161966998219304848846830728025833003658951646737413885874658727544185441774223451256767338771115302350972909580778635478898453747855106361985977700204914456334906620797155739055336246692972279286669427866320605421304169052905486295003247994064949343770850020954522646670870351312186789265521814519741293789273573802764125064289620331460825455474709149797834883272030083822969417022011874607443705700624237839335642430011940484248468434976709525639662103530993912033887612587845732817830101841295954658242614981033984 / 625230956501630129358090161850404159690783704344193752970448481832221496164908378945317148661610245127506718405375284157680636185384146028048404207104390751479071767596232891673153568774689134301522617747131159857100558339355910402929120689817287996966166807369682528176008191981968314760834262805930806221212826969500673900393296457011149226967031823701438972617105484526143876090398195378387070679379758435020723920811789947685087185684206543407487464834512225671790298538360903353291123553437377578892706709624392722276280650391878032564375 * s ^ 61 + -264287718850925263385969558214102281282896650936401137621632955148127125116773852087809667051757687843277478918943129678754261357641900242976242536067419503476148664755066224121808335737035862255197764310317975345642361027650637405525085657151740652247100786661503324454311046104760265796704535815246620665324607133353826392761677822539449093164485277675595104966088820457547408314877237196621625701797643117637509013593696634762580573365393727074515487157025894677591012792582356937533485500439727780032958573432311468435785227187400035217328123233545930218119873085800218885102115446354541066700932320848915726336 / 17985301254145252715837421915276086251544350295085066200510890445529415138675063174115216463201284502585253576152150147437147901404492910797556941311694506615389320874249817174637575594199223473566843009738075430470260416195514898692362580931954155186468763713387094067543693737804841717524771556124826779638970896431661822683753965512538471422188048129982624328299044250210757957441086350197957801788530013750982779039745272234677732220424128839126611268051233216045931878771284878396558765997425337097748754715455775803184070673196615226875 * s ^ 62 + 123502787007746470698766275387691462405139002626605163332044237114579646254825160728845396884001301154507132155958762228979494780342551044338813428478375840203404176157148218749137996670528534979649256486348731544604864035378116510377267101011311410744535584824106977010583578859882761308821471615927841982188813843819421151055159816959990138052433594272489382087305619745184567928247611904884506684100285372712674638329665018647909493719886686260757927672750684301180098860873480398197150400147548318706558504149190248394235949071866725016947641857765738194438910436666426280680485958923912635394307872591446016 / 4691409769797040096297040756962721394194683148009320807019621888234783533260167769963103155343348709482285082032558076889961195045081187061357344920883707490319795028497474265186742612172651979888751328511801260013110272896838944098520801912517386797618145477798563794681426068464874806762395849784756137632980844213110639774911911706600766391319376088161714023554224219688050940989762546786703191493399707960433730729435337510132440367035247936473335692909633914280305680924602611528534588122100340082883772206448772055434502392799743125 * s ^ 63 + -9310140605797366899281882089819354591009907820696512011067853856200934662412407424646098058195567101765568954798826233826789295702804149225920031789682526604161242701266449820265089679571495910184652400976987082925295017275517767802479740413665861378208208490250470478897801967226009306051166717654671553857986942967394585259136550554380428166476653722899143320070674566075410063224180753949601065661331836929949798460367915730493407889723443259451336358722018058361443194728908831551191914227478205752788266953965784266112580637295056341448217117822812512157855587742760204522387692009043916558635126738649088 / 206540052758360255811819404394585218612344541107328588988285240362537639829063989872589447090587679033811292919672368164966845064877788109619505751233873914668167076726303898467340869718292854460511064777249112076048879938854544708739909518161142814989478102796163185929370958989019645580734408481089892851766452260954556468077882905322046319114689513315295585942638802124631173502693948600672467550023886513981359214503442531892623160812872550662348112266461870440013457650768668432073849791539008682894254122296486820050575577041498125 * s ^ 64 + 2395602720455461304380095021214950154484725915396148559744831980343199163058645107734125360932454034411529734300799582328132381294333591638297910329507233226215790728523195875211010805353086324293336375577439379519256103264935291322892288 / 32492847478206293480416657737148666480112984717822392128092160509913429897226218704959745721261836500656363464496307397536221729762170326921116174608202475784634375 * s ^ 65 + -91480679598573746210880643051514484878396664569035950815544861604657117663929733233002182612793122643673190654625960043587603000729442968735110712897577780891236269170870793200452041615091274281195033105135870833674347944209050238976 / 794737617175156988636826653715266393056450647372444469318629338630632992472207868532707489819294032057144758823439094962363256200615637199978382649093860236875 * s ^ 66 + 112576273164284036502461108269673862613295753311923673274067153952825335089617744583048295462007550716154390527500050860593318532903843546742609301793010730526188558079167379220953997066304226825537551740682237195336416275399147941527552 / 656718184325738058276897758186715129462313718278763279813627376821779729446201102030860622420676635156553952374435172137232837373775388206248803529034559842404375 * s ^ 67 + -4504798825837522518139570711497035037451820554072204686913200866524281113091759383672842655207885230482387043911796059197942242184734969432471591041377617541752552027762429890070136143769586167888103277214359501850453682413621305409536 / 18514443007524953550094961673588983749352128044343243377830290888839561195000694418780481892456886894960890862960858915975055116673601325880977877269631040333125 * s ^ 68 + 1176813265188896067563723768815947149641741899623203330860426289490739583831118427140336931579174253747905958961200974269395608859618832802144408893979517761395852718869599839050315186506796604993087046425972864220313587267218672975872 / 3578421757756923795396505197416358203656293655629366367143669667590839558697613206991185575853011752807567141580670210650640904903301096598844463673962301913125 * s ^ 69 + -40398381886128192948101257050874677943200397687217025471238127286979470246945311333489362840396057538768979149509460471924047946455361530277495430330244104724113372966724617437461428312442069188845734189935605521427064457974274588672 / 95533761648735570433926530823472568366110051828396508657535040706086487074306988744997326586464844659240922925494628049406889146922607460686160357428436740625 * s ^ 70 + 8654583369293343801774374450278997100233623612516460432092965666384436826901427040893674185784997059142665774744589171523440998919505611827819071516797302970012056360814941028652803388172214813159647175278784088377429261095727529984 / 16747894017432655557552552317201363837021762172385560776999970099091705141421719014555086883059269063718779080765724917303429949213592912861030581178812366875 * s ^ 71 + -141403914230569989929509012540465516388726960988168426873152826304013677418980836214829398414486405845186595033507847872421010721939674650022591374267998993244312717255004292439063795539187401320566750462221321018966831703812734976 / 235885831231445852923275384749314983620024819329374095450703804212559227343967873444437843423369986812940550433320069257794788017092857927620149030687498125 * s ^ 72 + 493612766944976557752224261722958854736849750570184530488311776853390443618874225728924211280307688086541867220225172099221931076250936729376486308774485255023127875616429839372385347632762862004084860208954587873754383892371996672 / 748681116517197707104308829856521469750513557001926476865277291631166243309115424410607068256783001623680877462276741557348675010772983857229168662616841875 * s ^ 73 + -95115212230529971463950779931616362695804583436550098796711495178169095354813102296287868285300773414585258943620475098909172893188660105501277756985289915343211269534721644033105026143729562817332250114289899345362966217530277888 / 138536123104182485050177606916264355459379655796616532248826043743883990662330338372130162010550627175853974064013374008546145343371995925745166891038689375 * s ^ 74 + 442900563162350863037590510046736961756594508444694583671211646734442396750600137748250685414902713539178187557599855885699792982739142637914912963661290686281532762581754330552401448969290352250367348600147042813538160805270257664 / 655238420087349591453542735414763843388957831470483598474177233923775631511021870678994009509361074480390417870333525716096633380813494243389302863020828125 * s ^ 75 + -104263603601631244495389312619283128787680356460438761161584026486155345607531065341481335307704516030363968287479188596521519008544868612374517021465476708989352625206306950309585240589713232542228581286440778979501977348427743232 / 165993733088795229834897492971740173658535983972522511613458232594023159982792207238678482409038138868365572527151159848077813789806085208325290058631943125 * s ^ 76 + 3736829547465999498995434206718116393491647244298292200310925690026821128214281607044158456416496104483635192936009031347386715181669374155302459207499518507507891203075560516812191660606471350255760839742368057528171776635305984 / 6795065097202143911370072811708662079589192326360570650843319462913228771225411992226604543060040772389233963099755081500261383208436236598111288949845625 * s ^ 77 + -19108174321539474432516049660923885812469155183044671616253671767403008737283459142477833460101142194831832239035760796407552868546736144524323526955227638337083421499147601179682172003419457346384873087664575348280034997567488 / 42205373274547477710373123054091068817324175940127768017660369334864774976555353988985121385466091753970397286333882493790443373965442463342306142545625 * s ^ 78 + 388673489619618804502422855749560584405860420556229366896806275361362570776393891451255639284347517774785660835857513799190859916943492037143429484510813688848559282639141220385397525422541157387627643103581457657319355731410944 / 1111408162896416913039825573757731478856203299756697891131723059151439074382624321709941529817273749521220461873458905669815008847756651534680728420368125 * s ^ 79 + -8782476980947770773311379765774734545512327716940427098886458616971841750319600438967190788814725258417218862664699134954655187940971353981854069177703441212572180331740819078042907590102159127337184791222316990358018326528 / 34736932736253068074381171237935036063641297070064006598897423320876358005395353077354009370753984982691685009328298348798718826309006142668564726375 * s ^ 80 + 2400211042189660210904602384015301536241758069592985154274418317771936763229549565726732513742864642277159470982307699861140448649132870514387401700639454647029277459797153499002649460203024241970222253786251105722078345560064 / 14068457758182492570124374351363689605774725313375922672553456444954924992185117996328373795155363917990132428777960831263481124655147487780768714181875 * s ^ 81 + -26924593030634773368805375105943059185704497034669978429615702880662088081860949094526982159945492547341136121468183772791165545829234328128008385643052798726179171165651824271696693981853881628324502337745742752838510968832 / 251331925091713374891110827192118202107522325859874871274375474615752472627272260500855479564867067815945720949845923347190730331529867973425497726125 * s ^ 82 + 503732249997682482194405634960072931554490502856230041153448395931285987530603283868002732579577795543914603724095266546959399274409857167940355024668906369986730315723507516001224624139588694048610942527449149102310293504 / 8076093605347351961270692472685176451770945817409839069211445758074895558677350995575301898522635164043164862112741632913987850374362772665240538625 * s ^ 83 + -647401604151756977248177623899605758497695567158859282983639676869428942906140403681347614371687522333095006370462481326576293415080426341068622339728556621364594177963081259544867214907533244277594956639894647976493056 / 19302891891225805868116868989882134829363267404179411462434068686682107330139515086248953369475104777235992304937531828339369038990477335768830125 * s ^ 84 + 259059620824242263822259382084710064574102212072858218145053859161010347640547627551175573210619306110609225970054485283332579499543364686960842883001057849282408541097797680771682075578061292621648845722755342226423808 / 15626150578611366655142227277523632957103597422430952136256150841599801172017702688868200346717941962524374723044668622941393983944672128955719625 * s ^ 85 + -32905259963978783980687727945404261972735834466578545360242107246213922219856380436556312112230828495382175692195064879022673723835516695431662092943444041310690370260917982175410715898497725450485105018241676516261888 / 4391663234511691282164155378650432791865716922643993084045846314959421244423275919093677221626611139794432111705364384225359093526933997026770875 * s ^ 86 + 1822315570228832052820273445049422538882953721241590859568412351605217556541307285986355198731100738571871445974318479471904820768129095064857683020896639155307233527741461895461070115968291024739301931839333140004864 / 592363878143437428757025609213314190530724608170585113661997875041038214364069775133565764777542897925760610416072405314118203312935283319890025 * s ^ 87 + -337087978754267404074578612927731917590663002199517401324366547910693045373806838968141815983021517312055284092201710678858131559501526737854981012257825535279965668149891151696438051291621127255256879386073235456 / 296033922110663382687169219996658765882421093538523295183407233903567323520274750191687038869336780572594008203934235539289456928003639840025 * s ^ 88 + 1101891992676802190863865041676851732121918316121519094289116268011763815259653482785910035733382876370473244407257847646376935491142803617776982840000394765414564352188294278085306081996783284265288002074765688832 / 2927446563094337895462006731078070018170608591658730363480360424157499088144939196340016273263441496773429636683349662555195740732480438418025 * s ^ 89 + -10836691029610544683685350461666889852309104708342740844791126888787524345283040044568837764046873940856716896587189452171041838097778740240015836431399129891122087541872447319190603907106926305400144626362351616 / 98677974036887794229056406665552921960807031179507765061135744634522441173424916730562346289778926857531336067978078513096485642667879946675 * s ^ 90 + 916307609639420314774556006349806755818688149428991704253295621363601390732709644769867500649277691715600154504000835474298707672912636001049380107521024143035124331799416444911119446140858853499294746167738368 / 32892658012295931409685468888517640653602343726502588353711914878174147057808305576854115429926308952510445355992692837698828547555959982225 * s ^ 91 + -1557748434419983797283192840592913158259371643206177553679996439290041517019243429225119344036265882565174812209351451129286670933809549020463664369769446929275590969119657631232139522679505820498101375336448 / 258643122831728691426586592969540422233454326738310951157392834939489019599860180604322958936172685780424014765070747099854036442320369091 * s ^ 92 + 268849747401465481415524974249553863752195441005292189520678564799113619948376348049593027885733492447365751802691272395769376062437983583486626062118081485996487382593872971865208176900043516039172913627136 / 249004248688931348888949825529681772957673420151790046145316083326837254894275329153230177857806001838296411730347613667561339432047560305 * s ^ 93 + -62919510667005187224822660672506760341652951403922432467099255199951445647619088143409354800056100914980409158613788845334082936917883495161319526791473634991364168015260945636805990785687757231489024 / 408101184225746905975260340083226509065883059756568717038662731288222688819279833837403390913809269126367365885057535509667870072335 * s ^ 94 + 3566553781330096736625097402189143401929433402207594413218198392701198515491188847792505701799491366011997984010029216043971929931353493603370281421756463633394544133176482225002105309905045812150272 / 216808952278404873745885027824438506528275853952356593212763105877993581400117932429963144907906986785402798033171921326852980293585 * s ^ 95 + -355737710992545712776308729990760362556276253337295593573285611688873728808139922739048175479042334176476660203332177369457528509161393253176329207676107143875580977051344659960368617489692622848 / 304994402914079133574128828858050773190395331778721377791420328424051121057648316297304448330308155070418682656414538854171061291 * s ^ 96 + 2846426162100540477504821406370358099097596818564993027077417967281494233146639620639655387504859468567430806465702543982189965316310808246859421143193791148489260371756378664313018408226839855104 / 69030399859553243898944491598205491665426143425917271840124800999976903732714402255289906805426412430938095174568490627327383538863 * s ^ 97

theorem G67CenteredEvaluation.primitive5_deriv (s : ℝ) : HasDerivAt H5 (D5 s) s

theorem G67CenteredEvaluation.integral5_eq : ∫ (s : ℝ) in G67Centered.a + G67Centered.c..G67Centered.cutoff, G67Centered.densityPolynomial G67Centered.rectangleLate s = H5 G67Centered.cutoff - H5 (G67Centered.a + G67Centered.c)

theorem G67CenteredEvaluation.endpoint5_eq : H5 G67Centered.cutoff - H5 (G67Centered.a + G67Centered.c) = 5205645040153723383044501444518146901396789797651465874739520123765759986800790764389695197381960813569286292338217146863648128679631650013964034443603426926966671062722422127210103573901813993908891003691945242463331499740100832669992861230777404427596052562825651895586332841436454125054315450047716672988820052062741758889285379072138229489711683716143178060561208255765036896768026200103574414573908504664894626943699401438658648589050299553980446094784836690185306992995740977934136890902566004443550375487392833688874038363550168606860258035539353067306802231685336712990115662858389692258255940552596849907932460708311326673541590648391643640074587462887733431725804470159074637344014103624433402682762401335537706773523235957004087542821017 / 86796401306515887944123806647261238015597122891412260171727491937110350562371684889242309101072011753955029311057215587738923339541378098940109661084709595661817721605049944881356026155665485740701625436310577410227619220840523486371286628126900683310481115849289130286583034934824977561264430435477099407477628129402694024077920065552037230706914441124410944922533806088788590104729611182445067561400676083698869947877852091325560940423597952717313380339216744221731636274824697017009468198294117456502684028621026115437465665282977122450606762169868853991782012798783556641810844457456516714692509032047991163043423870388508625585828898332600373532776380446872607806872917440792433031988596037911627226703991631208115739469159986598042472525557937500