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

Equations

• G67CenteredEvaluation.W1 s = -5161135617187752767707000148836760261250301798194750383669132353889966012220643039749098807694888701658583220989261654924868928847819749483182031057052874262952831159670417897161980230620244651136966612766615594019699249374043734838603192122135059744863805389 / 163518825177206054215680525933256750842101581440883862918104206233179826772054456490260907263156788633362365406714198958715519239576637758053625619512219195522336952999269490254036297685154346513635142020173795558441252349318175048130774209074480494716400 * s ^ 0 + 53915236361572225265685682293579359195789543176934316101081074038370664891949884572 / 14040069290770566799142677182453604226329082520588613713550905579559501346123 * s ^ 1 + -3207355856210957883773921813067169363978840480333678087045762321196251452325379705024 / 14040069290770566799142677182453604226329082520588613713550905579559501346123 * s ^ 2 + 372050694599526530400430748471509332360073114759827442203630654440764819623808514864896 / 42120207872311700397428031547360812678987247561765841140652716738678504038369 * s ^ 3 + -3498501648488272258376927254339904482889517474644859289983655285417491550033259641296448 / 14040069290770566799142677182453604226329082520588613713550905579559501346123 * s ^ 4 + 13216041685756668923182661177503837859829057370570466719593291253143660723999962220982784 / 2420701601856994275714254686629931763160186641480795467853604410268879542435 * s ^ 5 + -20044127382728172360769176551006876607053839324677829690151120079307144690597733440617472 / 207488708730599509346936115996851293985158854984068182958880378023046817923 * s ^ 6 + 686199631046712234606642163621643764756087908486345227864794716271906636569159644620230656 / 484140320371398855142850937325986352632037328296159093570720882053775908487 * s ^ 7 + -8507092558730605764488989762536803414063481768840415887608735854268963125974469804307208448 / 484140320371398855142850937325986352632037328296159093570720882053775908487 * s ^ 8 + 813312811823370753108090454835762236279820284868212425023118353240418008681598135399357206528 / 4357262883342589696285658435933877173688335954665431842136487938483983176383 * s ^ 9 + -4156310785448892740192189439600615859841210395384288415521217181844822161750754448286647959552 / 2420701601856994275714254686629931763160186641480795467853604410268879542435 * s ^ 10 + 6675199209324469229197076335158025132073099892362486770585592883999864365775982665121496891392 / 484140320371398855142850937325986352632037328296159093570720882053775908487 * s ^ 11 + -141258909318109265050653847429900169601201090135933547983337036978736718774796476788848316432384 / 1452420961114196565428552811977959057896111984888477280712162646161327725461 * s ^ 12 + 41878311780122524546123932799103693398396588878620388487825842464678036987814051725443217358848 / 69162902910199836448978705332283764661719618328022727652960126007682272641 * s ^ 13 + -1616489013235201717434676794043041817936723214936398874619826063078176443280133528285428234059776 / 484140320371398855142850937325986352632037328296159093570720882053775908487 * s ^ 14 + 118719950961554915221266368136120765607421824236682069612595597606657059719689968842595106136522752 / 7262104805570982827142764059889795289480559924442386403560813230806638627305 * s ^ 15 + -34462699519702252901758885223940235481347915583722553487123932873222414981364563469382491775778816 / 484140320371398855142850937325986352632037328296159093570720882053775908487 * s ^ 16 + 2270325245457560114902510084806216990551755504528708837284802687991096547269091937732430527652691968 / 8230385446313780537428465934541767994744634581034704590702254994914190444279 * s ^ 17 + -4144838987465235361224322776063079963520222647191496299832201348408149941677713287985896727292936192 / 4357262883342589696285658435933877173688335954665431842136487938483983176383 * s ^ 18 + 26828141474295749701320853899751067092589642821450873989048428826500564983192413919019927196435218432 / 9198666087056578247714167809193740700008709237627022777843696759021742261253 * s ^ 19 + -2744524773208513373424974876074880619323860267378184561364679434634490491884294585231385615130427392 / 345814514550999182244893526661418823308598091640113638264800630038411363205 * s ^ 20 + 27765141144637358090309703416243290580182167608807849606172936815563524303627111539620632083346489344 / 1452420961114196565428552811977959057896111984888477280712162646161327725461 * s ^ 21 + -19659458100847856617925951920463163622711807099245696117522129996437094153572742535484298293581709312 / 484140320371398855142850937325986352632037328296159093570720882053775908487 * s ^ 22 + 842852323493146449439186438181194173200640498640711267291800867974753915207598802339927623669458665472 / 11135227368542173668285571558497686110536858550811659152126580287236845895201 * s ^ 23 + -178670860130973744263433556401373373773116345616619423559495033517091658485248171860102242768615636992 / 1452420961114196565428552811977959057896111984888477280712162646161327725461 * s ^ 24 + 2092230113500931385710663712737884879217657994165109010751440511368398180160189550099702848466817384448 / 12103508009284971378571273433149658815800933207403977339268022051344397712175 * s ^ 25 + -1307559379142876100628894795505234700356135628261232008387497003215710242135350868509540990892155863040 / 6293824164828185116857062185237822584216485267850068216419371466699086810331 * s ^ 26 + 393126258955158354700258221753204673443693334785763400015622972835885048043128651707684960014774042624 / 1867398378575395584122425043971661645866429694856613646629923402207421361307 * s ^ 27 + -85416390213702170635632895891978258906949352009660605148795695361642568285487573918892771975284916224 / 484140320371398855142850937325986352632037328296159093570720882053775908487 * s ^ 28 + 1671272744553741729160768940655046367740099443311321216370767340390952466217255175655702619030019899392 / 14040069290770566799142677182453604226329082520588613713550905579559501346123 * s ^ 29 + -13087467914246649003091635722792611549020579499792162826976371055630204334841869876226295070486326935552 / 210601039361558501987140157736804063394936237808829205703263583693392520191845 * s ^ 30 + 10254033797563979182387523777338931190787548422620986597059192472516753597129060790358402108766904385536 / 435242148013887570773422992656061731016201558138247025120078072966344541729813 * s ^ 31 + -81029362761624705937414698447117115479449747562684941625101500524872527171158290883999445280872202240 / 14040069290770566799142677182453604226329082520588613713550905579559501346123 * s ^ 32 + 28886137518384761170752565121662769911328801233066455280330456098830017043044553092856134355514294272 / 42120207872311700397428031547360812678987247561765841140652716738678504038369 * s ^ 33

theorem G67CenteredEvaluation.weight1_eq (s : ℝ) : G67Centered.squareEarly s = W1 s

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

Equations

• G67CenteredEvaluation.D1 s = ⋯ + 64799518255127855734251053813739226358314912716346233751035898118074582337703405961375854733292487831759128688627510628595419478012826427101508111958420735539287220732697684926043034000144675893935200161328927236513701212938807105579614832948003112690440864043613710041798743356405055950508073168715874468783396270447876060296814507055421200266711826782795043641137173775789267753478189790261377733421237632920707014159322303223149171215473146599192827789312 / 543381809478140886941335865253417869667175217755523162986172507726014900486230738738901112018177500268037089425252852632115919187077111154830249793051333891024361837363422026022250248707124044649502854719097344326294134904383230449856304171086027861177298704204423103524339815152035714743460225400768072611419376754087972894219120165075820535121018789879454954171446950475470387423096103875625 * s ^ 47 + -24749994654686509166092785437654493655056916021687515779348739355910183258726341204586660618271896093028688859466801643202619518342296095270523692863662398367752004100259154750612582563159250213682405300209546301123371573316432206877196065306725777404502610505428952120486383067312076955209475482533620875093666866248808461015615521604908004661993529068742157798687554967671501250150866067076661900794937015066270933116897736857143783463679561055272007892992 / 51816623341362746485481798471386609703091160489690378112398908181930028756208642602842686357674244033718988129792087425908045327885476688400436874707087933514306814679734787795084546919037326032359527706512597342690975638510792500827704681281533508434551176790528873207063511184819315990324865961215517378039481618059383442742975762809371973517404647479580865084171636786799062951615997666875 * s ^ 48 + 9493036961966726507636771143921921086030082250427243039528054412497642345335655539199487425890167727758184777812392583373685055844800707428508518089265934701919378940207203365141258260255512211018548421974131117091400956322454981182051333677499533770115938737150563482148823211133462689896085166693790323589814467157227320543989457198187791314903448586091661915488865899994123636053397949335764712960531837766912447639718113202577354033373752361977018056704 / 5167695589300327816611392300380874822141166949106587574551912675825905832829433359313152008716838353767122805397054541128295625692082580783871062976178580970429520601482984227542124625348736019399737264530905934446269807614283888222709092203279622134982192833556787893965902732717829357525660486698043512095581724712121798871940979040287770943784290988529628054216578331837103313233940468125 * s ^ 49 + -4629955851110258148193396451639534291540653213220413152262545322000566733936786424039708280234301936207820022382904471461251504559028716621962296316178417461259013273052575104858780933404378999695873026123567678465465057552530164898503486659487161978878045049453190786136665723099457501830157608639991220550202939361741348432780952460537656804908411563956661998632173610983719112742450126047900480709658232783608742720996678519249588540238300261136073752576 / 682525832549099900307165020805021202924305068749926660789875259071346053392566670097963472849393744837167162976969467696189988298954303122398064921382076731943521588875111124392356082593229285581097374560685689455167710439622400331301200857036931225375006600658443684108704134509901990616596668054458577069227774961978350794407299118528573520877170507919007478858793364582258928162973269375 * s ^ 50 + 309718592616140861821582258190835411477965353596942476689011268333537262655947093325526926364800024018655899642984067681410314839573898914186191076857491106715722791691205673553307720267879489982124943457753806132182256991309145527771284842712736084209824951459506921686279628159825771275254480888537151918747572562835705412955055854460735916379388952835257417097190234076211243224758259324268372874611023599707462020370246078830133886194223187676289302528 / 12877845897152828307682358883113607602345378655658993599808967152289548177218239058452140997158372544097493641074895616909245062244420813630152168327963711923462671488209643856459548728174137463794290086050673385946560574332498119458513223717677947648585030201102711020918945934149094162577295623669029756023165565320346241403911304123180632469380575621113348657713082350608659021942891875 * s ^ 51 + -19889738387575918004232746533059684231968802615447270843668123116885352268735861792949950051980751559951346521631112589492922485067091696168398015100096285582970304527124632485206460621455599720247956019177704635271799677971143671849215916231823566864831935817271797732834834855491315333227094263498713678352070150616805803563644161102455411193280433103447909504464659968354335062546989525442746122795281705542858773805937954566347031978041259817600811008 / 242978224474581666182686016662520898157459974635075350939791833062066946739966774687776245229403255549009313982545200319042359664989071955285889968452145507989861726192634789744519787324040329505552643133031573319746425930801851310537985353163734861294057173605711528696583885549982908727873502333377919924965388024912193234036062341946804386214727841907799031277605327369974698527224375 * s ^ 52 + 472095301199298938883336700492243572557588452020273770721796094546645394308595674582187847784373381842187859649513499755392380721046751821292930553401124450302697660454725098526140569940601719125240050861959241070425176541962211941591535291834973746951447763402348372609540558921357575422525245012128442149284962095487000022004276358013150328297579253252346138049588503637530340714714823937642350348670649559354380088132286637833182921636071723761664 / 1765304120680477954844021887827906642333752113360665433553896245029220557391814754962374911758874576245517788904070737055400350658517970337950828375644942335422306770458183170309135993810276948769281268902663983258959364802652198912663998032299495508562544398876145397785426475759278912009310469506745227984142719283586963434122553177808969610906109675952652416631710953640083249375 * s ^ 53 + -599409311875414340176409363953195118770311250883470004056351812223745235705998407182830627533937810790915453657886872577651302059918455945244523839228192495213119916206498079773710570805213547305679348122935957247329851107031711788928985326109377762123108899230718463356459222941568805385519312392342445978248564075298105554629897500603312339890473299609235295765254313050697880374446248455969423026351612416777294687654024151990591753784526217674752 / 714875222424325783366587376062540706399618624418781869786288562036626506712387793331870832034585572198598112861979058807558819688160169806277608185178530367237132493821908887149980691708293970989213075836615993220570321283718659063806081847790704792723675004503563012326329729852931129656662917403557984886140440040460836432000042195972227363094209703484958416652511047341851894375 * s ^ 54 + 4116790674012712391299127352279842683161098943778729230193095026444564127333782168585308000751782017034125987202036051695983634521947696092090024624008954513556395009677309737134375439390823827638900909655199154740056092973255067400454411208664313464862950386710676876057904836802791305083094576858627421595684217912333859632821517245969145809695403788316646729264806333423254088675108223382000334777928581484835342567584033188906599168120384384925696 / 1632073621006479618629378726482404254233091576503256721587564452951543534192432509304837182569525551623214559552820115390841833627686425406784728120879286310107415693442471232927314409371765480937637399551519531692245450477923731070198790633635382639991786331036436311160111270041597484687853075581707852287226287639542664307018964258729047376120742907956225819150072391101209041875 * s ^ 55 + -74717413745747867061074993010447293389271441020439296488952924712847500322977946613069770086489813023113436371201005864258494841369921754349132930014907521925643639360928914353255158495076211153034054429208118207121548545480799769782382361822651289780801476982300184783398735470635269387279762156642205592801946252635487453593131800823188862412832052730911585280280507052176934385870009579305469130812331917276490663430584825909601258225708568674304 / 10264613968594211437920620921272982731025733185555073720676505993405934177310896284936082909242299066812670185866793178558753670614380034004935396986662178050990035807814284483819587480325569062500864148122764350265694657093859943837728242978838884528250228497084505101635919937368537639546245758375521083567460928550582794383767070809616650164281401936831608925472153403152258125 * s ^ 56 + 11704058765778918458532600940919457486673777497146485356983385989965301464912345128240072661552969682282997428050425956001184123250414946866520589446574594463962603923419134063074755303748671254817115737710031765196344793261955669223452744128406758365777004116631201670282532026283633237825362192028563124859471059644595583043262812654388328181731050730738443542938777211469939696322016121470145901468826444117599693671811180446219798310922949230592 / 581015885014766685165318165355074494209003765220098512491122980758826462866654506694495259013715041517698312407554330861816245506474341547449173414339368568923964291008355725499221932848617116745331932912609302845227999458143015688928013753519182143108503499834971986885052071926520998464881835379746476428346845012297139304741532309978300952695173694537638241064461513385976875 * s ^ 57 + -21698632733568083212142596423811346296208569008756719845133216438641237887289952114711598729543441777385937495162273835852148641982439873430787741865204163709769906593804787364585529333769558057200291854348216915945173209400256865541969798814566416418617484500263801282193439777701183511004441763292609440444993023102227747832720003241034130003191244538209644639299229276292821588648139632352921099948194538884436049677652191216931181224406286336 / 406020884007523889004415209891736194415795782823269400762489853779752944001855001184133654097634550326833202241477519819578089103056842451047640401355254066334007191480332442696870672850186664392265501685960379346770090466906370152989527430831014775058353249360567426195004941947254366502363267211562876609606460525714283231824970167699721140947011666343562712134494418858125 * s ^ 58 + 3122613377794844184055734392113704079060603287416789927193193965424119115370763428691606874467982562386061699412048163177675495056591290119677509303797366683639026645782896343190367490746330112619773590387318337852446614903928347032117947450628592316258577190305970751210515767808788624706204106520242423259943329489781784815800837681101532920498885591278924829717472511754151357967382796560666641185901637676007481939943970019761083090173165568 / 22982314189105125792702747729720916665045044310751098156367350213948279849161603840611338911186861339254709560838350178466684288852274101002696626491806833943434369329075421284728528651897358361826349152035493170571891913221115291678652496084774421229718108454371741105377638223429492443529996257258276034506026067493261315008960575530172894770585566019446945969877042576875 * s ^ 59 + -47828406273579604121258723919790578221057194534771663203682667829573018672389077537414299062180372029552242986748773182976694047984818923993043458713645989234215739827225520964446768892843685801933611755028457014599145083264979963838855665250881175468332738924439178646011269115292485252855331530127151754744441959359443892115971981285353472295667595407250303213983397220033764743907683966677363277761764176048580486685397877523919077665406976 / 144542856535252363476117910249817085943679523966988038719291510779548929868940904657932949126961392070784336860618554581551473514794176735866016518816395182034178423453304536381940431772939360766203453786386749500452150397617077306155047145187260510878730241851394598147029171216537688324088026775209283235886956399328687515779626261196055941953368339744949345722497123125 * s ^ 60 + 119108740821139982008895635478255636235304659595125073352188718449107809697102819930561852169000909392591859764099169950368559238152073763974313555528547531467353094287422754022868426326377316539684976488930569407903350263853683103081592623504942902726501094804608648349553862723807706762691290521974374349649041531522503763011553125984663507223298270689956387036946868325134188111097739380129939992537312147146106162417270261159606915956736 / 154371153295036344047117739675845944404072115308281992224234436574811957852197477384762850616192301962389822207851784885957429884080644431327180333374576556106278131135604702437102632722968345424923588949505250445481114700196237778022478261146949637819932618566815163560372913367608780695003232582993182523197176645776455161031996718970511863958741551881398375638124375 * s ^ 61 + -88595453460014694932682409899887323180842704027956949995051247728022007221276864808506097476580863960248103224294280185746967733971653152315802338360272842539538498874149364042167907422645389077418694948541708856138520734896518999941984463077362817927045609597335572690813588442638952906360859375974295320288378617473186147395795294815555065130592941641177958654812203183265373376727445207799627120352295078866572766919680133594453351858176 / 51457051098345448015705913225281981468024038436093997408078145524937319284065825794920950205397433987463274069283928295319143294693548143775726777791525518702092710378534900812367544240989448474974529649835083481827038233398745926007492753715649879273310872855605054520124304455869593565001077527664394174399058881925485053677332239656837287986247183960466125212708125 * s ^ 62 + 261046197332175753322177412628351625963583855497412020645266395599158648215720043439845300195316283171699713651383107635833267930569497358036246485879149728326618032853091755824027306939800990750987637667718911621792873841152342767246673670834498679904459293165503385455704384808513213606404512951535950815452250090533502331981846660294431415357155453333801042273400145108357450494782724874425796334276827652068971796640767195186177507328 / 71040567554089435824720542878898271699987167652223650356297485768436243834421296541538357393553751478320212704947899165189797461610973047090280871318258884540394906182975012626370286572926067843959313828580418980893287943026340440875507713367211062043227159947913098739242021798255306348367801464792076632856500987471907575256326147708473016087777980617302519851875 * s ^ 63 + -491406860847986269868403880749792624278968299694445812111630217978544655115777555544462047439281253659108770117204768484938731670393571976189069961479517376377100913272874542847832072662243960649106937226416045371187789824 / 65554202432968562395106874238332414499007060898619495255603555822483987101072518927923318502090980652445391437865144651025169476362751266037892433125 * s ^ 64 + 56326268721985462967545147662155582000564125409127070775599723796574878794366638005690790968199168390856419959807494384880151314149723104956453976392639623357099588670762364287152839912688612696145694871673075698096930816 / 3856129554880503670300404366960730264647474170507029132682562107204940417710148172230783441299469450143846555168537920648539380962514780355170143125 * s ^ 65 + -104759611176980373643737577629959876659869206552136556978040286019884302162352435198355444515731296360574872258924782675259627792774491732620283992184606070903115965206491213762534584850023679054476110247514098229982527488 / 3856129554880503670300404366960730264647474170507029132682562107204940417710148172230783441299469450143846555168537920648539380962514780355170143125 * s ^ 66 + 185817015026061087830612107533510221520143723729405407992928588363127939662200430220299133002637187304011097709801894019359285756472220823792361328607527993958211570159993511953563172650329021730382226547432398880845594624 / 3856129554880503670300404366960730264647474170507029132682562107204940417710148172230783441299469450143846555168537920648539380962514780355170143125 * s ^ 67 + -44864083196303263754022981333684417384110317060487334844941064143328010050534017242553669162425000934983550118673695924705073973666126610849375404317827180639768322931112645247210747412456461799628887515183522868505870336 / 550875650697214810042914909565818609235353452929575590383223158172134345387164024604397634471352778591978079309791131521219911566073540050738591875 * s ^ 68 + 26591867887488273139250475636578887658577513432818218560893790325003884596004859076647796939093307309951557032948426994513014332340417122810969875724818257766151408946193452225635634574184804522975000768380903880134754304 / 202954187098973877384231808787406856034077587921422585930661163537102127247902535380567549542077339481255081850975680034133651629606041071324744375 * s ^ 69 + -40680197721611623748787829948480351533322344082823525719935095722053005560220817637481439696030384532317041768656624601855282758367683724659165940524319780990748167573543545914623369495109560059711663975895611801864241152 / 202954187098973877384231808787406856034077587921422585930661163537102127247902535380567549542077339481255081850975680034133651629606041071324744375 * s ^ 70 + 3476858444965576470549248721355610572906104051879906986268950872449220198757467407832604731880330033749658828555695399371865000808767263532811511989641669239537915510060221231829222348489575845179632970098216732456910848 / 11938481594057286904954812281612168002004563995377799172391833149241301602817796198856914678945725851838534226527981178478450095859178886548514375 * s ^ 71 + -3541771874200775310623779062109521105533951619365706264013598648593424030799904466873380847914886533061124405456607898336874221033620398601081718823185132133352940380281127792482682399025351501135556232138837356619759616 / 8824095091259733799314426469017689392785982083540112431767876675526179445560979799155110849655536499185003558738073044962332679548088742231510625 * s ^ 72 + 106342466210133815603714492336360218040918301437645005415162925827315553157582159493864418382942767869097856679317227566365664845657013636774714154125510953697432161196834140490850988227967701523625538899963596915358040064 / 202954187098973877384231808787406856034077587921422585930661163537102127247902535380567549542077339481255081850975680034133651629606041071324744375 * s ^ 73 + -6910064359478912257127423939692735890280598051623483840136891400781887116851556407776843846484733537872403193390201928408651966694781562790925730069620962159612636728276632041985050717426281518803247376835637661753409536 / 10681799320998625125485884673021413475477767785338030838455850712479059328836975546345660502214596814802899044788193686007034296295054793227618125 * s ^ 74 + 153035076276886850885725886015445820531844450248930773234017665937835513488740383737051487016451902327639423448989117054039193032871458807560640204054674670513785165808140407876936836573129069465783150394305298240496467968 / 202954187098973877384231808787406856034077587921422585930661163537102127247902535380567549542077339481255081850975680034133651629606041071324744375 * s ^ 75 + -168093068878707585552621519229583571744840097219885613477979475877029977441226017045245612071507789812390819721790382476045790914743425640955518009535748599240244588193080373336487191630676579598027632576972084677282103296 / 202954187098973877384231808787406856034077587921422585930661163537102127247902535380567549542077339481255081850975680034133651629606041071324744375 * s ^ 76 + 580668933470095813468616893727961400142158205157061214128994039643553815251492426654415594374803362160288081559514646163076948460858452872493362637426992798144738349086648814867049040674477484457387155200996162207219712 / 678776545481517984562648189924437645598921698733854802443682821194321495812383061473470065358118192245000273749082541920179436888314518633193125 * s ^ 77 + -7314719538754477306812857905667654296924987401047459787572184139090791254354609908438105801281732365880637619237773459807661595793238263553161914105492371238933138574947769851978214886996055861627037774676173011002851328 / 8824095091259733799314426469017689392785982083540112431767876675526179445560979799155110849655536499185003558738073044962332679548088742231510625 * s ^ 78 + 265292159757913965630954871989178649871491941762758046152952306142193431507926850490599203009470094016647643895178639273847534682545191516938755184334645448590760881905631503304190838842173042207188541825376248823545856 / 352963803650389351972577058760707575711439283341604497270715067021047177822439191966204433986221459967400142349522921798493307181923549689260425 * s ^ 79 + -151633872303914806489118002406288553055160125723423706035726980075038343760602330951594550375175064065626408490837732293259159451411882124228576781777764896715096831158507547271421643192221752413030088587959852423184384 / 238489056520533345927416931595072686291513029284867903561293964203410255285431886463651644585284770248243339425353325539522504852651047087338125 * s ^ 80 + 51920708396413565775298912660987976748074905627787101665802530303918377925457617211509096351047079259803143314176092901739974689080385521440015696427862615858159944245491922258693721985343979552440457289260616055259136 / 103812883426585103521346193753149286973952730394589558020798549123837405241893879990060127643006311755117688926330271117203913877036338143900125 * s ^ 81 + -1645006816372794611762763131025942501906809063218831682882193149748154232608740916147550225054764167493929394096973938760278234004609835198171017289386909239469729336167463794187385393776301351362522094605791580389376 / 4513603627242830587884617119702142911910988278025632957426023874949452401821473043046092506217665728483377779405663961617561472914623397560875 * s ^ 82 + 34320583674723690131694318481150192495266210112860322434925284665728595065126352479269392960061375098673310870874317752280662653037648575160874303926444256651880542852947174401234317203119504783989017869635953885184 / 140098358200519707856067737858501062043121093649918431876921118925556552283257597827341602757093538131063007997746654679087603072923533257625 * s ^ 83 + -12704170379442740132837672960708108647569728723496742215946877829536515704116187817906280324079879800578822881728919230607617719696094799417184971028494026499153618354364648589282664646616404360815787469193592438784 / 84059014920311824713640642715100637225872656189951059126152671355333931369954558696404961654256122878637804798647992807452561843754119954575 * s ^ 84 + 567626300004856215295343514449546104006850570742544190115422407236152950482669801426363529603285906893116939229852590462399116584478442490499636014158605776514869759516530933592830740323430327883442009773717848064 / 6671350390500938469336558945642907716339099697615163422710529472645550108726552277492457274147311339574428952273650222813695384424930155125 * s ^ 85 + -405467972191147567834299354722572557002445498595965564296811173521952112345084026597216005695215307896276343412354909642670473750609744819788699566368079204438212060050280801395221240421430071680481619278735343616 / 9339890546701313857071182523900070802874739576661228791794741261703770152217173188489440183806235875404200533183110311939173538194902217175 * s ^ 86 + 8085892066527414844962984574605619286450140805883586888633118888096906859037406588536748844668433359618860652986539526004354879021374931432331955117964779206486412511881937055629536801016730868439758727788101632 / 406082197682665819872660109734785687081510416376575164860640924421903050096398834282149573208966777191486979703613491823442327747604444225 * s ^ 87 + -3301052150310905936801840921586699629530471010388207683842148936590122480689488668050356410716990842392303089514746143382333665423166248078733926244279445907889814620037078855638721569907019810348447868567683072 / 406082197682665819872660109734785687081510416376575164860640924421903050096398834282149573208966777191486979703613491823442327747604444225 * s ^ 88 + 26329955324687108575976520030385029253613852202272672868309033058882301857405052790983516636709398188726114694963635436905617424381704843857196800062985413151891934466852589810775229420133780968890599445889024 / 9024048837392573774948002438550793046255787030590559219125353876042290002142196317381101626865928382033043993413633151632051727724543205 * s ^ 89 + -765294582749964483281326178851864460755830475596534491759291967154413054978663596958569589335234239342788850114883104102393075378057600755095986271718620472805318135081646366188315723116931038465019302903808 / 844245733227995467510727878866498309940770096416996184741457223330359771510184686657275619977061906843008273812086261587198186585456225 * s ^ 90 + 33155702666371788330470289175584231173868596619664563634456802284853618563226109409664239693776283777080313811115905845813962915489002634499218349351784532714280299054832144889970530295614485118009288425472 / 138831520575270365768430806746935277634704415855239372601928521169881384648341481805863101951783513569739138360209740794339257349608357 * s ^ 91 + -104993305601857383799079247532572423034805444286996482477312543325768954092309481402545300420810595810982881738505335528461682839168003770674530382331225379620124203766342626421715786285935606409023455232 / 2023783098764874136566046745582146904295982738414568113730736460202352545894190696878470873932704279442261492131337329363546025504495 * s ^ 92 + 984158421734726696556774980949571845028005587017708830857144404935577349606764476027918690620913182842283069538896291171250157454618573835037175960983242747059211111361533796398719722721959687416184832 / 110306309053925286642643259770328362970526311659970898301230352113365155449182807727525108812794782750468090227403258218925200500245 * s ^ 93 + -25125980350267389493567229991624125717568906474346956245282612491494983290273222019866652456203221477150964670266088254589586686554047938180743818508006316876103479201460154294166918833609824215760896 / 22061261810785057328528651954065672594105262331994179660246070422673031089836561545505021762558956550093618045480651643785040100049 * s ^ 94 + 22757563178975709752267689896833999548489763243240957664453430590710637634380982662717315531084326756431143795974829051157134659314767383328627379626428071654320311512926624760270313302449228611584 / 237217868933172659446544644667372823592529702494561071615549144329817538600393134897903459812461898388103419843877974664355269893 * s ^ 95 + -2846426162100540477504821406370358099097596818564993027077417967281494233146639620639655387504859468567430806465702543982189965316310808246859421143193791148489260371756378664313018408226839855104 / 711653606799517978339633934002118470777589107483683214846647432989452615801179404693710379437385695164310259531633923993065809679 * s ^ 96

theorem G67CenteredEvaluation.density1_eq (s : ℝ) : G67Centered.densityPolynomial G67Centered.squareEarly s = D1 s

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

Equations

• G67CenteredEvaluation.H1 s = ⋯ + 4049969890945490983390690863358701647394682044771639609439743632379661396106462872585990920830780489484945543039219414287213717375801651693844256997401295971205451295793605307877689625009042243370950010083057952282106325808675444098725927059250194543152554002725856877612421459775315996906754573044742154298962266902992253768550906690963825016669489173924690227571073360986829234592386861891336108338827352057544188384957643951446823200967071662449551736832 / 1630145428434422660824007595760253609001525653266569488958517523178044701458692216216703336054532500804111268275758557896347757561231333464490749379154001673073085512090266078066750746121372133948508564157292032978882404713149691349568912513258083583531896112613269310573019445456107144230380676202304217834258130262263918682657360495227461605363056369638364862514340851426411162269288311626875 * s ^ 48 + -24749994654686509166092785437654493655056916021687515779348739355910183258726341204586660618271896093028688859466801643202619518342296095270523692863662398367752004100259154750612582563159250213682405300209546301123371573316432206877196065306725777404502610505428952120486383067312076955209475482533620875093666866248808461015615521604908004661993529068742157798687554967671501250150866067076661900794937015066270933116897736857143783463679561055272007892992 / 2539014543726774577788608125097943875451466863994828527507546500914571409054223487539291631526037957652230418359812283869494221066388357731621406860647308742201033919307004601959142799032828975585616857619117269791857806287028832540557529382795141913293007662735914787146112048056146483525918432099560351523934599284909788694405812377659226702352827726499462389124410202553154084629183885676875 * s ^ 49 + 4746518480983363253818385571960960543015041125213621519764027206248821172667827769599743712945083863879092388906196291686842527922400353714254259044632967350959689470103601682570629130127756105509274210987065558545700478161227490591025666838749766885057969368575281741074411605566731344948042583346895161794907233578613660271994728599093895657451724293045830957744432949997061818026698974667882356480265918883456223819859056601288677016686876180988509028352 / 129192389732508195415284807509521870553529173727664689363797816895647645820735833982828800217920958844178070134926363528207390642302064519596776574404464524260738015037074605688553115633718400484993431613272648361156745190357097205567727305081990553374554820838919697349147568317945733938141512167451087802389543117803044971798524476007194273594607274713240701355414458295927582830848511703125 * s ^ 50 + -4629955851110258148193396451639534291540653213220413152262545322000566733936786424039708280234301936207820022382904471461251504559028716621962296316178417461259013273052575104858780933404378999695873026123567678465465057552530164898503486659487161978878045049453190786136665723099457501830157608639991220550202939361741348432780952460537656804908411563956661998632173610983719112742450126047900480709658232783608742720996678519249588540238300261136073752576 / 34808817460004094915665416061056081349139558506246259700283638212638648723020900174996137115319080986695525311825442852505689403246669459242301310990485913329119601032630667344010160212254693564635966102594970162213553232420742416896361243708883492494125336633580627889543910860005001521446430070777387430530616523060895890514772255044957249564735695903869381421798461593695205336311636738125 * s ^ 51 + 77429648154035215455395564547708852869491338399235619172252817083384315663986773331381731591200006004663974910746016920352578709893474728546547769214372776678930697922801418388326930066969872495531235864438451533045564247827286381942821210678184021052456237864876730421569907039956442818813620222134287979686893140708926353238763963615183979094847238208814354274297558519052810806189564831067093218652755899926865505092561519707533471548555796919072325632 / 167411996662986767999870665480476898830489922523566916797516572979764126303837107759877832963058843073267417333973643019820185809177470577191978188263528255005014729346725370133974133466263787029325771118658754017305287466322475552960671908329813319431605392614335243271946297143938224113504843107697386828301152349164501138250846953601348222101947483074473532550270070557912567285257594375 * s ^ 52 + -19889738387575918004232746533059684231968802615447270843668123116885352268735861792949950051980751559951346521631112589492922485067091696168398015100096285582970304527124632485206460621455599720247956019177704635271799677971143671849215916231823566864831935817271797732834834855491315333227094263498713678352070150616805803563644161102455411193280433103447909504464659968354335062546989525442746122795281705542858773805937954566347031978041259817600811008 / 12877845897152828307682358883113607602345378655658993599808967152289548177218239058452140997158372544097493641074895616909245062244420813630152168327963711923462671488209643856459548728174137463794290086050673385946560574332498119458513223717677947648585030201102711020918945934149094162577295623669029756023165565320346241403911304123180632469380575621113348657713082350608659021942891875 * s ^ 53 + 236047650599649469441668350246121786278794226010136885360898047273322697154297837291093923892186690921093929824756749877696190360523375910646465276700562225151348830227362549263070284970300859562620025430979620535212588270981105970795767645917486873475723881701174186304770279460678787711262622506064221074642481047743500011002138179006575164148789626626173069024794251818765170357357411968821175174335324779677190044066143318916591460818035861880832 / 47663211258372904780788590971353479343011307060737966705955198615788955049578998383984122617489613558628980300409909900495809467779985199124672366142413443056402282802370945598346671832877477616770594260371927547991902849671609370641927946872086378731188698769655925740206514845500530624251382676682121155571853420656848012721308935800842179494464961250721615249056195748282247733125 * s ^ 54 + -54491755625037667288764487632108647160937386443951818550577437474885930518727127925711875230357982799174132150716988416150118369083495995022229439929835681383010901473318007252155506436837595209607213465721450658848168282457428344448089575100852523829373536293701678486950838449233527762319937490212949634386233097754373232239081590963937485444588481782657754160477664822790716397676931677815402093304692037888844971604911286544599250344047837970432 / 3574376112121628916832936880312703531998093122093909348931442810183132533561938966659354160172927860992990564309895294037794098440800849031388040925892651836185662469109544435749903458541469854946065379183079966102851606418593295319030409238953523963618375022517815061631648649264655648283314587017789924430702200202304182160000210979861136815471048517424792083262555236709259471875 * s ^ 55 + 514598834251589048912390919034980335395137367972341153774136878305570515916722771073163500093972752129265748400254506461997954315243462011511253078001119314194549376209663717141796929923852978454862613706899894342507011621656883425056801401083039183107868798338834609507238104600348913135386822107328427699460527239041732454102689655746143226211925473539580841158100791677906761084388527922750041847241072685604417820948004148613324896015048048115712 / 11424515347045357330405651085376829779631641035522797051112951170660804739347027565133860277986678861362501916869740807735892835393804977847493096846155004170751909854097298630491200865602358366563461796860636721845718153345466117491391534435447678479942504317255054178120778890291182392814971529071954966010584013476798650149132749811103331632845200355693580734050506737708463293125 * s ^ 56 + -74717413745747867061074993010447293389271441020439296488952924712847500322977946613069770086489813023113436371201005864258494841369921754349132930014907521925643639360928914353255158495076211153034054429208118207121548545480799769782382361822651289780801476982300184783398735470635269387279762156642205592801946252635487453593131800823188862412832052730911585280280507052176934385870009579305469130812331917276490663430584825909601258225708568674304 / 585082996209870051961475392512560015668466791576639202078560841624138248106721088241356725826811046808322200594407211177848959225019661938281317628239744148906432041045414215577716486378557436562549256442997567965144595454350016798750509849793816418110263024333816790793247436430006645454136008227404701763345272927383219279874723036148149059364039910399401708751912743979678713125 * s ^ 57 + 5852029382889459229266300470459728743336888748573242678491692994982650732456172564120036330776484841141498714025212978000592061625207473433260294723287297231981301961709567031537377651874335627408557868855015882598172396630977834611726372064203379182888502058315600835141266013141816618912681096014281562429735529822297791521631406327194164090865525365369221771469388605734969848161008060735072950734413222058799846835905590223109899155461474615296 / 16849460665428233869794226795297160332061109191382856862242566442005967423132980694140362511397736204013251059819075594992671119687755904876026029015841688498794964439242316039477436052609896385614626054465669782511611984286147454978912398852056282150146601495214187619666510085869108955481573226012647816422058505356617039837504436989370727628160037141591508990869383888193329375 * s ^ 58 + -21698632733568083212142596423811346296208569008756719845133216438641237887289952114711598729543441777385937495162273835852148641982439873430787741865204163709769906593804787364585529333769558057200291854348216915945173209400256865541969798814566416418617484500263801282193439777701183511004441763292609440444993023102227747832720003241034130003191244538209644639299229276292821588648139632352921099948194538884436049677652191216931181224406286336 / 23955232156443909451260497383612435470531951186572894644986901373005423696109445069863885591760438469283158932247173669355107257080353704611810783679959989913706424297339614119115369698161013199143664599471662381459435337547475839026382118419029871728442841712273478145505291574888007623639432765482209719966781171017142710677673239894283547315873688314270200015935170712629375 * s ^ 59 + 780653344448711046013933598028426019765150821854197481798298491356029778842690857172901718616995640596515424853012040794418873764147822529919377325949341670909756661445724085797591872686582528154943397596829584463111653725982086758029486862657148079064644297576492687802628941952197156176551026630060605814985832372445446203950209420275383230124721397819731207429368127938537839491845699140166660296475409419001870484985992504940270772543291392 / 344734712836576886890541215945813749975675664661266472345510253209224197737424057609170083667802920088820643412575252677000264332784111515040449397377102509151515539936131319270927929778460375427395237280532397558578378698316729375179787441271616318445771626815576116580664573351442386652949943858874140517590391012398919725134408632952593421558783490291704189548155638653125 * s ^ 60 + -47828406273579604121258723919790578221057194534771663203682667829573018672389077537414299062180372029552242986748773182976694047984818923993043458713645989234215739827225520964446768892843685801933611755028457014599145083264979963838855665250881175468332738924439178646011269115292485252855331530127151754744441959359443892115971981285353472295667595407250303213983397220033764743907683966677363277761764176048580486685397877523919077665406976 / 8817114248650394172043192525238842242564450961986270361876782157552484722005395184133909896744644916317844548497731829474639884402444780887827007647800106104084883830651576719298366338149301006738410680969591719527581174254641715675457875856422891163602544752935070486968779444208798987769369633287766277389104340359049938462557201932959412459155468724441910089072324510625 * s ^ 61 + 59554370410569991004447817739127818117652329797562536676094359224553904848551409965280926084500454696295929882049584975184279619076036881987156777764273765733676547143711377011434213163188658269842488244465284703951675131926841551540796311752471451363250547402304324174776931361903853381345645260987187174824520765761251881505776562992331753611649135344978193518473434162567094055548869690064969996268656073573053081208635130579803457978368 / 4785505752146126665460649929951224276526235574556741758951267533819170693418121798927648369101961360834084488443405331464680326406499977371142590334611873239294622065203745775550181614412018708172631257434662763809914555706083371118696826095555438772417911175571270070371560314395872201545100210072788658219112476019070109991991898288085867782720988108323349644781855625 * s ^ 62 + -88595453460014694932682409899887323180842704027956949995051247728022007221276864808506097476580863960248103224294280185746967733971653152315802338360272842539538498874149364042167907422645389077418694948541708856138520734896518999941984463077362817927045609597335572690813588442638952906360859375974295320288378617473186147395795294815555065130592941641177958654812203183265373376727445207799627120352295078866572766919680133594453351858176 / 3241794219195763224989472533192764832485514421473921836708923168071051114896147025080019862940038341210186266364887482605106027565693533057870787000866107678231840753847698751179155287182335253923395367939610259355103408704120993338472043484085942394218584989903118434767831180719784394595067884242856832987140709561305558381671931098380749143133572589509365888400611875 * s ^ 63 + 4078846833315246145659022072317994155680997742147062822582287431236853878370625678747582815551816924557808025802861056809894811415148396219316351341861714505103406763329558684750426670934390480484181838558107994090513653768005355738229276106789041873507176455710990397745381012633018962600070514867749231491441407664585973937216354067100490864955553958340641285521877267318085163980980076162903067723075432063577684322511987424784023552 / 71040567554089435824720542878898271699987167652223650356297485768436243834421296541538357393553751478320212704947899165189797461610973047090280871318258884540394906182975012626370286572926067843959313828580418980893287943026340440875507713367211062043227159947913098739242021798255306348367801464792076632856500987471907575256326147708473016087777980617302519851875 * s ^ 64 + -491406860847986269868403880749792624278968299694445812111630217978544655115777555544462047439281253659108770117204768484938731670393571976189069961479517376377100913272874542847832072662243960649106937226416045371187789824 / 4261023158142956555681946825491606942435458958410267191614231128461459161569713730315015702635913742408950443461234402316636015963578832292463008153125 * s ^ 65 + 2560284941908430134888415802825253727298369336778503217072714718026130854289392636622308680372689472311655452718522472040006877915896504770747908017847255607140890394125562013052401814213118758915713403257867077186224128 / 11568388664641511010901213100882190793942422511521087398047686321614821253130444516692350323898408350431539665505613761945618142887544341065510429375 * s ^ 66 + -104759611176980373643737577629959876659869206552136556978040286019884302162352435198355444515731296360574872258924782675259627792774491732620283992184606070903115965206491213762534584850023679054476110247514098229982527488 / 258360680176993745910127092586368927731380769423970951889731661182731007986579927539462490567064453159637719196292040683452138524488490283796399589375 * s ^ 67 + 46454253756515271957653026883377555380035930932351351998232147090781984915550107555074783250659296826002774427450473504839821439118055205948090332151881998489552892539998377988390793162582255432595556636858099720211398656 / 65554202432968562395106874238332414499007060898619495255603555822483987101072518927923318502090980652445391437865144651025169476362751266037892433125 * s ^ 68 + -44864083196303263754022981333684417384110317060487334844941064143328010050534017242553669162425000934983550118673695924705073973666126610849375404317827180639768322931112645247210747412456461799628887515183522868505870336 / 38010419898107821892961128760041484037239388252140715736442397913877269831714317697703436778523341722846487472375588074964173898059074263500962839375 * s ^ 69 + 13295933943744136569625237818289443829288756716409109280446895162501942298002429538323898469546653654975778516474213497256507166170208561405484937862409128883075704473096726112817817287092402261487500384190451940067377152 / 7103396548464085708448113307559239961192715577249790507573140723798574453676588738319864233972706881843927864784148801194677807036211437496366053125 * s ^ 70 + -40680197721611623748787829948480351533322344082823525719935095722053005560220817637481439696030384532317041768656624601855282758367683724659165940524319780990748167573543545914623369495109560059711663975895611801864241152 / 14409747284027145294280458423905886778419508742421003601076942611134251034601080012020296017487491103169110811419273282423489265702028916064056850625 * s ^ 71 + 434607305620697058818656090169451321613263006484988373283618859056152524844683425979075591485041254218707353569461924921483125101095907941601438998705208654942239438757527653978652793561196980647454121262277091557113856 / 107446334346515582144593310534509512018041075958400192551526498343171714425360165789712232110511532666546808038751830606306050862732609978936629375 * s ^ 72 + -3541771874200775310623779062109521105533951619365706264013598648593424030799904466873380847914886533061124405456607898336874221033620398601081718823185132133352940380281127792482682399025351501135556232138837356619759616 / 644158941661960567349953132238291325673376692098428207519054997313411099525951525338323092024854164440505259787879332282250285607010478182900275625 * s ^ 73 + 53171233105066907801857246168180109020459150718822502707581462913657776578791079746932209191471383934548928339658613783182832422828506818387357077062755476848716080598417070245425494113983850761812769449981798457679020032 / 7509304922662033463216576925134053673260870753092635679434463050872778708172393809080999333056861560806438028486100161262945110295423519639015541875 * s ^ 74 + -6910064359478912257127423939692735890280598051623483840136891400781887116851556407776843846484733537872403193390201928408651966694781562790925730069620962159612636728276632041985050717426281518803247376835637661753409536 / 801134949074896884411441350476606010660832583900352312884188803435929449662773165975924537666094761110217428359114526450527572222129109492071359375 * s ^ 75 + 38258769069221712721431471503861455132961112562232693308504416484458878372185095934262871754112975581909855862247279263509798258217864701890160051013668667628446291452035101969234209143282267366445787598576324560124116992 / 3856129554880503670300404366960730264647474170507029132682562107204940417710148172230783441299469450143846555168537920648539380962514780355170143125 * s ^ 76 + -15281188079882507777511047202689415613167281565444146679816315988820907040111456095022328370137071801126438156526398406913253719522129603723228909957795327203658598926643670303317017420970598145275239325179280425207463936 / 1420679309692817141689622661511847992238543115449958101514628144759714890735317747663972846794541376368785572956829760238935561407242287499273210625 * s ^ 77 + 290334466735047906734308446863980700071079102578530607064497019821776907625746213327207797187401681080144040779757323081538474230429226436246681318713496399072369174543324407433524520337238742228693577600498081103609856 / 26472285273779201397943279407053068178357946250620337295303630026578538336682939397465332548966609497555010676214219134886998038644266226694531875 * s ^ 78 + -7314719538754477306812857905667654296924987401047459787572184139090791254354609908438105801281732365880637619237773459807661595793238263553161914105492371238933138574947769851978214886996055861627037774676173011002851328 / 697103512209518970145839691052397462030092584599668882109662257366568176199317404133253757122787383435615281140307770552024281684299010636289339375 * s ^ 79 + 16580759984869622851934679499323665616968246360172377884559519133887089469245428155662450188091880876040477743448664954615470917659074469808672199020915340536922555119101968956511927427635815137949283864086015551471616 / 1764819018251946759862885293803537878557196416708022486353575335105235889112195959831022169931107299837000711747614608992466535909617748446302125 * s ^ 80 + -151633872303914806489118002406288553055160125723423706035726980075038343760602330951594550375175064065626408490837732293259159451411882124228576781777764896715096831158507547271421643192221752413030088587959852423184384 / 19317613578163201020120771459200887589612555372074300188464811100476230678119982803555783211408066390107710493453619368701322893064734814074388125 * s ^ 81 + 25960354198206782887649456330493988374037452813893550832901265151959188962728808605754548175523539629901571657088046450869987344540192760720007848213931307929079972122745961129346860992671989776220228644630308027629568 / 4256328220489989244375193943879120765932061946178171878852740514077333614917649079592465233363258781959825245979541115805360468958489863899905125 * s ^ 82 + -19819359233407163997141724470192078336226615219503996179303531924676557019382420676476508735599568283059390290324987213979255831380841387929771292643215773969514811279126069809486571009353028329668940898864958799872 / 4513603627242830587884617119702142911910988278025632957426023874949452401821473043046092506217665728483377779405663961617561472914623397560875 * s ^ 83 + 8580145918680922532923579620287548123816552528215080608731321166432148766281588119817348240015343774668327717718579438070165663259412143790218575981611064162970135713236793600308579300779876195997254467408988471296 / 2942065522210913864977422495028522302905542966648287069415343497436687597948409554374173657898964300752323167952679748260839664531394198410125 * s ^ 84 + -747304139967220007813980762394594626327631101382161306820404578208030335536246342229781195534110576504636640101701131212212807040946752906893233589911413323479624609080273446428392038036259080047987498187858378752 / 420295074601559123568203213575503186129363280949755295630763356776669656849772793482024808271280614393189023993239964037262809218770599772875 * s ^ 85 + 283813150002428107647671757224773052003425285371272095057711203618076475241334900713181764801642953446558469614926295231199558292239221245249818007079302888257434879758265466796415370161715163941721004886858924032 / 286868066791540354181472034662645031802581286997452027176552767323758654675241747932175662788334387601700444947766959580988901530271996670375 * s ^ 86 + -405467972191147567834299354722572557002445498595965564296811173521952112345084026597216005695215307896276343412354909642670473750609744819788699566368079204438212060050280801395221240421430071680481619278735343616 / 812570477563014305565192879579306159850102343169526904886142489768228003242894067398581295991142521160165446386930597138708097822956492894225 * s ^ 87 + 91885137119629714147306642893245673709660690975949851007194532819283032489061438506099418689414015450214325602119767340958578170697442402640135853613236127346436505816840193813972009102462850777724530997592064 / 406082197682665819872660109734785687081510416376575164860640924421903050096398834282149573208966777191486979703613491823442327747604444225 * s ^ 88 + -3301052150310905936801840921586699629530471010388207683842148936590122480689488668050356410716990842392303089514746143382333665423166248078733926244279445907889814620037078855638721569907019810348447868567683072 / 36141315593757257968666749766395926150254427057515189672597042273549371458579496251111312015598043170042341193621600772286367169536795536025 * s ^ 89 + 13164977662343554287988260015192514626806926101136336434154516529441150928702526395491758318354699094363057347481817718452808712190852421928598400031492706575945967233426294905387614710066890484445299722944512 / 406082197682665819872660109734785687081510416376575164860640924421903050096398834282149573208966777191486979703613491823442327747604444225 * s ^ 90 + -765294582749964483281326178851864460755830475596534491759291967154413054978663596958569589335234239342788850114883104102393075378057600755095986271718620472805318135081646366188315723116931038465019302903808 / 76826361723747587543476236976851346204610078773946652811472607323062739207426806485812081417912633522713752916899849804435034979276516475 * s ^ 91 + 8288925666592947082617572293896057793467149154916140908614200571213404640806527352416059923444070944270078452778976461453490728872250658624804587337946133178570074763708036222492632573903621279502322106368 / 3193124973231218412673908555179511385598201564670505569844355986907271846911854081534851344891020812104000182284824038269802919040992211 * s ^ 92 + -104993305601857383799079247532572423034805444286996482477312543325768954092309481402545300420810595810982881738505335528461682839168003770674530382331225379620124203766342626421715786285935606409023455232 / 188211828185133294700642347339139662099526394672554834576958490798818786768159734809697791275741497988130318768214371630809780371918035 * s ^ 93 + 492079210867363348278387490474785922514002793508854415428572202467788674803382238013959345310456591421141534769448145585625078727309286917518587980491621373529605555680766898199359861360979843708092416 / 5184396525534488472204233209205433059614736648018632220157826549328162306111591963193680114201354789272000240687953136289484423511515 * s ^ 94 + -25125980350267389493567229991624125717568906474346956245282612491494983290273222019866652456203221477150964670266088254589586686554047938180743818508006316876103479201460154294166918833609824215760896 / 2095819872024580446210221935636238896439999921539447067723376690153937953534473346822977067443100872258893714320661906159578809504655 * s ^ 95 + 711173849342990929758365309276062485890305101351279927014169705959707426074405708209916110346385211138473243624213407848660458103586480729019605613325877239197509734778957023758447290701538394112 / 711653606799517978339633934002118470777589107483683214846647432989452615801179404693710379437385695164310259531633923993065809679 * s ^ 96 + -2846426162100540477504821406370358099097596818564993027077417967281494233146639620639655387504859468567430806465702543982189965316310808246859421143193791148489260371756378664313018408226839855104 / 69030399859553243898944491598205491665426143425917271840124800999976903732714402255289906805426412430938095174568490627327383538863 * s ^ 97

theorem G67CenteredEvaluation.primitive1_deriv (s : ℝ) : HasDerivAt H1 (D1 s) s

theorem G67CenteredEvaluation.integral1_eq : ∫ (s : ℝ) in 2 * G67Centered.a..G67Centered.a + G67Centered.b, G67Centered.densityPolynomial G67Centered.squareEarly s = H1 (G67Centered.a + G67Centered.b) - H1 (2 * G67Centered.a)

theorem G67CenteredEvaluation.endpoint1_eq : H1 (G67Centered.a + G67Centered.b) - H1 (2 * G67Centered.a) = 114466281151814146487692621662954901524065993453769609422388759107467769666108253802863716408782444895632071472474569100456792975925861120895056961767707329282357176390729399105502417706896619784135210114353582251532159167028476501650073006788640419296936853582098563566070923318476459128292506510052777700801093204320305637578784317855131024386321548655957599720300062521198092106729561858149240503076296191494164467089791522585727884800340811412842074240953267830589856053923918901185347176204531244569481056781462723097606647762598302389037821912132954136977603030584813294273812582148029819322680 / 240367563736902935460880507609450993578784762827118940469472358637576246954739901910887493721930067887440466804686531357531491086834212929688911936670343107568623769139152933547611352891419180909171775426677664692710145274202899972121053822138551384685698913364020202493244566201043460545755493360378742310330645585507274271959841803376951168563417907365366047531533851282655724161094054422037516042336580331912032770089359596841916032734859103251441700173796035098469977325349223615600756180148874912274841204694216016225694226373891158941274399133719693927061989564819767314202556352991345689892607