*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Formal_Power_Series.thy and inversion*From*: Raymond Rogers <raymond.rogers72 at gmail.com>*Date*: Fri, 17 Mar 2017 10:43:52 -0400*In-reply-to*: <88e1a02a-0d82-b5e4-b9fd-e81d241d830b@in.tum.de>*References*: <4b1d3bc7-f929-46d9-1182-9b8485c956ff@gmail.com> <88e1a02a-0d82-b5e4-b9fd-e81d241d830b@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.7.0

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?

----

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

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.

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)

----

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.

----

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: https://link.springer.com/article/10.1007/s10817-010-9195-9 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.

----

For instance the items: (T+) Bizley Riordan Arrays in GouldBk.pdf

Cheers, Manuel

---- Thanks again for the reply. Ray

**Follow-Ups**:**Re: [isabelle] Formal_Power_Series.thy and inversion***From:*Manuel Eberl

**References**:**[isabelle] Formal_Power_Series.thy and inversion***From:*Raymond Rogers

**Re: [isabelle] Formal_Power_Series.thy and inversion***From:*Manuel Eberl

- Previous by Date: [isabelle] *Extended submission deadline* - 10th Conference on Intelligent Computer Mathematics - CICM 2017
- Next by Date: Re: [isabelle] Formal_Power_Series.thy and inversion
- Previous by Thread: Re: [isabelle] Formal_Power_Series.thy and inversion
- Next by Thread: Re: [isabelle] Formal_Power_Series.thy and inversion
- Cl-isabelle-users March 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list