[isabelle] Formal_Power_Series.thy and inversion



While working my way through GouldBk.pdf with FormaI_Power_Series.thy I am at the Lagrange Inversion theorems and I am stuck. At present the problem is with:

fps_inv g  -- when g is delta, i.e. g=0 + a_1*X+a_2*X^2 ...
This is defined as fps=0.0.0...

Which I don't understand. How is that justified? That change is referred to in the 2016 news (more or less). This seems to be a major roadblock; alternate interpretations are that the "res" function of Laurent series are missing. Amine Chaieb referred to a Formal Power Series structure that included Laurent Series in 2009 talk, but I can't seem to find the talk or any reference in Isabelle . Does anybody have a pointer?
I can implement Niven's Laurent extension in
https://www.maa.org/sites/default/files/pdf/upload_library/22/Ford/IvanNiven.pdf
but that would delay any interesting work even further (:
I tried another approach but the prematurely declaring zero and not waiting for cancellation possibilities has struck at me again. The whole term does have a cancellation if the term is multiplied by X and yields fps $0 =1; at least from an outside algebra point of view.
A particularly simple Lagrange rendering is at:
http://users.math.msu.edu/users/magyar/Math880/Lagrange.pdf
(with a few typos).
Or I can try the Umbral calculus version but that also seems as hard as Niven.

Ray

--
From the QED manifesto:https://www.cs.ru.nl/~freek/qed/qed.html
"
Mathematics is arguably the foremost creation of the human mind.
"





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.