Email Gateway (Aug 22 2022 at 17:54): Email Gateway (Aug 22 2022 at 17:54):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Hello,
How could I formalize the following (trivial) infinite product identity
(1-x)(1+x) (1+x^2) (1+x^4) (1+x^8) (1+x^16) (1+x^32) (1+x^64)...(1+x^(2^n))...
= 1
in Isabelle, where x is a formal variable?
Thank you in advance.
José M.
Email Gateway (Aug 22 2022 at 17:56):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Thank you for the complete proof of this identity, I will do reverse
engineering in order to express more non-trivial identities in the same
way. With respect to the statement:
« 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. »
I would like to sketch how a proof of this identity can be done in Isabelle
when a library about analytic functions in the complex plane will be ready.
So, this example could be a good test of for that library.
Ingredients of the library:
If individual terms of a uniformly converging series are continuous,
then the the series is continuous in the same domaine:
http://mathworld.wolfram.com/UniformConvergence.html
Weierstrass M-Test: http://mathworld.wolfram.com/WeierstrassM-Test.html
Informal proof.
Let f(z) := (1-z)(1+z)(1+z^2)(1+z^4)(1+z^8)(1+z^16)…(1+z^(2^n))…
Substituting we have f(0) = 1.
In virtue of Weierstrass M-test, f(z) is uniformly convergent on a
neighbourhood of the origine z = 0. So, f(z) is continuous on this
neighbourhood.
Applying 1-z^2 = (1-z)(1+z), we obtain the functional equation
f(z^2) = f(z),
for any z in the domain of f(z). It follows by complete induction that, for
any positive integer n,
f(z) = f(z^(2^n)),
By continuity at z = 0, we have that
f(z) = lim f(z) = lim f(z^(2^n)) = f(lim z^(2^n)) = f(0) = 1,
provided that |z| < 1. We can choose a sequence of such values of z
converging to z = 0. In virtue of the above mentioned Identity Theorem, we
conclude that f(z) = 1 for any complex number z in the domain of definition
of f(z).
qed.
This way of proving this identity, avoiding formal manipulations, is
typical of XIX century, in particular of Lejeune Dirichlet and his student
Bernhard Riemann, who were « lazy » enough to change computations for ideas.
Jose M.
Message: 5
Last updated: Apr 18 2024 at 08:19 UTC