Email Gateway (Aug 22 2022 at 16:21): Email Gateway (Aug 22 2022 at 16:21):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
yes, of course, luckily in this case they are all positive
Thanks
Angeliki
Email Gateway (Aug 22 2022 at 16:22):From: Wenda Li <wl302@cam.ac.uk>
Hi Isabelle experts,
I am considering to do some developments that may involve infinite products. By briefly checking the Isabelle library, it seems that we have infinite sums in HOL/Series.thy:
definition sums :: "(nat ⇒ 'a::{topological_space, comm_monoid_add}) ⇒ 'a ⇒ bool"
(infixr "sums" 80)
where "f sums s ⟷ (λn. ∑i<n. f i) ⇢ s”
And some developments about infinite products in HOL/Analysis/Infinite_Product.thy:
definition convergent_prod :: "(nat ⇒ 'a :: {t2_space,comm_semiring_1}) ⇒ bool" where
"convergent_prod f ⟷ (∃M L. (λn. ∏i≤n. f (i+M)) ⇢ L ∧ L ≠ 0)"
I was wondering if there is any other theory about infinite products, as HOL/Analysis/Infinite_Product.thy does not provide functions corresponding to @{term “sums”} and @{term “suminf”}.
Thanks,
Wenda
Email Gateway (Aug 22 2022 at 16:23):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I'm pretty sure there isn't. I surveyed the material a while ago for my
work on Dirichlet series and Euler product expansions and found that
there was very little there.
I did not introduce something like "sums" for infinite products back
then because 1. I could not think of a good name and 2. every additional
constant you introduce means you have to provide a lot of additional
theorems to make it practically usable, and that was not something I
wanted to do at the time. Besides, one can phrase simply use "filterlim"
with little overhead.
It would be nice to have more on this, but I'm not sure how to do it.
Often, one could probably reduce infinite products to infinite sums via
the real or complex logarithm, but that seems like a bit of a hack
because it only works for real and complex numbers.
Unfortunately, I know little about this and don't know if it is possible
how to build a nice and general theory of infinite products for a
reasonably general type class similarly what we have to sums.
For "sums", we at least have some theory about absolutely summable
series index over an arbitrary set ("infsetsum") and Johannes Hölzl
recently told me about some ways to nicely generalise this, although I
doubt I'll be able to do anything of the sort any time soon. Ideally, it
would be nice to have something like this for products, too, but I don't
know if it is possible and how much work it would be.
Manuel
Email Gateway (Aug 22 2022 at 16:29):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear Manuel,
thank you for your answer.
It seems to me that the hack that you mention should work in the case
that Wenda and I have in mind: since we are dealing with reals only, in
our case it should be enough if we substitute
∏^\infty_{n=1} a_n with e^{∑^\infty_{n=1} ln a_n}
Thanks, Angeliki
Email Gateway (Aug 22 2022 at 16:29):From: Manuel Eberl <eberlm@in.tum.de>
Only if your real numbers are all positive, unfortunately. But if they
are, you're in luck.
In any case, you still might find some of the material in
Analysis/Infinite_Products of use.
Manuel
Last updated: Apr 24 2024 at 20:16 UTC