Email Gateway (Aug 22 2022 at 17:58): Email Gateway (Aug 22 2022 at 17:58):From: Manuel Eberl <eberlm@in.tum.de>
About half an hour after I wrote that email yesterday I realised that
I'm an idiot. The identity can be proved by a simple induction much more
easily:
lemma myprod: "(∏k<n. 1 + fps_X ^ (2 ^ k)) = Abs_fps (λi. if i < 2 ^ n
then 1 else 0)"
(is "?F n = ?G n")
proof (induction n)
case (Suc n)
have "?F (Suc n) = ?F n + fps_X ^ (2 ^ n) * ?F n"
by (simp add: algebra_simps)
also have "?F n = ?G n" by (fact Suc.IH)
also have "?G n + fps_X ^ (2 ^ n) * ?G n = ?G (Suc n)"
by (auto simp: fps_X_power_mult_nth fps_eq_iff)
finally show ?case .
qed (auto simp: fps_eq_iff)
FPS_Prodinf.thy
Email Gateway (Aug 22 2022 at 17:59):From: Lawrence Paulson <lp15@cam.ac.uk>
Thanks for the comment, this is quite interesting!
Isabelle/HOL indeed includes a development of non-standard analysis. It has many strong points: it's purely definitional (no axioms); it covers several numeric types including the reals and natural numbers; results can be proved about the non-standard reals with remarkable ease and then carried over to the standard reals.
But nobody uses it, which is a shame. It would be great to see some projects built on this material again.
Larry
Email Gateway (Aug 22 2022 at 18:08):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Concerning the question
Let f_n(z) = (1 - 1/n) / (1-z).
Evidently, lim f_n(z) = 1 / (1-z) as n goes to infinity (uniform
convergence on a neighbourhood of the origin). On the other hand, the
family of formal power series obtained by the expansion of f_n(z) at 0,
i.e.,
f_n(z) = (1-1/n) + (1-1/n)z + (1-1/n)z^2 + (1-1/n)z^3 + ...,
does not converge to the formal power series
1 + z + z^2 + z^3 + ...
with respect to the topology of formal power series.
Jose M.
Email Gateway (Aug 22 2022 at 18:11):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm not aware that we have infinite products of formal power series, but we do have infinite products where x is a real or complex variable. (This material is new and will be included with Isabelle 2018.) There is a theorem allowing you to prove that this infinite product converges without actually evaluating it. And it's a simple matter to prove by induction that the partial products have the form (1 - x^(2^n)), provided of course that norm x < 1. So it shouldn't be difficult to prove that the infinite product equals 1.
Larry
Email Gateway (Aug 22 2022 at 18:14):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
I think that - using Isabelle2017 - an alternative could be to follow
Edward Nelson's approach in "Radically Elementary Probability Theory": to
use finite products and non-standard analysis in place of actual infinite
products. Here there is a link to this reference for people interested in
this approach: https://web.math.princeton.edu/~nelson/books/rept.pdf
Indeed, Robinson's non-standard analysis was already used in Isabelle in
another context :
https://www.cl.cam.ac.uk/~lp15/papers/Reports/fleuriot-princip-CADE.pdf
2018-08-01 9:33 GMT-04:00 Lawrence Paulson <lp15@cam.ac.uk>:
Email Gateway (Aug 22 2022 at 18:16):From: Manuel Eberl <eberlm@in.tum.de>
I am not sure about the analytic argument at all, and I don't know
anything about non-standard analysis, but here is my take on this:
Formal power series are a metric space in Isabelle, where the distance
of two FPSs f and g is simply 2^(-n), where n is the index of the first
coefficient where f and g differ. This means that a sequence of FPSs
converges iff each coefficient stabilises eventually (i.e. does not
change anymore). I believe this is a standard definition.
Now, there is probably some connection between convergence these power
series as analytic functions in the complex plane and the convergence,
but I am not sure about this and we don't have it in Isabelle yet
anyway. Perhaps you know more about this than I do.
However, you can prove this limit directly on the topology of FPSs
(which I sketched above). The proof is a bit fiddly, but it basically
boils down to showing the following key lemma:
lemma "fps_nth (∏k=0..n. 1 + fps_X ^ (2 ^ k)) m = (if m < 2 ^ (n+1) then
1 else 0)"
This means that the m-th coefficient of the n-th partial product is 1 if
2^(n+1) > m and 0 otherwise, and the reasoning involves the uniqueness
of the binary representation of m. I don't know what proof you had in
mind, but my guess would be that it was something like this.
With this lemma, it is then trivial to show the actual convergence:
lemma "(λn. ∏k=0..n. 1 + fps_X ^ (2 ^ k)) ⇢ Abs_fps (λ_. 1)"
So the partial products converge to the FPS whose coefficients are all
1, i.e. 1 + x + x² + x³ + …
This is, of course, precisely 1 / (1 - x), and we have that fact in
Isabelle as well.
For the full proof, see the attachment.
Cheers,
Manuel
Scratch.thy
pEpkey.asc
Last updated: Apr 20 2024 at 08:16 UTC