BesselLarge0.lean

import LeanExe.ProofKit.BesselStart

/-!
`P0` and `Q0` on `[2, ∞)` within `2 ^ -80` of explicit approximations: Taylor polynomials of
degree 40 on `[2, 3]`, `[3, 9/2]`, `[9/2, 7]`, `[7, 10]`, `[10, 15]`, `[15, 22]`, and `[22, 30]`,
and Hankel's expansion with 60 terms in `1/x` on `[30, ∞)`.  The polynomials are dyadic
rationals that a Python model computed from high-precision values of the Bessel functions; the
proof uses only their residuals in the system of `P0` and `Q0`, which the kernel bounds, and
the enclosures at `x = 2` of `BesselStart`.  `chain0_sound` carries the bound `2 ^ -83` at 2
through the pieces, and `asym_bound0` from 30 to infinity.
-/

namespace LeanExe.ProofKit.BesselLarge0

open Real Set BesselPQ BesselChain BesselStart BesselConstants BesselEnergy PolyCalc PolyCalculus
  PolyBound

/-- `[2, 3]`. -/
def piece0_0 : Piece where
  a := 2
  b := 3
  c := 5 / 2 ^ 1
  H := 1 / 2 ^ 1
  A := [1285821016309941060627690518004799 / 2 ^ 110, 4250950283120667036364700374329 / 2 ^ 109, -4333415278011147779264742410867 / 2 ^ 110, 969452706400432788225086939621 / 2 ^ 109, -808163372566203604316917565779 / 2 ^ 110, 322797677308743286856332713063 / 2 ^ 110, -31383303950916589064716462785 / 2 ^ 108, 23999978588187634123615317093 / 2 ^ 109, -18160755171471190760922049179 / 2 ^ 110, 1706912090202360266527848271 / 2 ^ 108, -2557918753231997127105245635 / 2 ^ 110, 956783902032460757976056429 / 2 ^ 110, -178888506092851393820627601 / 2 ^ 109, 66930570802624699282236423 / 2 ^ 109, -12534946019823219463599671 / 2 ^ 108, 18808273751048055722351485 / 2 ^ 110, -7067159185793628383075591 / 2 ^ 110, 2660227583111476414795699 / 2 ^ 110, -1003206526246573375994263 / 2 ^ 110, 379017942789678306424887 / 2 ^ 110, -71727292662461455488395 / 2 ^ 109, 54391802888031895501117 / 2 ^ 110, -20658122982487343632513 / 2 ^ 110, 7858828155842911051153 / 2 ^ 110, -2994360110264544641437 / 2 ^ 110, 1142612561192219486011 / 2 ^ 110, -218314439607787564869 / 2 ^ 109, 167076348849675377153 / 2 ^ 110, -32007236968563097105 / 2 ^ 109, 24556979039115464569 / 2 ^ 110, -9431471185468310103 / 2 ^ 110, 3626329237581818245 / 2 ^ 110, -174471786254035767 / 2 ^ 107, 134444035177696923 / 2 ^ 108, -51849635843536881 / 2 ^ 108, 80058671473500277 / 2 ^ 110, -30930815767320295 / 2 ^ 110, 11960176229010245 / 2 ^ 110, -1157100034477607 / 2 ^ 108, 1792487707800431 / 2 ^ 110, -694703021152713 / 2 ^ 110]
  B := [-60435478031275864655521571548443 / 2 ^ 110, 21383005048187673433289067949229 / 2 ^ 110, -7293191005615816779618969317689 / 2 ^ 110, 2424067602186042751791786105991 / 2 ^ 110, -791423958069838219688751679553 / 2 ^ 110, 255277458614850640176208553327 / 2 ^ 110, -81677625499109602885220173167 / 2 ^ 110, 3248899803944360085880212609 / 2 ^ 107, -8238238791653562633328295709 / 2 ^ 110, 650586573541472445664923153 / 2 ^ 108, -51188129023536448684196597 / 2 ^ 106, 128260788102302466066862415 / 2 ^ 109, -39899872911139188772580025 / 2 ^ 109, 24579513984687910485117391 / 2 ^ 110, -932631254543196062999297 / 2 ^ 107, 276968435296921908558449 / 2 ^ 107, -318043242109052027679793 / 2 ^ 109, 86337529886476504241691 / 2 ^ 109, -21129256908095806734587 / 2 ^ 109, 8082626590648345913495 / 2 ^ 110, -80731171342692430225 / 2 ^ 108, -833161867571978232351 / 2 ^ 110, 326029266559623109347 / 2 ^ 109, -91638759680956286977 / 2 ^ 108, 45426697904488776849 / 2 ^ 108, -84321943479115371943 / 2 ^ 110, 37585762631010122827 / 2 ^ 110, -16309732475837882331 / 2 ^ 110, 1736065166087288585 / 2 ^ 108, -364449317051500681 / 2 ^ 107, 605585439379512851 / 2 ^ 109, -498978640295038613 / 2 ^ 110, 25527484111708245 / 2 ^ 107, -41569679236929855 / 2 ^ 109, 33700013675621837 / 2 ^ 110, -3402800681368239 / 2 ^ 108, 5481070039331973 / 2 ^ 110, -2201630531505847 / 2 ^ 110, 882474650348093 / 2 ^ 110, -353082960359267 / 2 ^ 110, 141052924422221 / 2 ^ 110]

/-- `[3, 9 / 2 ^ 1]`. -/
def piece0_1 : Piece where
  a := 3
  b := 9 / 2 ^ 1
  c := 15 / 2 ^ 2
  H := 3 / 2 ^ 2
  A := [1292152802610754377100980086126185 / 2 ^ 110, 1457266144819875074348314505425 / 2 ^ 109, -529279256202178450035967715709 / 2 ^ 109, 84408493915813272835706447633 / 2 ^ 108, -100090708845301512525553616821 / 2 ^ 110, 28320519711887358907740819685 / 2 ^ 110, -1940941016723771884675519047 / 2 ^ 108, 1040788810828853721279520687 / 2 ^ 109, -549299449051936026210407505 / 2 ^ 110, 71650850643060118001499367 / 2 ^ 109, -37077693947324577222425943 / 2 ^ 110, 9537136772048617715208719 / 2 ^ 110, -2443032330656811112685381 / 2 ^ 110, 624046019627591588290299 / 2 ^ 110, -79557000934498091846591 / 2 ^ 109, 20262649701821330191097 / 2 ^ 109, -1289500186528767656501 / 2 ^ 107, 2625694521534403589949 / 2 ^ 110, -167108512086195643741 / 2 ^ 108, 170236654442305291687 / 2 ^ 110, -43380980156407169233 / 2 ^ 110, 5531188836847286391 / 2 ^ 109, -705790547787110105 / 2 ^ 108, 360541173082850181 / 2 ^ 109, -184335925045888389 / 2 ^ 110, 23582439890612057 / 2 ^ 109, -377453550529111 / 2 ^ 105, 773985457342051 / 2 ^ 108, -198560248001575 / 2 ^ 108, 101966051419775 / 2 ^ 109, -52406455473633 / 2 ^ 110, 6739240160241 / 2 ^ 109, -3469320325137 / 2 ^ 110, 893686426611 / 2 ^ 110, -230384342097 / 2 ^ 110, 29717172345 / 2 ^ 109, -15343642169 / 2 ^ 110, 247739815 / 2 ^ 106, -1024683057 / 2 ^ 110, 265057495 / 2 ^ 110, -34302677 / 2 ^ 109]
  B := [-20871900713132279369946453705721 / 2 ^ 109, 2606811044367253835206416333537 / 2 ^ 108, -2543476276961842959897580944971 / 2 ^ 110, 608844623267664758066420511947 / 2 ^ 110, -71808480970715675053349591309 / 2 ^ 109, 33497449134838668162393462329 / 2 ^ 110, -7746948726966172037870802641 / 2 ^ 110, 1780422429200104774624009815 / 2 ^ 110, -50915062153886216382381575 / 2 ^ 107, 92882622981452479219757961 / 2 ^ 110, -2641405866247931574857711 / 2 ^ 107, 1199835975954532651858281 / 2 ^ 108, -544294115858039036880227 / 2 ^ 109, 246620812379766046962391 / 2 ^ 110, -27901064172514132085185 / 2 ^ 109, 12607100478620271770315 / 2 ^ 110, -2842699901240135396123 / 2 ^ 110, 639324785521095344871 / 2 ^ 110, -71644761455079111349 / 2 ^ 109, 31968387567060729649 / 2 ^ 110, -7089240816834644755 / 2 ^ 110, 779778729776626463 / 2 ^ 109, -84861483882739025 / 2 ^ 108, 72825365172153141 / 2 ^ 110, -7657961933736609 / 2 ^ 109, 391297186404089 / 2 ^ 107, -306332485908279 / 2 ^ 109, 111573557720097 / 2 ^ 110, -17651159422173 / 2 ^ 110, 1875913861505 / 2 ^ 110, 81434906757 / 2 ^ 109, -99458406467 / 2 ^ 109, 22383517635 / 2 ^ 108, -2027815015 / 2 ^ 106, 10665386331 / 2 ^ 110, -1658633963 / 2 ^ 109, 995804653 / 2 ^ 110, -72918703 / 2 ^ 108, 83915323 / 2 ^ 110, -11908487 / 2 ^ 109, 1672139 / 2 ^ 108]

/-- `[9 / 2 ^ 1, 7]`. -/
def piece0_2 : Piece where
  a := 9 / 2 ^ 1
  b := 7
  c := 23 / 2 ^ 2
  H := 5 / 2 ^ 2
  A := [647715382049599740937995807600827 / 2 ^ 109, 1766427266646790290343876615695 / 2 ^ 111, -876292728735369022878196409797 / 2 ^ 112, 383084853772703964743836996461 / 2 ^ 113, -155879878754637465523693803051 / 2 ^ 114, 1891749793491682910883502321 / 2 ^ 110, -2843747233588496147791325357 / 2 ^ 113, 8345129704748284420108398261 / 2 ^ 117, -1502654368225730080758099835 / 2 ^ 117, 1066945579505900314941154621 / 2 ^ 119, -93639909357815142437532049 / 2 ^ 118, 65164013862079690395157237 / 2 ^ 120, -45027823248391004174683291 / 2 ^ 122, 60427301112315771364303 / 2 ^ 115, -2645343398977636171482225 / 2 ^ 123, 901505524251066977375139 / 2 ^ 124, -306356306214207821019103 / 2 ^ 125, 103877486552928863449837 / 2 ^ 126, -17580760043089904465317 / 2 ^ 126, 23772317051405793278959 / 2 ^ 129, -2007045048095643206899 / 2 ^ 128, 2709270349741941582705 / 2 ^ 131, -913847456703799470975 / 2 ^ 132, 77037134176951951375 / 2 ^ 131, -12986316976170591201 / 2 ^ 131, 35024653283579336239 / 2 ^ 135, -5904272007368548833 / 2 ^ 135, 1990893611039160751 / 2 ^ 136, -20982961264663301 / 2 ^ 132, 226513835815951505 / 2 ^ 138, -152872598873092235 / 2 ^ 140, 6450381287961679 / 2 ^ 138, -17424993510637675 / 2 ^ 142, 1471531381857619 / 2 ^ 141, -1989078967282981 / 2 ^ 144, 672425746837843 / 2 ^ 145, -227409799528481 / 2 ^ 146, 2404352260035 / 2 ^ 142, -26041234536395 / 2 ^ 148, 8817579589339 / 2 ^ 149, -2986830686195 / 2 ^ 150]
  B := [-3469740062203621408173015459339 / 2 ^ 107, 73102900957678001254617844849 / 2 ^ 104, -1556537508630692208942106304355 / 2 ^ 111, 1023881021753957398370404524801 / 2 ^ 113, -83359669666071016800371219747 / 2 ^ 112, 107678568328109189131473738201 / 2 ^ 115, -8631972125027730585226194309 / 2 ^ 114, 2751668331878421277714556863 / 2 ^ 115, -3491745848148761425314713761 / 2 ^ 118, 1103378218344678285195706587 / 2 ^ 119, -21722973884808799529998035 / 2 ^ 116, 54606260718473821537627467 / 2 ^ 120, -17125024622859906201666339 / 2 ^ 121, 5362528329568160659762031 / 2 ^ 122, -3354617327187525850119411 / 2 ^ 124, 1048364683681720884356591 / 2 ^ 125, -163707428606888038771855 / 2 ^ 125, 102203246586376106985309 / 2 ^ 127, -15944877487085465156485 / 2 ^ 127, 2486660430693826304627 / 2 ^ 127, -3101273248693808999347 / 2 ^ 130, 483274377450306822633 / 2 ^ 130, -75271946080424205433 / 2 ^ 130, 11716766367709345083 / 2 ^ 130, -14579460819269885103 / 2 ^ 133, 9062160842391898239 / 2 ^ 135, -2813058256132800847 / 2 ^ 136, 435976379447099955 / 2 ^ 136, -269794279886022349 / 2 ^ 138, 650758601322645 / 2 ^ 132, -6412450232918695 / 2 ^ 138, 3936628804017541 / 2 ^ 140, -1203702899913807 / 2 ^ 141, 732671699012933 / 2 ^ 143, -221710272825353 / 2 ^ 144, 16655052499607 / 2 ^ 143, -19843698561329 / 2 ^ 146, 5845641636585 / 2 ^ 147, -1697617807709 / 2 ^ 148, 30234427617 / 2 ^ 145, -2098418469 / 2 ^ 144]

/-- `[7, 10]`. -/
def piece0_3 : Piece where
  a := 7
  b := 10
  c := 17 / 2 ^ 1
  H := 3 / 2 ^ 1
  A := [1296837104277252199573138597896281 / 2 ^ 110, 570586792973607447720000515873 / 2 ^ 111, -196237957636163841548886648711 / 2 ^ 112, 59676189378602742782538069609 / 2 ^ 113, -16932675331977413455121022911 / 2 ^ 114, 4592827741119788385507422647 / 2 ^ 115, -1206636407671885049140886539 / 2 ^ 116, 38691166059250905082836095 / 2 ^ 114, -77941335689138775764713123 / 2 ^ 118, 4834393210482253603459065 / 2 ^ 117, -37033396359654077928963 / 2 ^ 113, 1150503856349214370452947 / 2 ^ 121, -8654143451921799281377 / 2 ^ 117, 33098433383878643253455 / 2 ^ 122, -3932672735115943080835 / 2 ^ 122, 3719574198389920528087 / 2 ^ 125, -875785566239406319987 / 2 ^ 126, 102731672941808493835 / 2 ^ 126, -3003407602509684941 / 2 ^ 124, 11209715605806456305 / 2 ^ 129, -163066232591740773 / 2 ^ 126, 606104247835589377 / 2 ^ 131, -140575342575178615 / 2 ^ 132, 32559445103575281 / 2 ^ 133, -7532579894025507 / 2 ^ 134, 217620487029909 / 2 ^ 132, -50256779203185 / 2 ^ 133, 92787330578615 / 2 ^ 137, -10700995629907 / 2 ^ 137, 4934310834619 / 2 ^ 139, -142152665751 / 2 ^ 137, 131012819813 / 2 ^ 140, -30180226555 / 2 ^ 141, 217228493 / 2 ^ 137, -1600917105 / 2 ^ 143, 184339319 / 2 ^ 143, -84902563 / 2 ^ 145, 19552473 / 2 ^ 146, -9006023 / 2 ^ 148, 2074271 / 2 ^ 149, -477791 / 2 ^ 150]
  B := [-18940565800080591258169053934171 / 2 ^ 110, 2194603320759215440258346846293 / 2 ^ 110, -126262125751982665339888490617 / 2 ^ 109, 57741133469926312912179387543 / 2 ^ 111, -52500360160446195716897064667 / 2 ^ 114, 11869851667904934525733430085 / 2 ^ 115, -333835022018962216747692785 / 2 ^ 113, 598290223352308131906330735 / 2 ^ 117, -66756658399033873597716687 / 2 ^ 117, 14846583043013825215551461 / 2 ^ 118, -3292004061529691237906099 / 2 ^ 119, 1456110179144587048030987 / 2 ^ 121, -321307932039390495885095 / 2 ^ 122, 17690928534686054302819 / 2 ^ 121, -15559159152349790083345 / 2 ^ 124, 3416320841414034624451 / 2 ^ 125, -93656074630219210113 / 2 ^ 123, 41040588597483320575 / 2 ^ 125, -2246238396555116647 / 2 ^ 124, 7863149612900513265 / 2 ^ 129, -1719451488728997065 / 2 ^ 130, 375838645950330243 / 2 ^ 131, -10265462078898379 / 2 ^ 129, 17939950216350121 / 2 ^ 133, -1959084578786309 / 2 ^ 133, 855602076324203 / 2 ^ 135, -186809600474443 / 2 ^ 136, 20391176261447 / 2 ^ 136, -2225530236005 / 2 ^ 136, 1942947229043 / 2 ^ 139, -212001546683 / 2 ^ 139, 361383281 / 2 ^ 133, -10091016205 / 2 ^ 141, 2200863473 / 2 ^ 142, -959759991 / 2 ^ 144, 104599623 / 2 ^ 144, -45581497 / 2 ^ 146, 9926987 / 2 ^ 147, -540197 / 2 ^ 146, 470039 / 2 ^ 149, -51087 / 2 ^ 149]

/-- `[10, 15]`. -/
def piece0_4 : Piece where
  a := 10
  b := 15
  c := 25 / 2 ^ 1
  H := 5 / 2 ^ 1
  A := [1297495861367492728941307381499251 / 2 ^ 110, 366556962707709915008831288687 / 2 ^ 112, -86858394295622811965475694795 / 2 ^ 113, 9121218213585100827429409633 / 2 ^ 113, -447770701349704554317269477 / 2 ^ 112, 10776825220861161992867041475 / 2 ^ 120, -982687679678368354923206147 / 2 ^ 120, 1401338492644156946146870571 / 2 ^ 124, -490775364229235528397693873 / 2 ^ 126, 169438489117475018603373881 / 2 ^ 128, -57813973497799830282226767 / 2 ^ 130, 2441660316895715464838063 / 2 ^ 129, -3272306978591313830640121 / 2 ^ 133, 544267597886622635819495 / 2 ^ 134, -179927535121916338854233 / 2 ^ 136, 236637891895208414777551 / 2 ^ 140, -9679471819543630616725 / 2 ^ 139, 25233364748861177235765 / 2 ^ 144, -8192101498781216214063 / 2 ^ 146, 1325421921115242172033 / 2 ^ 147, -427631972009856045459 / 2 ^ 149, 137610730542363786735 / 2 ^ 151, -44179712508408756971 / 2 ^ 153, 28308712573116489089 / 2 ^ 156, -4526370026504484405 / 2 ^ 157, 1445067669860256207 / 2 ^ 159, -921320711437536681 / 2 ^ 162, 36663700815404581 / 2 ^ 161, -23316627683675205 / 2 ^ 164, 29625390678690291 / 2 ^ 168, -4700680478318893 / 2 ^ 169, 2980918338777841 / 2 ^ 172, -944456930852807 / 2 ^ 174, 299035701382955 / 2 ^ 176, -23656216377435 / 2 ^ 176, 14963329721171 / 2 ^ 179, -4730188865387 / 2 ^ 181, 1494685996263 / 2 ^ 183, -944266038175 / 2 ^ 186, 74543762889 / 2 ^ 186, -47065046465 / 2 ^ 189]
  B := [-12932987075907401870760058988459 / 2 ^ 110, 513569694903520665828680721675 / 2 ^ 109, -650342808129612458044798199847 / 2 ^ 113, 410399247282003679713829269197 / 2 ^ 116, -64539691219204535067616683127 / 2 ^ 117, 20237770689331346785936357761 / 2 ^ 119, -12655706484371927225673612369 / 2 ^ 122, 1973251344393340226425171963 / 2 ^ 123, -1227568669329244533078843671 / 2 ^ 126, 5952254675112496348601729 / 2 ^ 122, -117959616910874271214579827 / 2 ^ 130, 36453030537411516319362869 / 2 ^ 132, -1405537184434457649603623 / 2 ^ 131, 3462555484461523772990389 / 2 ^ 136, -1064611649500970779501459 / 2 ^ 138, 81717834167215366947675 / 2 ^ 138, -50116567082772347880033 / 2 ^ 141, 15350369453616458339367 / 2 ^ 143, -9393772958435846706199 / 2 ^ 146, 1435827118387822433605 / 2 ^ 147, -438569842235265826967 / 2 ^ 149, 4183215109780508085 / 2 ^ 146, -81664510451733810197 / 2 ^ 154, 12448073763270315609 / 2 ^ 155, -3793039067355311379 / 2 ^ 157, 2310557324408864509 / 2 ^ 160, -351743129747581851 / 2 ^ 161, 107059820370216077 / 2 ^ 163, -8144221423867479 / 2 ^ 163, 4955216820240975 / 2 ^ 166, -6028670243114867 / 2 ^ 170, 1833369232303185 / 2 ^ 172, -557467787139985 / 2 ^ 174, 169488880827859 / 2 ^ 176, -12881392438179 / 2 ^ 176, 978929982081 / 2 ^ 176, -2380473312461 / 2 ^ 181, 1447079119173 / 2 ^ 184, -439816654287 / 2 ^ 186, 133669871013 / 2 ^ 188, -40623639475 / 2 ^ 190]

/-- `[15, 22]`. -/
def piece0_5 : Piece where
  a := 15
  b := 22
  c := 37 / 2 ^ 1
  H := 7 / 2 ^ 1
  A := [162226095078341357146669309959809 / 2 ^ 107, 114268806335386113943943892227 / 2 ^ 112, -36837547925383517047127149489 / 2 ^ 114, 1317618729100788236051707519 / 2 ^ 113, -1411905263968350129512512203 / 2 ^ 117, 362615717477591248285524501 / 2 ^ 119, -180849423307613276451969413 / 2 ^ 122, 44122253075518972613247761 / 2 ^ 124, -10583653095589346500298173 / 2 ^ 126, 1252240872628780634873791 / 2 ^ 127, -146520319817613083946115 / 2 ^ 128, 67937517489821477626175 / 2 ^ 131, -31251050865537396247343 / 2 ^ 134, 7138474287570841703027 / 2 ^ 136, -202605625420958568397 / 2 ^ 135, 366086019866525325493 / 2 ^ 140, -41148882590205366647 / 2 ^ 141, 9211770959953027423 / 2 ^ 143, -2054439093795226587 / 2 ^ 145, 913266782932293461 / 2 ^ 148, -202364669559705445 / 2 ^ 150, 2794702879691795 / 2 ^ 148, -9855246794377349 / 2 ^ 154, 270879061014167 / 2 ^ 153, -29717642147375 / 2 ^ 154, 104123918430623 / 2 ^ 160, -22760548154981 / 2 ^ 162, 4966989439887 / 2 ^ 164, -1082277475179 / 2 ^ 166, 235488876531 / 2 ^ 168, -25586191801 / 2 ^ 169, 5553253251 / 2 ^ 171, -2407883329 / 2 ^ 174, 260744953 / 2 ^ 175, -112834617 / 2 ^ 178, 24392465 / 2 ^ 180, -164651 / 2 ^ 177, 1137221 / 2 ^ 184, -245285 / 2 ^ 186, 52871 / 2 ^ 188, -11389 / 2 ^ 190]
  B := [-4377944576836813461849316831027 / 2 ^ 109, 1886785880552227323328947912669 / 2 ^ 112, -50738574713585221381249788581 / 2 ^ 111, 5448927049484534799668931395 / 2 ^ 112, -18695909825141460302058381021 / 2 ^ 118, 2001532792915186333253958449 / 2 ^ 119, -855831724212908135975260003 / 2 ^ 122, 182706516898859260374604005 / 2 ^ 124, -9737583118069632887309557 / 2 ^ 124, 8292436130295852873382857 / 2 ^ 128, -881576430164133821024575 / 2 ^ 129, 46802406042215359420007 / 2 ^ 129, -39708231623564550424931 / 2 ^ 133, 16825618195156052401491 / 2 ^ 136, -445116369942799860205 / 2 ^ 135, 752855951895487720135 / 2 ^ 140, -159015529358409119513 / 2 ^ 142, 16777978832032166537 / 2 ^ 143, -7074973991232797749 / 2 ^ 146, 372620973291442325 / 2 ^ 146, -313760640074810485 / 2 ^ 150, 16500580366768565 / 2 ^ 150, -1734361691568721 / 2 ^ 151, 2914937086332697 / 2 ^ 156, -153008798354397 / 2 ^ 156, 64218344853727 / 2 ^ 159, -26939176851869 / 2 ^ 162, 5647786283321 / 2 ^ 164, -1183549161645 / 2 ^ 166, 123963282899 / 2 ^ 167, -25958067449 / 2 ^ 169, 10867688921 / 2 ^ 172, -2274258771 / 2 ^ 174, 475797247 / 2 ^ 176, -99516285 / 2 ^ 178, 20809741 / 2 ^ 180, -2175299 / 2 ^ 181, 909389 / 2 ^ 184, -95027 / 2 ^ 185, 19857 / 2 ^ 187, -8297 / 2 ^ 190]

/-- `[22, 30]`. -/
def piece0_6 : Piece where
  a := 22
  b := 30
  c := 26
  H := 4
  A := [324484878700228878440630558927083 / 2 ^ 108, 5168690706127237862212087253 / 2 ^ 109, -4756349937370138952489369303 / 2 ^ 113, 1943825323244577749014618135 / 2 ^ 116, -372099775563906544925968231 / 2 ^ 118, 34165326216263525224940867 / 2 ^ 119, -12190620916629074869769901 / 2 ^ 122, 2129001976468060703396205 / 2 ^ 124, -365753413249189263938099 / 2 ^ 126, 62017500228861805871561 / 2 ^ 128, -2600945877477683632873 / 2 ^ 128, 1729768257495795556601 / 2 ^ 132, -285423508388946044623 / 2 ^ 134, 46790099675881234737 / 2 ^ 136, -1906711328039168003 / 2 ^ 136, 1236966983753509539 / 2 ^ 140, -49931753222171931 / 2 ^ 140, 16060318558274055 / 2 ^ 143, -2573604107764353 / 2 ^ 145, 822140594682271 / 2 ^ 148, -130928306915055 / 2 ^ 150, 20794284582765 / 2 ^ 152, -1647189995179 / 2 ^ 153, 130181029829 / 2 ^ 154, -2566678983 / 2 ^ 153, 12929529619 / 2 ^ 160, -2031664275 / 2 ^ 162, 79675351 / 2 ^ 162, -24957353 / 2 ^ 165, 7806041 / 2 ^ 168, -152385 / 2 ^ 167, 190139 / 2 ^ 172, -7405 / 2 ^ 172, 4609 / 2 ^ 176, -179 / 2 ^ 176, 111 / 2 ^ 180, -17 / 2 ^ 182, 3 / 2 ^ 184, 0, 0, 0]
  B := [-6235356658633600886677203137083 / 2 ^ 110, 957636259055660724726804306257 / 2 ^ 112, -73475150915441721643504042295 / 2 ^ 113, 22530703079548798053986902667 / 2 ^ 116, -431447280597013253762827653 / 2 ^ 115, 132082220604683547451360585 / 2 ^ 118, -10100668605978209963324071 / 2 ^ 119, 1543622073381752238771255 / 2 ^ 121, -1885746718314766648910689 / 2 ^ 126, 143871292683328901227389 / 2 ^ 127, -21936661874170890775993 / 2 ^ 129, 6684672079623583324619 / 2 ^ 132, -508886242882744518431 / 2 ^ 133, 38713322448729818255 / 2 ^ 134, -11772470682596908205 / 2 ^ 137, 3577591298987342473 / 2 ^ 140, -543260836474427933 / 2 ^ 142, 20611014296820005 / 2 ^ 142, -12504098675528565 / 2 ^ 146, 1895380184296153 / 2 ^ 148, -17946511396101 / 2 ^ 146, 43478270800913 / 2 ^ 152, -6579938380387 / 2 ^ 154, 497653899817 / 2 ^ 155, -150483058279 / 2 ^ 158, 1421349691 / 2 ^ 156, -858827055 / 2 ^ 160, 518716645 / 2 ^ 164, -78292905 / 2 ^ 166, 11812729 / 2 ^ 168, -890823 / 2 ^ 169, 268623 / 2 ^ 172, -5061 / 2 ^ 171, 6101 / 2 ^ 176, -919 / 2 ^ 178, 69 / 2 ^ 179, -21 / 2 ^ 182, 3 / 2 ^ 184, 0, 0, 0]

/-- The pieces before the last. -/
def pieces : List Piece := [piece0_0, piece0_1, piece0_2, piece0_3, piece0_4, piece0_5]

/-- The last piece, `[22, 30]`. -/
def last : Piece := piece0_6

/-- Hankel's expansion with 60 terms on `[30, ∞)`. -/
def asym : AsymPiece where
  X := 30
  A := asymA 0 60
  B := asymB 0 60
  m := 59

theorem sys : PQSystem ((1 / 4 : ℚ) : ℝ) P0 Q0 P0d Q0d := by
  intro x hx
  have := P0_system x hx
  push_cast
  exact this

set_option maxRecDepth 100000 in
theorem start : rootE0 ((1 / 4 : ℚ) : ℝ) P0 Q0 P0d Q0d (firstPiece pieces last)
    (firstPiece pieces last).a ≤ ((1 / 2 ^ 83 : ℚ) : ℝ) := by
  obtain ⟨e1, e2, e3, e4⟩ := start_values0
  have hf : firstPiece pieces last = piece0_0 := rfl
  have ha : ((piece0_0.a : ℚ) : ℝ) = 2 := by norm_num [piece0_0]
  have hc : (2 : ℝ) - ((piece0_0.c : ℚ) : ℝ) = (((2 - piece0_0.c : ℚ)) : ℝ) := by push_cast; ring
  rw [hf, ha]
  have h := root0_le_encl ((1 / 4 : ℚ) : ℝ) 2
    (e1.sub (Encl.exact (evalQ piece0_0.A (2 - piece0_0.c))))
    (e2.sub (Encl.exact (evalQ piece0_0.B (2 - piece0_0.c))))
    (e3.sub (Encl.exact (evalQ (derivP piece0_0.A) (2 - piece0_0.c))))
    (e4.sub (Encl.exact (evalQ (derivP piece0_0.B) (2 - piece0_0.c))))
    (s := 33 / 32) (by norm_num) (by norm_num) (by norm_num)
  simp only [rootE0, root0, Piece.fA, Piece.fB, Piece.fA1, Piece.fB1, hc, ← evalQ_cast]
  refine h.trans ?_
  exact Rat.cast_le.mpr (by decide +kernel)

theorem chain_ok : chain0 (1 / 4) (33 / 32) (1 / 2 ^ 80) pieces last (1 / 2 ^ 83) = true := by
  decide +kernel

theorem asym_ok : asym.ok (1 / 4) = true := by
  decide +kernel

theorem final_ok : chainEnd0 (1 / 4) (33 / 32) pieces last (1 / 2 ^ 83) + jumpAsym0 (33 / 32) last asym +
    asymTail (1 / 4) asym ≤ 1 / 2 ^ 80 := by
  decide +kernel

theorem two_le_a : ∀ pc ∈ pieces ++ [last], (2 : ℚ) ≤ pc.a := by decide +kernel

/-- `P0` and `Q0` within `2 ^ -80` of the piece's polynomials on `[2, 30]`. -/
theorem pieces_bound :
    ∀ pc ∈ pieces ++ [last], ∀ x ∈ Icc (pc.a : ℝ) pc.b,
      |P0 x - pc.fA x| ≤ 1 / 2 ^ 80 ∧ |Q0 x - pc.fB x| ≤ 1 / 2 ^ 80 := by
  obtain ⟨hall, -⟩ := chain0_sound (1 / 4) (by norm_num) sys (33 / 32) (1 / 2 ^ 80) pieces last (1 / 2 ^ 83)
    chain_ok start
  intro pc hpc x hx
  have h := hall pc hpc x hx
  have h2 : (2 : ℝ) ≤ x := le_trans (by exact_mod_cast two_le_a pc hpc) hx.1
  have e := abs_le_root0 (((1 / 4 : ℚ)) : ℝ) x (P0 x - pc.fA x) (Q0 x - pc.fB x) (P0d x - pc.fA1 x)
    (Q0d x - pc.fB1 x) (by norm_num)
  simp only [rootE0, root0] at h
  have hδ : ((1 / 2 ^ 80 : ℚ) : ℝ) = 1 / 2 ^ 80 := by norm_num
  exact ⟨(e.1.trans h).trans hδ.le, (e.2.trans h).trans hδ.le⟩

/-- `P0` and `Q0` within `2 ^ -80` of Hankel's expansion with 60 terms on `[30, ∞)`. -/
theorem asym_bound (x : ℝ) (hx : 30 ≤ x) :
    |P0 x - asym.fA x| ≤ 1 / 2 ^ 80 ∧ |Q0 x - asym.fB x| ≤ 1 / 2 ^ 80 := by
  obtain ⟨-, hend⟩ := chain0_sound (1 / 4) (by norm_num) sys (33 / 32) (1 / 2 ^ 80) pieces last (1 / 2 ^ 83)
    chain_ok start
  have hX : ((asym.X : ℚ) : ℝ) = 30 := by norm_num [asym]
  have hb : ((last.b : ℚ) : ℝ) = asym.X := by norm_num [last, piece0_6, asym]
  have hj := jumpAsym0_le (1 / 4) P0 Q0 P0d Q0d (33 / 32) last asym (by norm_num [asym]) (by norm_num)
    (by norm_num [asym])
  have ha := asym_bound0 (1 / 4) (by norm_num) sys asym asym_ok x (by rw [hX]; exact hx)
  have hf : (((chainEnd0 (1 / 4) (33 / 32) pieces last (1 / 2 ^ 83) + jumpAsym0 (33 / 32) last asym +
      asymTail (1 / 4) asym : ℚ)) : ℝ) ≤ ((1 / 2 ^ 80 : ℚ) : ℝ) := Rat.cast_le.mpr final_ok
  push_cast at hf
  rw [hb] at hend
  have h30 : (2 : ℝ) ≤ x := by linarith
  have e := abs_le_root0 (((1 / 4 : ℚ)) : ℝ) x (P0 x - asym.fA x) (Q0 x - asym.fB x) (P0d x - asym.fA1 x)
    (Q0d x - asym.fB1 x) (by norm_num)
  simp only [root0] at ha hj
  simp only [rootE0, root0] at hend hj
  constructor <;> linarith [e.1, e.2]

#print axioms pieces_bound
#print axioms asym_bound

end LeanExe.ProofKit.BesselLarge0