Optimised dyadic rationals

Stream: Is there code for X?

[Geoffrey Irving]

Does anyone have decently optimized dyadic rational code, for verified computation purposes? It’s not hard to write, but figured I’d check before doing it myself.

[Geoffrey Irving]

I’m a bit sad there’s no way to easily express a pair of two integers that will be unboxed if both are small.

[Aaron Liu]

Didn't this land in core a while ago?

[Aaron Liu]

docs#Dyadic

[Geoffrey Irving]

Nice! And sorry for not doing the search, I was pessimistically assuming it wouldn’t be that easy. :)

[Kim Morrison]

This library hasn't been exercised much yet, so @Geoffrey Irving if you have requests or suggestions please let me know.

[Geoffrey Irving]

Here's 200 terms of the Mandelbrot Böttcher series, as Dyadic rationals. Thank you! :heart:

#[1,-1p-1,1p-3,-1p-2,15p-7,0,-47p-10,-1p-4,987p-15,0,-3673p-18,1p-5,-61029p-22,0,-689455p-25,-21p-9,59250963p-31,0,-164712949p-34,39p-11,-2402805839p-38,-1p-6,-4850812329p-41,29p-11,-18151141041p-46,0,3534139462275p-49,-1039p-17,-22045971176589p-53,-1p-8,-750527255965871p-56,-4579p-19,54146872254247683p-63,0,-155379776183158669p-66,2851p-20,-6051993294029466699p-70,-1p-10,7704579806709870203p-73,92051p-24,-403307733528668035403p-78,0,1650116480759617184697p-81,-229813p-26,36124726440442241978477p-85,-41p-12,-225851495844149964787753p-88,564373p-26,-35761228458796476847725737p-94,0,362376876750551361794705823p-97,-29407003p-33,-6510398483578238274151194427p-101,33p-13,74815618913797220433481657203p-104,-30057875p-35,-698617278028915809388280344009p-109,0,-8675905413734991085610532783493p-112,-27868893p-36,-375687870961637050293461860951517p-116,1p-12,-1418434432207399687114226995905967p-119,-11847286243p-40,1084116104452462070609082665064238307p-127,0,-5267312999069023320468907267187837501p-130,21920911673p-42,-12587804195470930508423250884414875171p-134,-55p-16,-417465475024774297026833228267243630109p-137,10217713227p-42,-767196419810162046740001735517744387367p-142,0,78305803829791781470449330875047041905661p-145,-1447722066907p-48,-309138699931269436435772103286758515421879p-149,-6677p-21,-4762077071053136681440439791970629118569861p-152,8140709464361p-50,-898433408030351928659626606398808743523101411p-158,0,6396904578318243782775827158644261596698981573p-161,-7113832088153p-51,12325347197791945711576332419237705246727881039p-165,10439p-23,859524763639415653256406686989311141385605931017p-168,-36843615694781p-55,-346210142151645442264854087843339281975229036359p-173,0,-399629924972837688479488577064957798395993139497083p-176,-10288277991389p-57,-1012304885972405900855581770068720885091139867803867p-180,-104325p-25,4103777203739806732878678125824143143154829453682775p-183,340704551647237p-57,108376734166611269209485353086407219330670697959596263p-190,0,6782399940562309096731441404849652006563439725039228663p-193,-13025534542844563p-65,-5212774163111565741384568993260007702411936933422137151p-197,69735p-27,1749621609166100653959196203116873770019996374684408079183p-200,-71608953734461123p-67,1311635862589369585472703589697877677901086925728121746745p-205,-33p-14,-365885284282303297886245644284276114667710996174122761557075p-208,36281518593201443p-68,-21037435104652553397530379423554311424543666822639692977470847p-212,475805p-27,154472070943271712563673702833927794825195557591870681879926259p-215,-7279642326975824071p-72,1472937063700516491377968726867240513261137840579590913223565151p-221,0,-30016936941029238795511924604636437853053801779596964566485113401p-224,5284604814359475389p-74,795627929409815556008117859171272456370091708773942301881031524397p-228,639193p-30,-2619701071176509604609471545269563642151980416641905221365809825301p-231,-20860683838102114113p-74,-138268885720927885713404244258390439076583246641539533859266359532537p-236,-33p-16,120065623815432109297897401316904025258970435605148784501336912044907p-239,-1671161044648160976945p-80,235183938660872677677759316970790053238014769813356479079650877789059p-243,-725625p-32,-409961135793900161853290015403455895724345127508218050040343153192380335p-246,-10111509191249229780013p-82,104105914542998754338954254950933521028178746243498328611098025618931587235p-255,0,-43580996806273210517501141950817703073081227840289714743086658438448881053p-258,16506579224278377447821p-83,-5291166082614465507900402287577166520692790918940550851351996855554678161235p-262,-294996927p-37,-28477581699252930276988826093291737504693461254525056894833637606623252912333p-265,175500623382876533700741p-87,-290134568698401615270803872770325633954835866812519773412106892357519871238335p-270,13p-18,-13633491876970405442332852492529912584815063119571974440979940204798782854620507p-273,-468313198532168593346691p-89,146679191319490251210214162419841595908477113479350056801845758575660598303803361p-277,-568992355p-39,1124832409989212509045945615993252060070897025506411795390648913431171550301982947p-280,1078192855540008727273043p-89,-83283543070995966726491129327302399125127091962843392815408081892622612191675196159p-286,0,514212139641264083585631959659619695294127275051843320770756204836538424366035941993p-289,-59146818568353277756070159p-96,-9511636929399299544960838007508040518433042788951960386689311853500521681842643668725p-293,1834345301p-41,48426581541653764037427847411453254038777219154705774934425383518616599776984483027597p-296,-170654635573266980933214231p-98,-967461965770124610403117714875777316261627605098722633846578134777018823203571448378171p-301,-1265p-20,-9779810999355378942904563487546888240348497447991169961306671531441545729874742309460799p-304,-557956160964668210363035449p-99,-553402979446154230241393816746032128841627473126126440479588326601835860126999890118655823p-308,-3093862891p-43,1190023755135072851723368833995725415563728171241922114879183587741073784495125101111424507p-311,16338264435940752159686683761p-103,-159265621133342817793010551736970507411744455904251367104052627741720240557498954539521147283p-318,0,1068209937433639309448530533143994841461211893318920212646134978433822792736767422359780963901p-321,-32311527284616962991735607059p-105,21683451192360971160112937982426875222116808013597948538053875333005102035779029341884157456699p-325,5768515427p-44,347802167325340235909173842563130110455128082779647491829054764220247031102777815783286930073429p-328,-27445340036018663189247713993p-105,-18245423626005078350781682030251933181451347747127812333469630156191488032948726069925592376488181p-333,507p-22,-76445221191685652808725339189090339190559336612672652713912501917875028878730008068733504496974137p-336,519283213047784707099783408845p-111,437979869983459684420919337669220048525190314965343180400799851795400164887449059678313266012456563p-340,45349077837p-45,17618787435907578707008956806804036310435508303248288086942978765226792825245654470177651200555637897p-343,-11769332494043624306864016981503p-113,160547341188289500347263839238617462508346034284249850507825159055627984638729050776384818257504821681p-349,0,-4232344205652379583972937246261433281768969491503811721891605042657646543414204624376518429950506219927p-352,13713846038986901692471349228463p-114,80208098041457605518234810298416413304498340621832325233120562693827440789260338182999701921433548121523p-356,854646625p-46,-1451624472154401157390024617464421788611828764301727734084626258471073779974249215877965268664923216558315p-359,-237659459316207208102495783597533p-118,10500506528510758503704545735441747398039417911133607113864323564601012808025694161660778598636860786444993p-364,-457p-24,-337909317422014923920076893307889242874551488903169280665350070481045577052607915818531022288326431479574307p-367,-833418054450972768231054955147245p-120,2963071704188349829584806331970750549821712044093271998510415478698037423589029906356722781258369397092059541p-371,-11700192937165p-52,-15020778517521636165509691702306324220299664568455256311553713893052554070282886441187901382362347152956983465p-374,3275796152153003339602101815578085p-120,-3550940557707906988936457322259559537228291457376007064260683528336036258082467362107600225440949789817972286969p-382,0,70129728330013439288415907034433766713755989187416518956148431246390922641105470597783844599457960396329068510247p-385,-455923325312439142438623430688965123p-129,-1190330401348345791034775885774633963422486897924746552450688414662546942257384836115392835370701669231241266100647p-389,2251139093419p-54,5308487409990664308407093846776403812824717015552344964358501732208389749968126900972829445799575266637809079175591p-392,866596263925047073263081932820666525p-131]

This is from https://github.com/girving/bottcher/blob/main/Bottcher/Actual.lean, with a few more Dyadic facts added in https://github.com/girving/bottcher/blob/main/Bottcher/Dyadic.lean. The theorem that this is the right computation is https://github.com/girving/bottcher/blob/195d6c043b60ac6a74d1b9826cea2942f1550f71/Bottcher/Pray.lean#L255.

[Geoffrey Irving]

The key reason I need them is that if you do monic power series computations involving field operations and sqrt, you get Dyadic rationals (https://github.com/girving/series/blob/66279eadd04c727f75930a9d585c6de3b5c319f2/Series/Series/Sqrt.lean#L20). In this case it's alternately possible to clear denominators by multiplying by 2 ^ (2 * n), then work in Nat, but I haven’t formalised that yet.