Email Gateway (Aug 22 2022 at 15:15): Email Gateway (Aug 22 2022 at 15:15):From: Raymond Rogers <raymond.rogers72@gmail.com>
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_1X+a_2X^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
Email Gateway (Aug 22 2022 at 15:15):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
On 16/03/17 23:27, Raymond Rogers wrote:
fps_inv g -- when g is delta, i.e. g=0 + a_1X+a_2X^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?
That change is referred to in the 2016 news (more or less).
I'm not sure what you mean. Do you mean this?
That has nothing to do with fps_inv. Or do you mean something else?
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.
The main problem right now is that I didn't understand at all what
result you need and what you need it for.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 15:15):From: Manuel Eberl <eberlm@in.tum.de>
I forgot the links:
[1] https://en.wikipedia.org/wiki/Lagrange_inversion_theorem
[2] http://users.math.msu.edu/users/magyar/Math880/Lagrange.pdf
Email Gateway (Aug 22 2022 at 15:15):From: Raymond Rogers <raymond.rogers72@gmail.com>
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_1X+a_2X^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_1X+a_2X^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:
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.
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
Thanks again for the reply.
Ray
Email Gateway (Aug 22 2022 at 15:15):From: Manuel Eberl <eberlm@in.tum.de>
First of all: There are no non-total functions in HOL. If you take the
first element of the empty list, if you divide by zero, if you evaluate
0^0, you always get /some/ result; there is just no other way in that
logic. The question is: What result do you get?
One approach is to leave it unspecified (e.g. using HOL's "undefined" or
something like that), then you simply don't know or care (logically)
what that element is. But it still /is/ an element (i.e. 1/0 is a real
number, you just don't know which number), and it's always the same
number, so e.g. "1/0 - 1/0 = 0" holds.
In my experience, it is usually a lot less painful to adopt conventions
like "x / 0 = 0 for all x". This diverges from mathematical convention,
but as I said, you simply cannot have ‘completely undefined’ expressions
in HOL, and if you must return some value, you might as well choose a
convenient one. Choosing "x / 0 = 0" has the advantage that a number of
nice properties of division still hold without additional conditions,
which makes rewriting arithmetic terms less painful. Of course, as an
Isabelle user, you have to /know/ what this means.
A similar issue is the sum over an infinite set, which is always 0 in
Isabelle. One may naïvely expect that "(∑n∈{1..}. 1/n^2) = π²/6", but it
is in fact zero by definition, and if one wants an actual infinite sum,
one has to use another concept of "sum", e.g. "suminf"/"sums" or the
measure-theoretic one.
Therefore, the justification of choosing fps_inv as 0 for inputs that
don't have an inverse is simply that it you can't return a "proper"
result, so you might as well return a "convenient" dummy result.
Second, I think you may be confused by what fps_inv actually is. fps_inv
is the /compositional/ inverse of formal power series. Therefore,
cancelling "X * fps_inv X" to "1" makes no sense to me at all. In fact,
"fps_inv X = X", and "X" plugged into "X" yields "X", which is the
compositional identity, as expected.
Perhaps you mean the /multiplicative/ inverse? This is simply "inverse
X", which is defined like this:
fun natfun_inverse:: "'a fps ⇒ nat ⇒ 'a"
where
"natfun_inverse f 0 = inverse (f$0)"
| "natfun_inverse f n = - inverse (f$0) * sum (λi. f$i * natfun_inverse
f (n - i)) {1..n}"
definition fps_inverse_def: "inverse f = (if f $ 0 = 0 then 0 else
Abs_fps (natfun_inverse f))"
Thus, "inverse X" is indeed 0 in Isabelle. This is because X simply does
not have an inverse in the ring of formal power series and we have to
return something.
take X*(fps_inv X).
If I cancel first then I get =1
If I evaluate (fps_inv X) first I get =0
Okay, so you probably again mean "X * inverse X" here. You are correct
that you can evaluate "inverse X" to "0", and then you get "X * 0 = 0".
However, you can /not/ cancel "X * inverse X" to get "1". The law "f *
inverse f = 1" only holds if "f $ 0 ≠ 0", as you can see in this theorem:
lemma inverse_mult_eq_1':
assumes f0: "f$0 ≠ (0::'a::field)"
shows "f * inverse f = 1"
You can't do any better than this if you want to stay in the type "'a
fps". If you want multiplicative inverses for all non-zero formal power
series, you have to go to the ring of formal Laurent series, do your
stuff there, and then go back to the ring of formal power series once
you're done. This is perhaps a bit odd for a mathematician, but I'm
afraid that's how things are in a typed logic like HOL.
However, note that you can write things like "X^2 / X" in the ring of
formal power series (as long as the coefficients are a field), which
evaluates to "X" as expected. For "'a :: field fps", a power series
divides another iff the subdegree of the former is smaller than that of
the latter, and we have a full Euclidean ring structure on FPSs, i.e. we
have well-behaved division and remainder operations "div" and "mod" just
like on integers or polynomials. I think this is probably enough and
probably less painful than going to formal Laurent series.
Note that, due to somewhat unfortunate notation, "f / g" on formal power
series is not the same as "f * inverse g". It is the same if g is a
unit, but otherwise, "f / g" is essentially what you get when you
compute "f / g" in the ring of formal Laurent series and then cut off
all the terms with negative exponents, and "f mod g" is the remainder,
i.e. "f - (f / g) * g".
If you only want to divide by powers of X, you can also use fps_shift.
How can I trust a system where 0=1, depending upon order evaluation?
Well, you can't. Luckily, Isabelle is (hopefully) not such a system. It
is a core principle of Isabelle that definitions should never be able to
introduce inconsistencies.
Could you send me a copy?
It's currently broken in ways that I don't understand, but I'll attempt
to fix it and then I can send it to you. I'm not sure if it will be very
helpful; it was never more than a small experiment.
Her article is behind a paywall I can't afford:
https://link.springer.com/article/10.1007/s10817-010-9195-9
I know Amine's article and it really doesn't say very much about Laurent
series. It essentially describes that one can define them as "'a fps
fract" in the way I did in my experiment and nothing more. I don't think
Amine ever actually had the time to build a library of facts about
Laurent series.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 15:16):From: Raymond Rogers <raymond.rogers72@gmail.com>
1)Thanks, I am trying some things, like perhaps defining a finite fps
type and copying in polynomial gcd. Although fps_gcd might cover some
things.
2) "
Second, I think you may be confused by what fps_inv actually is. fps_inv
is the /compositional/ inverse of formal power series. Therefore,
cancelling "X * fps_inv X" to "1" makes no sense to me at all. In fact,
"fps_inv X = X", and "X" plugged into "X" yields "X", which is the
compositional identity, as expected.
"
Duh... really, really ... my bad.
I have been doing that occasionally and really should have paid more
attention. I did know better.
3) Shifts do seem to work on some Lagrange Inversion expressions.
Although I haven't tried it in the proofs yet. Just as a replacement
for division & cancellation or vice-versa.
Thanks for the help!
Ray
Email Gateway (Aug 22 2022 at 15:16):From: Manuel Eberl <eberlm@in.tum.de>
We do have a "finite fps" type; it is called "poly", and the connection
between polynomials and formal power series is made in
"~~/src/HOL/Library/Polynomial_FPS.thy"
I also still have a formalisation of executable rational formal power
series lying around here; I really should clean up and commit this stuff
soon.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 15:16):From: Raymond Rogers <raymond.rogers72@gmail.com>
So it would seem that res(f/g) i.e. (f/g) $ -1
would be ((X*f)/g) $ 0
?
I'll run some tests.
Ray
Email Gateway (Aug 22 2022 at 15:16):From: Raymond Rogers <raymond.rogers72@gmail.com>
And we have a measure of success!
lemma Ias_Lag_880_ii:
fixes f g::"real fps"
assumes "f$0 \<noteq>0"
assumes "g = X*f"
shows "((( (fps_deriv g)*X)/g)$ 0) = 1"
using assms(1) assms(2) by auto
and --shows "((( (fps_deriv g)*X)/g)$ 0) = 0
fails!
Forgive any inelegance in my syntax.
Now all we need is to rearrange the above as a function:
fps->fps->element of field
res f g ->(X*f)/g %0
This seems to match the requirements of most combinatorial theorems;
although it _looks_ like we could generalize a little.
A bit happier!
Ray
Last updated: Nov 21 2024 at 12:39 UTC