While working towards the Lagrange Inversion theorem in Isabelle to do some formal combinatorics I am following:
http://users.math.msu.edu/users/magyar/Math880/Lagrange.pdf
I get to Lemma 1, ii .
$\left[x^{-1}\right]f\left(x\right)^{i}f'\left(x\right)=\begin{cases}
\begin{array}{cc}
1 & if\,i=-1\\
0 & else
\end{array}\end{cases}$
And the subsequent proof seems good.
I changed the $[x^{-1}]$ to $[x^{0}]\cdot{x} $ to avoid negative indexing,
and constructed the following Isabelle program.
imports Complex_Main Binomial
"~~/src/HOL/Library/Formal_Power_Series"
lemma Ias_Lag_880_ii:
fixes f g::"real fps"
assumes "f $ 0 \noteq 0"
assumes "g = X\*f"
assumes "i=(-1)"
shows "(((X*(g^i)*(fps_deriv g))$( 0)) = 0)"
by auto
Which works for natural i and is true.
But it also "proves" the proposition (=0) when i=-1 as above.
I am really interested in why Isabelle contradicts the paper or, more probably, what I am doing wrong. I did some work by hand and it agrees with the paper.
The problem was "(fps_inv g)" with g $\in \delta series$ ; i.e. g=0+a_1*x+a_2*x^2 ... is defined as the zero fps. This was apparently done quite deliberately citing some ring/field theory in the 2016 news section. This is unfathomable to me. I thought of a couple of ways to fix it but none guaranteed consistency with existing theory structure. For instance adding an infinitesimal to the fps ring. This works fine for addition, subtraction, and multiplication; but division seems iffy unless I define 1/eps = "1/eps" or some such. And how would the rest of structures adapt to that?
I can go back to Niven's technique of extension to Laurent series.
https://www.maa.org/sites/default/files/pdf/upload_library/22/Ford/IvanNiven.pdf or adapt something from the umbral calculus. I basically don't see how to go forward, around Lagrange's Inversion theorems for a large number of standard combinatorial proofs.
I am going to ask on the ci-isabelle-users mailing list.
Constructive comments more than welcome
Ray