[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
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:
(with a few typos).
Or I can try the Umbral calculus version but that also seems as hard as
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