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

Equations

• G67CenteredEvaluation.W2 s = 125252311396607272375629666084019813193602129800475700238847738951835234105078312290613069013276929743325890563556467524039373368348350110299046955655668705307307277580581321215790114730263438479898738122268034741164118463077579508875426341203823996358510359922193525057112837291547336296283971873229220529447822211749696717942619 / 21601573351781194880354606826286930847002901417156487568365181443017431351582152055400792376580740233118523541550480147029355369989190007817199242219701552443367291266272168340981724775182410968852095264947427447805271541588147151194815119221286242953276199331981666181667926638105447714593178112292364343571603015964624400 * s ^ 0 + -16057328344514779970146237202973629071981730055997644311709946532834350430798873341384158000907834012 / 26016531848676609019733212304201985278528371719929018837564202498970513101376639717306762443 * s ^ 1 + 276979206710124490949583863733316516371426300564929518827715525073511513482032575207624997540944431168 / 8672177282892203006577737434733995092842790573309672945854734166323504367125546572435587481 * s ^ 2 + -9278602101869873168024390082553753278795111596139309089107476295022497039395098516951747654208536637184 / 8672177282892203006577737434733995092842790573309672945854734166323504367125546572435587481 * s ^ 3 + 25118915944104613431708927589925682925081084768075421311853741354938448855014430034418143889083207460544 / 963575253654689222953081937192666121426976730367741438428303796258167151902838508048398609 * s ^ 4 + -27251467775453542336221794368230778375840835830199700723661355614030230740228616669973516895137218548224 / 55377888141074093273165628574291156403849237377456404507373781394147537465680374025770035 * s ^ 5 + 11845986887604392206803929584815162921337612281489545496639692788666531287345917710880863963687537808384 / 1582225375459259807804732244979747325824263925070182985924965182689929641876582115022001 * s ^ 6 + -12893138261256989738663206143921959641725241598124585131320415904081391512645231282717354153881663574016 / 136735526274257020427569453269854707169998116981373838289811805911475401149828084014247 * s ^ 7 + 45670794150756642959649484164059281814955411203609468590451486289546378565043162719928535646347013788416 / 45578508758085673475856484423284902389999372327124612763270601970491800383276028004749 * s ^ 8 + -1246048756867507405998088880630456021950754384782370123124827749522360456146353200389170180739461949509632 / 136735526274257020427569453269854707169998116981373838289811805911475401149828084014247 * s ^ 9 + 5445883268300376095928665081627992734524999331098125193730812712320440574096256914744218128450631973715968 / 75964181263476122459760807372141503983332287211874354605451003284153000638793380007915 * s ^ 10 + -2491068567035442059796842421625039259258858478152742352780891793623100419108833416005091864227408396353536 / 5064278750898408163984053824809433598888819147458290307030066885610200042586225333861 * s ^ 11 + 15001885824184650504572243209376917811934694641301687781783378942595848747894433622591641493925713477156864 / 5064278750898408163984053824809433598888819147458290307030066885610200042586225333861 * s ^ 12 + -16442150767224559722473045920407439805555964079575998968040629180131533190121207836888586548922806863003648 / 1045009900979036605266550789246391060088169030427901174466521738300517469105094116511 * s ^ 13 + 13874471261200624285814536042830254095138735289030549754594730642376249236239155443808132866747912177844224 / 187565879662904006073483474992941985144030338794751492852965440207785186762452790143 * s ^ 14 + -289424564248474963879289634332318937437630419496038091163854945042117254288948986119522592417011880716926976 / 937829398314520030367417374964709925720151693973757464264827201038925933812263950715 * s ^ 15 + 7950290727348167173087969964142107954470019162232726324587175214596749871616684101374399543104648931295232 / 6946884431959407632351239814553406857186308844250055290850571859547599509720473709 * s ^ 16 + -148614750357870331710725297657013768961283812931177043019493878053423017516783675354375737460714996964524032 / 39365678447769976583323692282469305524055750117416979981486573870769730555082684351 * s ^ 17 + 76955064043575523047225565725683880410561373374975333281569731335770308241620958778882588502956663893917696 / 6946884431959407632351239814553406857186308844250055290850571859547599509720473709 * s ^ 18 + -423671340337162213384077774973158752939930740730813849914125850393329157606740933026552807111160390616088576 / 14665644911914305001630395164057192254059985337861227836240096147933821187187666719 * s ^ 19 + 12284000280806927474043683124889939144205842185162315307870999243608394932444457895882899195496719840182272 / 183780011427497556411408460702471080877944678419313632033083911628243373273028405 * s ^ 20 + -35209994390203682140662133459012244871811268955909002080119581659275402269777126081825037110573129372008448 / 257292015998496578975971844983459513229122549787039084846317476279540722582239767 * s ^ 21 + 7061575742094217727015271608908101642493969038205789734124696487162347427263177396465029789253521740136448 / 28588001777610730997330204998162168136569172198559898316257497364393413620248863 * s ^ 22 + -85728713201214614431862786238532330926656964775935318788047141813110037950817586246801444270957771207213056 / 219174680295015604312864904985909955713696986855625887091307479793682837755241283 * s ^ 23 + 5144735796081461184183186488862723038946068305133463996007316341697639525184243750077897955422638589345792 / 9529333925870243665776734999387389378856390732853299438752499121464471206749621 * s ^ 24 + -5683685153994439417236172541117997007664091478220138914811223543035869654432359858939270966328485417582592 / 8823457338768744134978458332766101276718880308197499480326388075430065932175575 * s ^ 25 + 1005124199400193219199153251285348011529843403551723184753503083355726920289906866576187311485277396008960 / 1529399272053248983396266111012790887964605920087566576589907266407878094910433 * s ^ 26 + -85494861988863240968064753008510307269571691364674287250918257283363003638834107318850014606097419075584 / 151259268664607042313916428561704593315180805283385705377023795578801130265867 * s ^ 27 + 47288904972993956876791363553356343233475618853042377835508795281447431080175135479744854386796346212352 / 117646097850249921799712777770214683689585070775966659737685174339067545762341 * s ^ 28 + -261671443168023385855290941980548048050254804624608013425896648620806363074187730603542360382335543672832 / 1137245612552415910730556851778741942332655684167677710797623351944319609035963 * s ^ 29 + 579407275841714885485306217317413844921803881605719914018571887094265625235706419159021634258612208533504 / 5686228062762079553652784258893709711663278420838388553988116759721598045179815 * s ^ 30 + -128343914499173709508964350367957476999619219318253424939842378449067932552278541893059259980845808615424 / 3917179332124988136960806933904555579145814023244223226080702656697100875568317 * s ^ 31 + 286689805293756776183191363449521565172430452096457021524859907006813833653919481094045331096223088640 / 42120207872311700397428031547360812678987247561765841140652716738678504038369 * s ^ 32 + -28886137518384761170752565121662769911328801233066455280330456098830017043044553092856134355514294272 / 42120207872311700397428031547360812678987247561765841140652716738678504038369 * s ^ 33

theorem G67CenteredEvaluation.weight2_eq (s : ℝ) : G67Centered.squareLate s = W2 s

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

Equations

• G67CenteredEvaluation.D2 s = ⋯ + -47301272086090821752712108057542849883836012527353926934093253928276103306413185056192388506716043909643338320708561264607879723214741137277088097274814951857309846622988926875425046221873498091017313806805844016640505244677459848058305962549314399852297312745588117678400535619437790239986483606213820776642682042496339964769549235228006917367438004948184761985452218537114176168682077201045696788080838010622051531303988138169193480566417476740089361548355589078238305761229420727469611442390833418702233828175354157652976336896 / 23185968630136086077641061020878567483574898854478607047247447558531455116613205912869311420253962004908009460768218989796318689471807521781086155883238545907947590288680051854605799454074482088589676315509531904358862816005267411346639388760322051057554895883567395839875097235266815977014707634941862207241367216509496841429090914646735042909147348298434418762538574172949505471024676955113573179543663236644961496112712259383606952859076605599599794302347333125 * s ^ 47 + 37225997636942664802803239682207392647082072375988256740762135656230332988470143306433424075976493030946457438041680421823433020721424054240736166376149122691780636821063314640342046395734321109207474709539813250994996720003468379031646191159039345646258968568776419347980493164391425535966570397509782080320961696237895225976051623277550963946092628035475321816345414134013934094657502093325635314310649486825736697990271529351647033328515448344262596499835980101267305394123651653837349170611745310638270461358864347069463658496 / 4812182168518810318000974928861589477723092215080465613579658927242377477032929529086083502316860038754492529593403941278481237437544957350791466315389132169574028173122274913220071584807911376877102631520846244300896056152036632543642137289878161540247242541872478381860869237508207089569090263855858193955755460030272929353207548322907273056615487382693935969583477658536689814740970688797156697641137652888576914287544053834333518517921559652747127119355106875 * s ^ 48 + -2556973562351267323309783474307806468303639800876418526386161481707856431813794464551299612144029933001680223864107559794896705162941581863817616893456168544815036024239292641788220385057852884350312738791867856584457655246048385671248104650804709373319353571896062322021807865632719549332475012841153522726395094446466350046269263312612847764274146912713909879761861571709744135460952499257053518883378264396383105415455678766175509390470318613798588956088717375227822195124946574215670191353333654635905133988158998959957737472 / 90795889972053024867942923186067725994775324812838973841125640136648631642130745831812896270129434693480991124403847948650589385614055799071537100290360984331585437228722168173963614807696441073152879840015966873601812380227106274408342213016569085665042312110801478903035268632230322444699816299167135735014253962835338289683161289111457982200292214767810112633650521859182826693225862052776541464927125526199564420519699128949689028640029427410323153195379375 * s ^ 49 + 168612685600090469962943077910208679777940786525998079584815137399562808708489623384090424977995674977430672332153649515971620963421048177991260300516151025476752456601499197991433034421435233452295304936574484157432661716740692608239467318879739961489175256777812634866044346545636141987818873973502608553064926569386894571508476319161148456197778201963513172550553919255712295237082848095431402755764237760076615637057537437623541238680120236469421006314569793474986000824478789461015911041113870170104517814260705872863821824 / 1713129999472698582414017418605051433863685373827150449832559247861294936643976336449299929625083673461905492913280149974539422370076524510783718873403037440218593155258908833471011600145215869304771317736150318369845516608058608951100796472010737465378156832279273186849722049664723064994336156588059164811589697411987514899682288473801094003779098391845473823276424940739298616853318151939180027640134443890557819255088662810371491106415649573779682135761875 * s ^ 50 + -10673542709060737825376658647498023187046908639723294004258723901074858355731602953592768959949003408148251139759172482103870698760614922123983742904717897146209948463276568522836222534395795309752575890545711567183107783594427803703043573233348183919752967863802493251240206612583407998137684297407666242986966420326896031674391641845723896338355552722208384202797281018368762886046090754813732618690372735162426116846922435759714829367990843188877084287377418155200428867711202986486021971800829423519009498618030166871375872 / 32323207537220727970075800351038706299314818374097178298727532978514998804603327102816979804246861763432179111571323584425272120190123103977051299498170517739973455759602053461717200002739922062354175806342458837166896539774690734926430122113410140856191638344891946921692868861598548396119550124303003109652635800226179526409099782524548943467530158336707053269366508315835822959496568904512830710191215922463355080284691751139084737856899048561880795014375 * s ^ 51 + 648539615576641480370015026314731857319170278407546777701755386799533708994515435177574950543668895799904740937565164720554776699239026358765006338028113646948185851822527594082730068770483446627111286576328184686934662255195749906158236299430894600641053768874402255408257623586983598951012573313001605154744305075931787106977044905338489220547513503286103360280470972696706563495735436509491890733537173566793385234855874702236570325473293915366248931300709821922973011667123908363890795446453522148666247263908847935291392 / 609871840324919395661807553793183137722921101398059967900519490160660354803836360430509052910318146479852436067383463857080606041323077433529269801852273919622140674709472706824852830240375887968946713327216204474847104524050768583517549473837927185965879968771546168333827714369783932002255662722698171880238411325022255215266033632538659310708116195032208552252198270110109867160312620839864730380966338159685944911031919832812919582205642425695864056875 * s ^ 52 + -49308143465348034731379196609938909800286870183739968978933918283839206556291939373088029707196619970572792730572088990280958954190942906986209956732495989206823642647325881988347093594052376169119831311649416187970011175667285222269008223524558939036777427448398268994326931922601019015627468998027800193696411239079792120048941651973165732957659947371872077646866878595393382569236624130423224181826655342456432637644774948979805203164403234056321672884772183416662468386459611969807548033294617435818050755123715506176 / 15002628233620806269508930992919808558778900922438807603761764536190016353935607006728224469516571461461032596181728957641401344156923013788818720372248503594552180136023042651468668181357799020170394660087481352853487110379837361529053392876877006370467638404259333554742262536463652357931063509451137041653056783966501567372660786512967929711645868368114155918727664020813998847760513169168402508695144969611717913729844772153524380266306915591150625 * s ^ 53 + 17489614265237540908353967944990444472126783915831406606914523437143867805304272934281258253491520029133164806613193904059999656171168308470498855272286960086084261864150379837301295378820102063753924660506254381184568170665530394122974732011167145607026552661503421489129470414957447746448441034921132609221711026177142777884772763643752590476702392915578636509756201865068178722516114759714188805430033594318022006545902577549333394217972314384553323332497797642190640529509263249433268923013812869774249831822312603648 / 1794326501666483456839755195940978195007549821847897307357753531772609160060597313918688315627508234982163106388801826058156062836170271569627936773041416225950650579187536833568761655247377490795367644516934071049216375122615820410538586049674826740394305107760316363088619267966259372919558040191645425065943326571387291778392456456486262605462713400646118445293017044123551710000360767308929475155025135146138724439543262161508373563738874825886875 * s ^ 54 + -113605629288680014281741200850313286795273491552191922711874490543019373422265214016201830010845399074373461947822830518617099053460043081278994894131206404626827398337115049922920814344884958751268425505996520343668230367459138234147440061221677217056399771253852780504292655024066278510895787558598182478578815964307369568718600935031964040279597832230379783889100953238781201945165117591398725568541028409958882692536578527188252844332970159537450611588234446320316056776603617554521725586354645506216033775110747848704 / 4096481258521594307124724126582233237658745819690482531892229761216711478628910848757760116809971630808334639114056999113903464210879299243867553764868138930943938114748904846449436986508163705400744999746207973527456252638424797541040922868125547841277564491301854338372130781583346870250311752135643328924134764436563439720480891155374297646433741914682647771329340798848108620944219864988310688561472478352505389758202541915896475494573657621364375 * s ^ 55 + 1949789386561138417999091293992708724312585951580695600475489691485229689650643421929354345738711724196190130194488895333807935128132002447548386656897140223409046140783545930398584803434013675234197392017488945403851270356728800009263803944657147241388707760949464484603546339735102768273443551136390592037818137124442751187678443095628855856530569241650558571348619808701472152423230351678253993347653815906392552429065424192542748362930357748528954990681567055366709444815136846974101566869338475822812780740000874496 / 25764033072462857277513988217498322249426074337675990766617797240356675966219565086526793187484098306970658107635578610779267070508674838011745621162692697678892692545590596518549918154139394373589591193372377191996580205273111934220383162692613508435707952775483360618692646425052496039310136805884549238516570845512977608304911265128140236770023534054607847618423527036780557364429055754643463450072153951902549621120770703873562738959582752335625 * s ^ 56 + -288780685796029096375851682363603129849811284731029329756778180696629922903871319755557392776977628337411771584073341649696575480158628646859429649692531746307616997577926751230784800194256568910820661276164220477670737928540183946142899117787484359356666044519275489350056916422868860644152873522492999681793720122013931327462631572035054139223532302797910013114883459459444563554454451613841691729191918305084917699774298502703338344961966925094603536184200655199057337841095695234412963187542702559596739173766135808 / 1458341494667708902500791785896131448080721188925056081129309277756038262238843306784535463442496130583244798545410110044109456821245745547834657801661850812012793917674939425578297254007890247561674973209757199546976238034327090616248103548638500477492902987291510978416564891984103549394913404106672598406598349746017600470089316894045673779435294380449500808590010964346069284779003155923214912268235129352974506855892681351333739941108457679375 * s ^ 57 + 506140666679404234624255383815930538455267852630400044400173328353514110495234460672559069260606249281523321312393590379097010582382338803031635211275288567755631366888837798788602771020000594923670496274907842624068875134910955312262056703548058458264365402566806843784071307709657610330151300835991002358565841484739829006727153131022157367975512160926849163517493031180450238185323755342389701218951733026122144715065050391616469244380309401481872325838466191676936953699253006416959116430036313794683168949796864 / 1019106565106714816562398173232796260014480215880542334821320250004219610229799655335105145662121684544545631408392809255142876884168934694503604333795842635927878349178853546875120373171132248470772168560277567817593457745860999731829562228258910186927255756318316546762099854635991299367514608041001116985743081583520335758273456949018639957676655751537037602089455600521362183633125895124538722759074164467487426174628009330072494717755735625 * s ^ 58 + -68850351540064382718455148661214935771230110510905866443604070156389881444424593122058828988869530010845462715320303688218114857067219044932148106779338606522531260924209769003751421853308495615830537481872725713037294770437192775968229088760630313405054667377170812913453239369895772800602876124911905146484610263016533926741187008239614568150606793808103556852381163036925412075070018622423384795663405369919617159121589535290787719369580883911466600963579520914496593440869418802933383555374628397065791216812032 / 57685277270191404711079141881101675095159257502672207631395485849295449635649037094439913905403114219502582909909026938970351521745411397802090811346934488826106321651633219634440775839875410290798424635487409499109063645992132060292239371410881708693995608848206596986533954035999507511368751398547233036928853674538886929713591902774639997604339004803983260495629562293662010394327880856105965439192877234008722236299698641324858191571079375 * s ^ 59 + 996701730461654190259872399709584935803007045395082287266039263264306197960422715933453730107553267811322134657887662169390641898049284463541114516282716040655640935940187607345738366893832004772863807209698092166479093601445302427709777051539664148143067411217269368691949703921120340970025084849270183964994099818235847242265389406965867836057477802068163241224715750609372699530219626107559216684181277101674102327572068201150971037892423743515199973984039711947112672454835479161893056484565565873270999220224 / 362800485976046570509931709944035692422385267312403821581103684586763834186471931411571785568573045405676622074899540496668877495254159734604344725452418168717649821708385029147426263143870504973574997707467984271126186452780704781712197304470954142729532131120796207462477698339619544096658813827341088282571406758106207105116930206129811305687666696880397864752387184236867989901433212931484059365992938578671209033331437995753825104220625 * s ^ 60 + -124317656791936890077830454780892832314137375277204966689938288548492039315496577248681436167141507739757892298796720480127803753997254701100362045923453871666584803896865827919117149661071305913876952319686379529324196579661898068848791967015669405984866261951734110099634091616259586640216448713306108986632022837966493562466643775466108255475333406669462383699842709316679652822093089408994597775691046598869619310816299887578051794519453810893636986894984713782772993918037506159221019023334427089948578414592 / 20535876564681881349618776034568058061644449093154933297043604787930028350177656494994629371806021438057167287258464556415219480863443003845528946723721783134961310662738775234759977159087009715485377228724602883271293572798907817832765885158733253362048988554007332497876096132431294948867480027962703110334230571213558892742467747516781772020056605483796105552021916088879320183099993184800984492414694636528559001886685169570971232314375 * s ^ 61 + 23561802558536452922868375694605623816672059433733663874498911541964269320489083932818200326167264357678105876388554821764920185335652329136772353415046708867870122073493034153351401813743811711770429685178021347188573710912756514018443840569616130498040438984847690104186837542513729952487479176687381449996190007186281022230470370280510931567787940598432695987787370700776727294174455776314493465892094546613245113147207837609259008901512086398138084772591577728809164680924311163031896535205039436726272 / 1845962473475310539444675853438548978268951148232678361222366446062220738759562256797488391140551294761975145628713244816781054003036562146191375819644875093852538628294828229872607253310433922936120669710563720675083174682521743883461132589526549790548067768696287683679457524354140262607851161096583727327180259302256768554094436749901932386279192489378964688206732867586302382003447014491106858050214205792124912965410123673844375 * s ^ 62 + -867066041685545514998680681148769477463683559740891201332918619521072993782619631076126889982083362737225238231536814901176150872897478384597009377320799590057358867235226136188888785216220690216927442610523201575188438356511316262731092549010459539161326934554599536015274903424262031618036032815159694767818443667243285204394812824652343510671798616431914083320068457211723314173357835543124458140509920158463734811308489611775167420959259782720554559394681612903603697861885608885358322289061247431213056 / 33690059050946974831751752570437776635738728368419043622201194626111311649975730568128824518632541285265050434102472724135915139230621461703131551684138677251955630868421245133335373887237056852292380201105733026121261929313624603328612745993758136473857053535963784113729398645288096275250027525026869050491475837562211805605858305211822059804572540015053827234091073440503648055378274218650362630345014521343605891344452688397844375 * s ^ 63 + 24792398519095385747188057783868645850351043984219662392440015264888814342294504742438867215548912543559423788241176699524686972746176912267214540109250718313805526556263748837740035966693317463947702678449018347564842007152414097932288 / 499889961203173745852563965186902561232507457197267571201417853998668152265018749307073011096335946163944053299943190731326488150187235798786402686280038088994375 * s ^ 64 + -894694924413180920060523256685797965308507420882954893745319271546761445890394646842377318233114807684260138639323992362011814731927226274541890386035642808789502526500889480795145832489842013527301312771786439855425639442317746110464 / 9801763945160269526520862062488285514362891317593481788263095176444473573823897045236725707771293062038118692155748837869146826474259525466400052672157609588125 * s ^ 65 + 1571484010250307025102605111129062628060882011643385949091252090272630528409835218333543118169811622392379088133006264632610683957149560173577232376737372049157418282435242964554907398658325612512598897696407610856650053283304599191552 / 9801763945160269526520862062488285514362891317593481788263095176444473573823897045236725707771293062038118692155748837869146826474259525466400052672157609588125 * s ^ 66 + -292452658190111142859333003369255551727355136613915191831488855151164219280207496730452139114227126638214488655143080458045456330745511802278687107224296976798337480082999723270107690857122491064808141345978110781165600147605127430144 / 1089084882795585502946762451387587279373654590843720198695899464049385952647099671692969523085699229115346521350638759763238536274917725051822228074684178843125 * s ^ 67 + 11965847675190880752619114996909961590231155257900470064606392051828061544441046868925777619520524614122794378796897899993908695419622382550507597625570317713505204580117329923464678885766862043258364791416493984921677752020928299008 / 27925253405015012896070832086861212291632168995992825607587165744856050067874350556229987771428185361931962085913814352903552212177377565431339181402158431875 * s ^ 68 + -1776342714306545849901869952142735785150007510628440272545396651740546561329195253179612762353223444917699280827744305510415132837192863589898452724329026646346808293789350336292058894425796530321910651059149257684639748312314937344 / 2729536047106730583826472309242073381888858623668471675929572591602471059265913964142780759613281275978312083585560801411625404197788784591033153069383906875 * s ^ 69 + 221668996870519362200296948110610466201486858081927698182880319734668252225435439762558907347184412121092885876876573702902796721819184168656284409672443570498736112841977753434643412138540546384061545236474794107343273020551593984 / 235885831231445852923275384749314983620024819329374095450703804212559227343967873444437843423369986812940550433320069257794788017092857927620149030687498125 * s ^ 70 + -33774694833355563864311271685553573306090992432833958032906705556357632973965072777052474248295864902259662723583062670111713030701004229771306145214588631320878311171951830468404463142664520335702659747662549772836314171003895808 / 26209536803493983658141709416590553735558313258819343938967089356951025260440874827159760380374442979215616714813341028643865335232539769735572114520833125 * s ^ 71 + 2455511347898541410646893444661932598299404917726199938087213506639647794777778962577405182372885523622783871390831660352966198083068444213662185122945359188042530559841147709702867321677015870511102169701815847132787567908356096 / 1465129386530719583374381271734875674658539250493006804041638535481734331328993002760483499524037185173543791511304777998725391410514645513168627519798125 * s ^ 72 + -54106618742990039052610956427177491994309032599017036636338727131600332402407379349491180141060553812965620634530816255481829142748808739776491356807333607392434169762815828817224679449863292806752850438708301015664770106295058432 / 26209536803493983658141709416590553735558313258819343938967089356951025260440874827159760380374442979215616714813341028643865335232539769735572114520833125 * s ^ 73 + 21007305832354439187467509246641386573403414977228992743870391573170841991383001184611970397178833898888538655365707559889606148487276918957174065185121501806563075082921038073542540636630790660119825677728945658813572837135089664 / 8736512267831327886047236472196851245186104419606447979655696452317008420146958275719920126791480993071872238271113676214621778410846589911857371506944375 * s ^ 74 + -23098482534564307186082135287458625384404741420445324957836579817661525058942186929842285514235073867698726558874721268702485160498971078087549769042712298397576694544752931650087786096950783352675930350772336669817809147346812928 / 8736512267831327886047236472196851245186104419606447979655696452317008420146958275719920126791480993071872238271113676214621778410846589911857371506944375 * s ^ 75 + 2658907083393730090777262647283280407062732970557960915603692570048962706090506717184069782993044735589454993863922116373706748981155938705683777328321758600414066043250398921738660740379657085874367807738120726468839401873997824 / 970723585314591987338581830244094582798456046622938664406188494701889824460773141746657791865720110341319137585679297357180197601205176656873041278549375 * s ^ 76 + -169848141222003622640885646524121689396012582159188324001853386745961349312451045344939548423779261754822018168290642905429541408588220952011493084486231203108610573757770184282824576268813304527237559367655807731467475222528 / 63658179901278246923639702947347011790835861146497387658612925090293778245181529395151012647761827683213268908497560322459190609299309899460491919375 * s ^ 77 + 34298369652580273819565558315408175573621587169518148466099378191988411917087185056279981426369469493649134443406569215578290840931048454671285752887242214635905077763137722137118917658569485893417232470321581745663964761554944 / 14068457758182492570124374351363689605774725313375922672553456444954924992185117996328373795155363917990132428777960831263481124655147487780768714181875 * s ^ 78 + -14479564367592335497813279757271123581915237845683426844134627290809574312323477318776308295332756078544087134038668811741269202654383821598671958771736608881252170320730128723559945314347111720392039416962328804599055515648 / 6947386547250613614876234247587007212728259414012801319779484664175271601079070615470801874150796996538337001865659669759743765261801228533712945275 * s ^ 79 + 41239832886494549835046538519443048409888520116822625075239914228666294559226594552434075230554447035468642044837400172586809167229106471361541413845952212713597015076099662525226051068277606260837976925217828599403120689152 / 24812094811609334338843693741382168616886640764331433284926730943483112860996680769538578121967132130494060720948784534856227733077861530477546233125 * s ^ 80 + -7554579821046860689139593479608729959377263922149733618069463425258304601630664005185034890075235232463639045121540614226777128512250652914494769796838519188806046091432348262887741701845581745347240011908795550805329444864 / 6130046953456423777831971394929712246524934777070118811570133527213474942128591719533060477191879702827944413410876179199773910525118731059158481125 * s ^ 81 + 576500497151487166419476464531531615712336964688595863217021167343786308257088999373791588924023402331316389962655033385343072645000637144597244619167619156966421528428962224650380799939415026077098112970245964309230256128 / 681116328161824864203552377214412471836103864118902090174459280801497215792065746614784497465764411425327157045652908799974878947235414562128720125 * s ^ 82 + -492811878867419142754336738610957514328622888928850931770329127323854058861341170049174162731165845258291581814742312338169785323002427155547931727674454835942324478776305698570020230638739286202796545819514641395482624 / 919185328153609803243660428089625468064917495437114831544479461270576539530453099345188255689290703677904395473215801349493763761451301703277625 * s ^ 83 + 57295327363362235943118711695394514627272133140549435407218241067738862423456554858928888239289707808643267750491772371935830589477343165018094385642585528265365182227963847557910380308142651131460601337578094988361728 / 183837065630721960648732085617925093612983499087422966308895892254115307906090619869037651137858140735580879094643160269898752752290260340655525 * s ^ 84 + -16882869273791478818036724194993181770866252410372551790483981174427085399987762132956661504834173810030742770328909697318545334446218995788386859529771431773341004706339654874701297329228340982379813252105432440242176 / 102131703128178867027073380898847274229435277270790536838275495696730726614494788816132028409921189297544932830357311261054862640161255744808625 * s ^ 85 + 41613618732832614256440349308203021653376926569584287697575265117572998749049453126653668725747718589998008199270547663819652228425729982258389083850470442237671738637863836188951249385577136582508860407083358486528 / 523752323734250600138837850763319355022745011645079676093720490752465264689716865723753991845749688705358629899268262877204423795698747409275 * s ^ 86 + -10161384676590360191668163023382680833198339676645956510595238075032451122363549683167062512501656436268645484706581933287434143467215628356519047540132577406682365253974856768469677978184600227646802965441605009408 / 296033922110663382687169219996658765882421093538523295183407233903567323520274750191687038869336780572594008203934235539289456928003639840025 * s ^ 87 + 62013195613503506134666999483089303809456162454142488382609101461855896748554432203438308935993471937503027243706230671490101719417558457255670473137393529768151184009208182300490521481709134829483483271765426176 / 4698951144613704487097924126931091521943191960928941193387416411167735293972615082407730775703758421787206479427527548242689792507994283175 * s ^ 88 + -9781217187178957315584834649241296142056175508320034767142432380897207850323385087714951088834698990959622432422631089630619360516729385445320460937112160761210508413183672927003093474371004146662032606622646272 / 2192843867486395427312364592567842710240156248433505890247460991878276470520553705123607695328420596834029690399512855846588569837063998815 * s ^ 89 + 89224910682606518163882829251466095772472619821046157936140756208497238141543031670878648644749981561924750925210402924025105181810074505727152927065598380648443836319582567003628680257111978673021328501506048 / 68383904391467632868368958188186363105202377809776690964058035089759141492324959619239325218142014454283670178778987188563053113421954225 * s ^ 90 + -3639113603656568410657768994158989966957156625298092655241181538475036524672357269565699155500568409341083002560647567037534465819071594348720655826816101646573258410612430396049275514221278784086336079921152 / 11245353166596899627242895346501757488411057684274389180756210214760392156515660026274911258094464599148870207176989004341479845318276917 * s ^ 91 + 4788457455208975577310557900490987723400559632332536796463223329086584303141468813490989901170230627895774720484420327563602124712444629942105011518499810901634506042273099755039721545011280324571114242048 / 72363919990971040072348103902842712280637436835742530120696333428316551843730115999195053140891020586543566326750250993188415993039105 * s ^ 92 + -31898595962181397143582414292241656453146944470859044481438837247811941801270351097920032434117762442266426385169756315381524561575806518426466930822142513118462172718181691833418535117257957469704945664 / 2978270344455982739351368013798865800204210414819214254133219507060859197127935808643177937945459134262638436139887971910980413506615 * s ^ 93 + 12164630231720538223907658769710172095344417426643048948044585024812220039060430918064958303617197382105993250133343177048780427961678959333018164949418870268104574939418622657488650133340834091761664 / 9454826490336453140797993694599573968902255285140362711534030181145584752787097805216437898239552807182979162348850704479302900021 * s ^ 94 + -72569181857078888468131102002004425964861888701141730392722432100103979670156743641947652838543334184112194869382151370803011472761375068094349189661463522356906987930110257170340024297124047880192 / 711653606799517978339633934002118470777589107483683214846647432989452615801179404693710379437385695164310259531633923993065809679 * s ^ 95 + 2846426162100540477504821406370358099097596818564993027077417967281494233146639620639655387504859468567430806465702543982189965316310808246859421143193791148489260371756378664313018408226839855104 / 711653606799517978339633934002118470777589107483683214846647432989452615801179404693710379437385695164310259531633923993065809679 * s ^ 96

theorem G67CenteredEvaluation.density2_eq (s : ℝ) : G67Centered.densityPolynomial G67Centered.squareLate s = D2 s

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

Equations

• G67CenteredEvaluation.H2 s = ⋯ + -2956329505380676359544506753596428117739750782959620433380828370517256456650824066012024281669752744352708645044285079037992482700921321079818006079675934491081865413936807929714065388867093630688582112925365251040031577792341240503644122659332149990768582046599257354900033476214861889999155225388363798540167627656021247798096827201750432335464875309261547624090763658569636010542629825065356049255052375663878220706499258635574592535401092296255585096772224317389894110076838795466850715149427088668889614260959634853311021056 / 69557905890408258232923183062635702450724696563435821141742342675594365349839617738607934260761886014724028382304656969388956068415422565343258467649715637723842770866040155563817398362223446265769028946528595713076588448015802234039918166280966153172664687650702187519625291705800447931044122904825586621724101649528490524287272743940205128727442044895303256287615722518848516413074030865340719538630989709934884488338136778150820858577229816798799382907041999375 * s ^ 48 + 37225997636942664802803239682207392647082072375988256740762135656230332988470143306433424075976493030946457438041680421823433020721424054240736166376149122691780636821063314640342046395734321109207474709539813250994996720003468379031646191159039345646258968568776419347980493164391425535966570397509782080320961696237895225976051623277550963946092628035475321816345414134013934094657502093325635314310649486825736697990271529351647033328515448344262596499835980101267305394123651653837349170611745310638270461358864347069463658496 / 235796926257421705582047771514217884408431518538942815065403287434876496374613546925218091613526141898970133950076793122645580634439702910188781849454067476309127380482991470747783507655587657466978028944521465970743906751449794994638464727204029915472114884551751440711182592637902147388885422928937051503832017541483373538307169867822456379774158881752002862509590405268297800922307563751060678184415744991540268800089658637882342407378156422984609228848400236875 * s ^ 49 + -1278486781175633661654891737153903234151819900438209263193080740853928215906897232275649806072014966500840111932053779897448352581470790931908808446728084272407518012119646320894110192528926442175156369395933928292228827623024192835624052325402354686659676785948031161010903932816359774666237506420576761363197547223233175023134631656306423882137073456356954939880930785854872067730476249628526759441689132198191552707727839383087754695235159306899294478044358687613911097562473287107835095676666827317952566994079499479978868736 / 2269897249301325621698573079651693149869383120320974346028141003416215791053268645795322406753235867337024778110096198716264734640351394976788427507259024608289635930718054204349090370192411026828821996000399171840045309505677656860208555325414227141626057802770036972575881715805758061117495407479178393375356349070883457242079032227786449555007305369195252815841263046479570667330646551319413536623178138154989110512992478223742225716000735685258078829884484375 * s ^ 50 + 168612685600090469962943077910208679777940786525998079584815137399562808708489623384090424977995674977430672332153649515971620963421048177991260300516151025476752456601499197991433034421435233452295304936574484157432661716740692608239467318879739961489175256777812634866044346545636141987818873973502608553064926569386894571508476319161148456197778201963513172550553919255712295237082848095431402755764237760076615637057537437623541238680120236469421006314569793474986000824478789461015911041113870170104517814260705872863821824 / 87369629973107627703114888348857623127047954065184672941460521640926041768842793158914296410879267346557180138577287648701510540873902750049969662543554909451148250918204350507021591607406009334543337204543666236862121347010989056506140620072547610734285998446242932529335824532900876314711143985991017405391074568011363259883796712163855794192734017984119164987097671977704229459519225748898181409646856638418448782009521803328946046427198128262763788923855625 * s ^ 51 + -2668385677265184456344164661874505796761727159930823501064680975268714588932900738398192239987250852037062784939793120525967674690153730530995935726179474286552487115819142130709055633598948827438143972636427891795776945898606950925760893308337045979938241965950623312810051653145851999534421074351916560746741605081724007918597910461430974084588888180552096050699320254592190721511522688703433154672593183790606529211730608939928707341997710797219271071844354538800107216927800746621505492950207355879752374654507541717843968 / 420201697983869463610985404563503181891092638863263317883457928720694984459843252336620737455209202924618328450427206597528537562471600351701666893476216730619654924874826695002323600035618986810604285482451964883169655017070979554043591587474331831130491298483595309982007295200781129149554151615939040425484265402940333843318297172819136265077892058377191692501764608105865698473455395758666799232485806992023616043700992764808101592139687631304450335186875 * s ^ 52 + 648539615576641480370015026314731857319170278407546777701755386799533708994515435177574950543668895799904740937565164720554776699239026358765006338028113646948185851822527594082730068770483446627111286576328184686934662255195749906158236299430894600641053768874402255408257623586983598951012573313001605154744305075931787106977044905338489220547513503286103360280470972696706563495735436509491890733537173566793385234855874702236570325473293915366248931300709821922973011667123908363890795446453522148666247263908847935291392 / 32323207537220727970075800351038706299314818374097178298727532978514998804603327102816979804246861763432179111571323584425272120190123103977051299498170517739973455759602053461717200002739922062354175806342458837166896539774690734926430122113410140856191638344891946921692868861598548396119550124303003109652635800226179526409099782524548943467530158336707053269366508315835822959496568904512830710191215922463355080284691751139084737856899048561880795014375 * s ^ 53 + -24654071732674017365689598304969454900143435091869984489466959141919603278145969686544014853598309985286396365286044495140479477095471453493104978366247994603411821323662940994173546797026188084559915655824708093985005587833642611134504111762279469518388713724199134497163465961300509507813734499013900096848205619539896060024470825986582866478829973685936038823433439297696691284618312065211612090913327671228216318822387474489902601582201617028160836442386091708331234193229805984903774016647308717909025377561857753088 / 405070962307761769276741136808834831087030324905847805301567642477130441556261389181662060676947429459447880096906681856317836292236921372298105450050709597052908863672622151589654040896660573544600655822361996527044151980255608761284441607675679172002626236915002005978041088484518613664138714755180700124632533167095542319061841235850134102214438445939082209805646928561977968889533855567546867734768914179516383670705808848145158267190286720961066875 * s ^ 54 + 17489614265237540908353967944990444472126783915831406606914523437143867805304272934281258253491520029133164806613193904059999656171168308470498855272286960086084261864150379837301295378820102063753924660506254381184568170665530394122974732011167145607026552661503421489129470414957447746448441034921132609221711026177142777884772763643752590476702392915578636509756201865068178722516114759714188805430033594318022006545902577549333394217972314384553323332497797642190640529509263249433268923013812869774249831822312603648 / 98687957591656590126186535776753800725415240201634351904676444247493503803332852265527857359512952924018970851384100433198583455989364936329536522517277892427285781855314525846281891038605761993745220448431373907706900631743870122579622232732115470721686780926817399969874059738144265510575692210540498378626882961426301047811585105106744443300449237035536514491115937426795344050019842201991121133526382433037629844174879418882960546005638115423778125 * s ^ 55 + -14200703661085001785217650106289160849409186444023990338984311317877421677783151752025228751355674884296682743477853814827137381682505385159874361766400800578353424792139381240365101793110619843908553188249565042958528795932392279268430007652709652132049971406731597563036581878008284813861973444824772809822351995538421196089825116878995505034949729028797472986137619154847650243145639698924840696067628551244860336567072315898531605541621269942181326448529305790039507097075452194315215698294330688277004221888843481088 / 28675368809651160149873068886075632663611220737833377723245608328516980350402375941304320817669801415658342473798398993797324249476155094707072876354076972516607566803242333925146058905557145937805214998223455814692193768468973582787286460076878834888942951439112980368604915471083428091752182264949503302468943351055944078043366238087620083525036193402778534399305385591936760346609539054918174819930307348467537728307417793411275328462015603349550625 * s ^ 56 + 1949789386561138417999091293992708724312585951580695600475489691485229689650643421929354345738711724196190130194488895333807935128132002447548386656897140223409046140783545930398584803434013675234197392017488945403851270356728800009263803944657147241388707760949464484603546339735102768273443551136390592037818137124442751187678443095628855856530569241650558571348619808701472152423230351678253993347653815906392552429065424192542748362930357748528954990681567055366709444815136846974101566869338475822812780740000874496 / 1468549885130382864818297328397404368217286237247531473697214442700330530074515209932027211686593603497327512135227980814418223018994465766669500406273483767696883475098664001557345334785945479294606698022225499943805071700567380250561840273478969980835353308202551555265480846227992274240677797935419306595444538194239723673379942112303993495891341441112647314250141041096491769772456178014677416654112775258445328403883930120793076120696216883130625 * s ^ 57 + -144390342898014548187925841181801564924905642365514664878389090348314961451935659877778696388488814168705885792036670824848287740079314323429714824846265873153808498788963375615392400097128284455410330638082110238835368964270091973071449558893742179678333022259637744675028458211434430322076436761246499840896860061006965663731315786017527069611766151398955006557441729729722281777227225806920845864595959152542458849887149251351669172480983462547301768092100327599528668920547847617206481593771351279798369586883067904 / 42291903345363558172522961790987811994340914478826626352749969054925109604926455896751528439832387786914099157816893191279174247816126620887205076248193673548371023612573243341770620366228817179288574223082958786862310902995485627871195002910516513847294186631453818374080381867539002932452488719093505353791352142634510413632590189927324539603623537033035523449110317966036009258591091521773232455778818751236260698820887759188678458292145272701875 * s ^ 58 + 506140666679404234624255383815930538455267852630400044400173328353514110495234460672559069260606249281523321312393590379097010582382338803031635211275288567755631366888837798788602771020000594923670496274907842624068875134910955312262056703548058458264365402566806843784071307709657610330151300835991002358565841484739829006727153131022157367975512160926849163517493031180450238185323755342389701218951733026122144715065050391616469244380309401481872325838466191676936953699253006416959116430036313794683168949796864 / 60127287341296174177181492220734979340854332736951997754457894750248957003558179664771203594065179388128192253095175746053429736165967146975712655693954715519744822601552359265632102017096802659775557945056376501238014007005798984177944171467275701028708089622780676258963891423523486662683361874419065902158841813427699809738133959992099757502922689340685218523277880430760368834354427812347784642785375703581758144303052550474277188347588401875 * s ^ 59 + -17212587885016095679613787165303733942807527627726466610901017539097470361106148280514707247217382502711365678830075922054528714266804761233037026694834651630632815231052442250937855463327123903957634370468181428259323692609298193992057272190157578351263666844292703228363309842473943200150719031227976286621152565754133481685296752059903642037651698452025889213095290759231353018767504655605846198915851342479904289780397383822696929842395220977866650240894880228624148360217354700733345888843657099266447804203008 / 865279159052871070666187128216525126427388862540083114470932287739431744534735556416598708581046713292538743648635404084555272826181170967031362170204017332391594824774498294516611637598131154361976369532311142486635954689881980904383590571163225630409934132723098954798009310539992612670531270978208495553932805118083303945703878541619599964065085072059748907434443434404930155914918212841589481587893158510130833544495479619872872873566190625 * s ^ 60 + 996701730461654190259872399709584935803007045395082287266039263264306197960422715933453730107553267811322134657887662169390641898049284463541114516282716040655640935940187607345738366893832004772863807209698092166479093601445302427709777051539664148143067411217269368691949703921120340970025084849270183964994099818235847242265389406965867836057477802068163241224715750609372699530219626107559216684181277101674102327572068201150971037892423743515199973984039711947112672454835479161893056484565565873270999220224 / 22130829644538840801105834306586177237765501306056633116447324759792593885374787816105878919682955769746273946568871970296801527210503743810865028252597508291776639124211486777993002051776100803388074860155547040538697373619622991684444035572728202706501459998368568655211139598716792189896187643467806385236855812244478633412132742573918489646947668509704269749895618238448947383987425988820527621325569253298943751033217717740983331357458125 * s ^ 61 + -62158828395968445038915227390446416157068687638602483344969144274246019657748288624340718083570753869878946149398360240063901876998627350550181022961726935833292401948432913959558574830535652956938476159843189764662098289830949034424395983507834702992433130975867055049817045808129793320108224356653054493316011418983246781233321887733054127737666703334731191849921354658339826411046544704497298887845523299434809655408149943789025897259726905446818493447492356891386496959018753079610509511667213544974289207296 / 636612173505138321838182057071609799910977921887802932208351748425830878855507351344833510525986664579772185905012401248871803906766733119211397348435375277183800630544902032277559291931697301180046694090462689381410100756766142352815742439920730854223518645174227307434158980105370143414891880866843796420361147707620325675016500173020234932621754769997679272112679398755258925676099788728830519264855533732385329058487240256700108201745625 * s ^ 62 + 23561802558536452922868375694605623816672059433733663874498911541964269320489083932818200326167264357678105876388554821764920185335652329136772353415046708867870122073493034153351401813743811711770429685178021347188573710912756514018443840569616130498040438984847690104186837542513729952487479176687381449996190007186281022230470370280510931567787940598432695987787370700776727294174455776314493465892094546613245113147207837609259008901512086398138084772591577728809164680924311163031896535205039436726272 / 116295635828944563985014578766628585630943922338658736757009086101919906541852422178241768641854731570004434174608934423457206402191303415210056676637627130912709933582574178481974256958557337144975602191765514402530240004998869864658051353140172636804528269427866124071805824034310836544294623149084774821612356336042176418907949515243821740335589126830874775357024170657937050066217161912939732057163494964903869516820837791452195625 * s ^ 63 + -13547906901336648671854385642949523085370055620951425020826853430016765527853431735564482655970052542769144347367762732830877357389023099759328271520637493594646232300550408377951387269003448284639491290789425024612319349320489316605173321078288430299395733352415617750238670366004094244031813012736870230747163182300676331318668950385192867354246853381748657551876069643933176783958716180361319658445467502475995856426695150183986990952488434105008664990541900201618807779091962638833723785766581991112704 / 33690059050946974831751752570437776635738728368419043622201194626111311649975730568128824518632541285265050434102472724135915139230621461703131551684138677251955630868421245133335373887237056852292380201105733026121261929313624603328612745993758136473857053535963784113729398645288096275250027525026869050491475837562211805605858305211822059804572540015053827234091073440503648055378274218650362630345014521343605891344452688397844375 * s ^ 64 + 24792398519095385747188057783868645850351043984219662392440015264888814342294504742438867215548912543559423788241176699524686972746176912267214540109250718313805526556263748837740035966693317463947702678449018347564842007152414097932288 / 32492847478206293480416657737148666480112984717822392128092160509913429897226218704959745721261836500656363464496307397536221729762170326921116174608202475784634375 * s ^ 65 + -40667951109690041820932875303899907514023064585588858806605421433943702085927029401926241737868854894739097210878363289182355215087601194297358653910711036763159205750040430945233901476811000614877332398717565447973892701923533914112 / 29405291835480808579562586187464856543088673952780445364789285529333420721471691135710177123313879186114356076467246513607440479422778576399200158016472828764375 * s ^ 66 + 1571484010250307025102605111129062628060882011643385949091252090272630528409835218333543118169811622392379088133006264632610683957149560173577232376737372049157418282435242964554907398658325612512598897696407610856650053283304599191552 / 656718184325738058276897758186715129462313718278763279813627376821779729446201102030860622420676635156553952374435172137232837373775388206248803529034559842404375 * s ^ 67 + -73113164547527785714833250842313887931838784153478797957872213787791054820051874182613034778556781659553622163785770114511364082686377950569671776806074244199584370020749930817526922714280622766202035336494527695291400036901281857536 / 18514443007524953550094961673588983749352128044343243377830290888839561195000694418780481892456886894960890862960858915975055116673601325880977877269631040333125 * s ^ 68 + 11965847675190880752619114996909961590231155257900470064606392051828061544441046868925777619520524614122794378796897899993908695419622382550507597625570317713505204580117329923464678885766862043258364791416493984921677752020928299008 / 1926842484946035889828887413993423648122619660723504966923514436395067454683330188379869156228544789973305383928053190350345102640239052014762403516748931799375 * s ^ 69 + -888171357153272924950934976071367892575003755314220136272698325870273280664597626589806381176611722458849640413872152755207566418596431794949226362164513323173404146894675168146029447212898265160955325529574628842319874156157468672 / 95533761648735570433926530823472568366110051828396508657535040706086487074306988744997326586464844659240922925494628049406889146922607460686160357428436740625 * s ^ 70 + 221668996870519362200296948110610466201486858081927698182880319734668252225435439762558907347184412121092885876876573702902796721819184168656284409672443570498736112841977753434643412138540546384061545236474794107343273020551593984 / 16747894017432655557552552317201363837021762172385560776999970099091705141421719014555086883059269063718779080765724917303429949213592912861030581178812366875 * s ^ 71 + -4221836854169445483038908960694196663261374054104244754113338194544704121745634097131559281036983112782457840447882833763964128837625528721413268151823578915109788896493978808550557892833065041962832468457818721604539271375486976 / 235885831231445852923275384749314983620024819329374095450703804212559227343967873444437843423369986812940550433320069257794788017092857927620149030687498125 * s ^ 72 + 2455511347898541410646893444661932598299404917726199938087213506639647794777778962577405182372885523622783871390831660352966198083068444213662185122945359188042530559841147709702867321677015870511102169701815847132787567908356096 / 106954445216742529586329832836645924250073365285989496695039613090166606187016489201515295465254714517668696780325248793906953572967569122461309808945263125 * s ^ 73 + -27053309371495019526305478213588745997154516299508518318169363565800166201203689674745590070530276906482810317265408127740914571374404369888245678403666803696217084881407914408612339724931646403376425219354150507832385053147529216 / 969752861729277395351243248413850488215657590576315725741782306207187934636312368604911134073854390230977818448093618059823017403603971480216168237270825625 * s ^ 74 + 21007305832354439187467509246641386573403414977228992743870391573170841991383001184611970397178833898888538655365707559889606148487276918957174065185121501806563075082921038073542540636630790660119825677728945658813572837135089664 / 655238420087349591453542735414763843388957831470483598474177233923775631511021870678994009509361074480390417870333525716096633380813494243389302863020828125 * s ^ 75 + -5774620633641076796520533821864656346101185355111331239459144954415381264735546732460571378558768466924681639718680317175621290124742769521887442260678074599394173636188232912521946524237695838168982587693084167454452286836703232 / 165993733088795229834897492971740173658535983972522511613458232594023159982792207238678482409038138868365572527151159848077813789806085208325290058631943125 * s ^ 76 + 241718825763066371888842058843934582460248451868905537782153870004451155099136974289460889363004066871768635805811101488518795361923267155062161575301978054583096913022763538339878249125423371443124346158010975133530854715817984 / 6795065097202143911370072811708662079589192326360570650843319462913228771225411992226604543060040772389233963099755081500261383208436236598111288949845625 * s ^ 77 + -84924070611001811320442823262060844698006291079594162000926693372980674656225522672469774211889630877411009084145321452714770704294110476005746542243115601554305286878885092141412288134406652263618779683827903865733737611264 / 2482669016149851630021948414946533459842598584713398118685904078521457351562079646410889493262711279645317487431404852575908433762673086078959184855625 * s ^ 78 + 34298369652580273819565558315408175573621587169518148466099378191988411917087185056279981426369469493649134443406569215578290840931048454671285752887242214635905077763137722137118917658569485893417232470321581745663964761554944 / 1111408162896416913039825573757731478856203299756697891131723059151439074382624321709941529817273749521220461873458905669815008847756651534680728420368125 * s ^ 79 + -904972772974520968613329984829445223869702365355214177758414205675598394520217332423519268458297254909005445877416800733829325165898988849916997423233538055078260645045633045222496582146694482524502463560145550287440969728 / 34736932736253068074381171237935036063641297070064006598897423320876358005395353077354009370753984982691685009328298348798718826309006142668564726375 * s ^ 80 + 41239832886494549835046538519443048409888520116822625075239914228666294559226594552434075230554447035468642044837400172586809167229106471361541413845952212713597015076099662525226051068277606260837976925217828599403120689152 / 2009779679740356081446339193051955657967817901910846096079065206422132141740731142332624827879337702570018918396851547323354446379306783968681244883125 * s ^ 81 + -3777289910523430344569796739804364979688631961074866809034731712629152300815332002592517445037617616231819522560770307113388564256125326457247384898419259594403023045716174131443870850922790872673620005954397775402664722432 / 251331925091713374891110827192118202107522325859874871274375474615752472627272260500855479564867067815945720949845923347190730331529867973425497726125 * s ^ 82 + 576500497151487166419476464531531615712336964688595863217021167343786308257088999373791588924023402331316389962655033385343072645000637144597244619167619156966421528428962224650380799939415026077098112970245964309230256128 / 56532655237431463728894847308796235162396620721868873484480120306524268910741456969027113289658446148302154034789191430397914952620539408656683770375 * s ^ 83 + -123202969716854785688584184652739378582155722232212732942582281830963514715335292512293540682791461314572895453685578084542446330750606788886982931918613708985581119694076424642505057659684821550699136454878660348870656 / 19302891891225805868116868989882134829363267404179411462434068686682107330139515086248953369475104777235992304937531828339369038990477335768830125 * s ^ 84 + 57295327363362235943118711695394514627272133140549435407218241067738862423456554858928888239289707808643267750491772371935830589477343165018094385642585528265365182227963847557910380308142651131460601337578094988361728 / 15626150578611366655142227277523632957103597422430952136256150841599801172017702688868200346717941962524374723044668622941393983944672128955719625 * s ^ 85 + -8441434636895739409018362097496590885433126205186275895241990587213542699993881066478330752417086905015371385164454848659272667223109497894193429764885715886670502353169827437350648664614170491189906626052716220121088 / 4391663234511691282164155378650432791865716922643993084045846314959421244423275919093677221626611139794432111705364384225359093526933997026770875 * s ^ 86 + 41613618732832614256440349308203021653376926569584287697575265117572998749049453126653668725747718589998008199270547663819652228425729982258389083850470442237671738637863836188951249385577136582508860407083358486528 / 45566452164879802212078893016408783886978816013121931820153682695464478028005367317966597290580222917366200801236338870316784870225791024606925 * s ^ 87 + -115470280415799547632592761629348645831799314507340414893127705398096035481403973672352983096609732230325516871665703787357206175763813958596807358410597470530481423340623372368973613388461366223259124607290966016 / 296033922110663382687169219996658765882421093538523295183407233903567323520274750191687038869336780572594008203934235539289456928003639840025 * s ^ 88 + 62013195613503506134666999483089303809456162454142488382609101461855896748554432203438308935993471937503027243706230671490101719417558457255670473137393529768151184009208182300490521481709134829483483271765426176 / 418206651870619699351715247296867145452944084522675766211480060593928441163562742334288039037634499539061376669049951793599391533211491202575 * s ^ 89 + -4890608593589478657792417324620648071028087754160017383571216190448603925161692543857475544417349495479811216211315544815309680258364692722660230468556080380605254206591836463501546737185502073331016303311323136 / 98677974036887794229056406665552921960807031179507765061135744634522441173424916730562346289778926857531336067978078513096485642667879946675 * s ^ 90 + 89224910682606518163882829251466095772472619821046157936140756208497238141543031670878648644749981561924750925210402924025105181810074505727152927065598380648443836319582567003628680257111978673021328501506048 / 6222935299623554591021575195124959042573416380689678877729281193168081875801571325350778594850923315339813986268887834159237833321397834475 * s ^ 91 + -909778400914142102664442248539747491739289156324523163810295384618759131168089317391424788875142102335270750640161891759383616454767898587180163956704025411643314602653107599012318878555319696021584019980288 / 258643122831728691426586592969540422233454326738310951157392834939489019599860180604322958936172685780424014765070747099854036442320369091 * s ^ 92 + 4788457455208975577310557900490987723400559632332536796463223329086584303141468813490989901170230627895774720484420327563602124712444629942105011518499810901634506042273099755039721545011280324571114242048 / 6729844559160306726728373662964372242099281625724055301224759008833439321466900787925139942102864914548551668387773342366522687352636765 * s ^ 93 + -15949297981090698571791207146120828226573472235429522240719418623905970900635175548960016217058881221133213192584878157690762280787903259213233465411071256559231086359090845916709267558628978734852472832 / 139978706189431188749514296648546692609597889496503069944261316831860382265012983006229363083436579310344006498574734679816079434810905 * s ^ 94 + 12164630231720538223907658769710172095344417426643048948044585024812220039060430918064958303617197382105993250133343177048780427961678959333018164949418870268104574939418622657488650133340834091761664 / 898208516581963048375809400986959527045714252088334457595732867208830551514774291495561600332757516682383020423140816925533775501995 * s ^ 95 + -2267786933033715264629096937562638311401934021910679074772576003128249364692398238810864151204479193253506089668192230337594108523792970877948412176920735073653343372815945536573125759285126496256 / 2134960820398553935018901802006355412332767322451049644539942298968357847403538214081131138312157085492930778594901771979197429037 * s ^ 96 + 2846426162100540477504821406370358099097596818564993027077417967281494233146639620639655387504859468567430806465702543982189965316310808246859421143193791148489260371756378664313018408226839855104 / 69030399859553243898944491598205491665426143425917271840124800999976903732714402255289906805426412430938095174568490627327383538863 * s ^ 97

theorem G67CenteredEvaluation.primitive2_deriv (s : ℝ) : HasDerivAt H2 (D2 s) s

theorem G67CenteredEvaluation.integral2_eq : ∫ (s : ℝ) in G67Centered.a + G67Centered.b..2 * G67Centered.b, G67Centered.densityPolynomial G67Centered.squareLate s = H2 (2 * G67Centered.b) - H2 (G67Centered.a + G67Centered.b)

theorem G67CenteredEvaluation.endpoint2_eq : H2 (2 * G67Centered.b) - H2 (G67Centered.a + G67Centered.b) = 51754009728125913193633205705375495723956268175527427051153020818189295190396990967675169482126383388284706633247853472595537828772109943024835573467911907546934694260776352607817138287381918588100292000650395006322411884287452847342722307153608276877733013890370662339619781773225349675712077503237560533330111758649075011049151059451322406506938910154801578342140042924791170203410648005528900154732224695416896214550923804796002366006354006354733450594584689821283580737745736029209083302580089109031571106359388135544269535482665918468690275642076726823536542742593146658217303299709212967395007429634475458183513227396951195887827839283213612836347097837128864264829992 / 152071549853495285330756033022120685765225716247197736499958109913640100720714826976213814595546937784020446337932383465885024461884565512007326213717197642420549894139675152633848866028098785841681558945484755342759083059340720400885055494379614867567645593443384328402089898789102893195066616417244269800164637210011695881482711035075271161576698532560456130431384452168240260050316909772157856567459873141641671647333211725504532659199388457099689698859116884544829911453144023320777627447847944959196096905940425227730920372220739385529837086464591399198062075762455558923869772529438858926910031607956627864838384416687205327449675006849261712583446098205839806295756427