# Re: [isabelle] Formal_Power_Series.thy and inversion

```Thanks for the attention and reply!
Since the response is long and scattered, I have marked my replies by "----"

On 03/17/2017 03:50 AM, Manuel Eberl wrote:
```
```Hallo,

On 16/03/17 23:27, Raymond Rogers wrote:
```
```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...
```
```What do you mean by âdeltaâ? Are you confused by the fact that fps_inv
only works when the 0th coefficient of the FPS is zero? If yes, that
also confuses me (I know nothing about the Lagrange inversion theorem),
but Wikipedia also does it that way [1], and the document you linked [2]
also demands that the series have constant coefficient zero. (âLet f(x),
g(x) â xâãxãâ)

So perhaps that's just the way it is?
```
```----
```
"delta" is often used to designate series g=a_0 + a_1*X+a_2*X^2 ; where a_0=0 and a_1 !=0. Yes, but "confusion" isn't the right word; why do it? If I am told that division by zero is illegal then doing it should error out. If there is a reason that Formal...thy returns the absolute zero fps? Can I get a reference/reason/Axiom? I am not even sure that decision is consistent; as evidenced by the fact that cancellations are not considered first (maybe). These concerns are only _motivated_ by Lagrange inversion, the real concern is consistency with normal mathematics.
``` In fact it looks like a contradiction: take X*(fps_inv X).
If I cancel first then I get =1
If I evaluate (fps_inv X) first I get =0
```
How can I trust a system where 0=1, depending upon order evaluation? I mentally tried alternate structures controlling order but rapidly got bogged down because of the thought of things occurring deeper inside of other uses/lemma, and having no underlying consistent guidelines. I list two instances of complex reasoning/manipulation from GouldBk.pdf below. I can supply references to many... other papers using similar conventions. In addition the forms of the "Lagrange Inversion" are many and varied; more like distant cousins of one another than close kin.
```
```
```That change is referred to in the 2016 news (more or less).
```
```I'm not sure what you mean. Do you mean this?

* Library/Formal_Power_Series: proper definition of division (with
remainder) for formal power series; instances for Euclidean Ring and
GCD.

That has nothing to do with fps_inv. Or do you mean something else?
```
```----
Yes and the following:
Classes division_ring, field and linordered_field always demand
"inverse 0 = 0". Given up separate classes division_ring_inverse_zero,
field_inverse_zero and linordered_field_inverse_zero. INCOMPATIBILITY.
```
Even if I accept the logic for rings and fields (which as of now I don't really see why I should) we have the fact that the fps theory is setting a _non_zero_ item to zero during inversion. Rephrasing: this is setting an additional equivalence class operation in place. I haven't seen this in my studies and classes; but it's been some time and this particular case didn't get mentioned as I recall.
```

```
```This seems to be a major roadblock; alternate  interpretations are that the
"res" function of Laurent series are missing.
```
```Indeed we don't have Laurent series yet. We do have fraction fields,
which can be used to derive Laurent Series quite easily and I actually
already did that once, but it was only a small toy theory with no real
use, so I never uploaded it anywhere. (it has succumbed to bit rot in
the mean time and will need some repair before it works again)
```
```----
```
Could you send me a copy? Hints are appreciated since I am a newbie. I promise not to nitpick :)
```
In any case, I doubt it will be necessary for this. My feeling is that
Laurent series might make the presentation of the inversion theorem
nicer,  but that they are not really necessary.
```
```----
```
Possibly, but when used in combinatorial analysis, like GouldBk.pdf, there is a strong dependency upon one or more of the various forms. So I am trying to prove the various forms are compatible with compositional inverses; which is basically what Lagrange inversion is. I can't produce compatibility unless I can cancel before inversion: per X*1/X . At least so far. I can try to replace X* with explicit shifts though. (?)
```
```
```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.
```
```I don't know of anything like this. I'm pretty sure we have no Laurent
series in Isabelle.
```
```-----
Her article is behind a paywall I can't afford:
and her "talk" is like all talk; blowing in the wind never to be seen again.
http://talks.cam.ac.uk/talk/index/16357

```
```

The main problem right now is that I didn't understand at all what
result you need and what you need it for.
```
```----
```
Like I mentioned above: the various structural forms of the Lagrange Inversion are directly relied on for Combinatorial, Umbral, and Method Coefficients analysis. So it behooves me to make sure they are consistent with any proof method I use.
```For instance the items:
(T+) Bizley
Riordan Arrays
in GouldBk.pdf

```
```
Cheers,

Manuel
```
```----