Email Gateway (Aug 22 2022 at 17:40): Email Gateway (Aug 22 2022 at 17:40):From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
Dear Lukas,
The result that you mechanized in Euler_Partition-AFP corresponds to the
identity:
(1+x)(1+x^2)(1+x^3)(1+x^4)(1+x^5)...
= 1/(1-x) 1/(1-x^3) 1/(1-x^5) 1/(1-x^7)...
The coefficient of x^n in the expansion of (1+x)(1+x^2)(1+x^3)(1+x^4)(1+x^5)...
is the number of partitions of n with only distinct parts. The coefficient
of x^n in the expansion of 1/(1-x) 1/(1-x^3) 1/(1-x^5) 1/(1-x^7)... is the
number of partitions of n into odd parts. The proof is as follows:
substitute (1+x^n) by (1-x^(2n))/(1-x^n) in the product
(1+x)(1+x^2)(1+x^3)(1+x^4)(1+x^5)...
and simplify (1-x^(2n)) both in the numerator and the denominator in order
to obtain
1/(1-x) 1/(1-x^3) 1/(1-x^5) 1/(1-x^7)...
I wonder how this very simple idea could be formalized in Isabelle.
Kind Regards,
Jose M.
Email Gateway (Aug 22 2022 at 17:53):From: Manuel Eberl <eberlm@in.tum.de>
There is a development on Formal Power Series in
HOL-Computational_Algebra. Just import
"HOL-Computational_Algebra.Computational_Algebra".
The theory in question is called "Formal_Power_Series.thy". You can find
it in "~~/src/HOL/Computational_Algebra".
If you have any questions, feel free to ask me (in private or on the
mailing list). I have worked with this quite a bit in the past.
I'm pretty sure we don't have anything on the pentagonal number theorem.
Manuel
Email Gateway (Aug 22 2022 at 17:53):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
Hi José,
I don't know much about the pentagonal number theorem, but I saw the
definition and proofs (on wikipedia) include combinatorial facts about
number partitions, and the partition function.
Number partitions and the partition function have been formalized in
this AFP entry:
https://www.isa-afp.org/entries/Card_Number_Partitions.html
Possibly this and the Formal Power Series helps to get you started to
prove that theorem.
Best regards,
Lukas
Email Gateway (Aug 22 2022 at 17:53):From: Lukas Bulwahn <lukas.bulwahn@gmail.com>
Hi José,
I read a bit more about the proof and I believe the core fact has
already been proved in this entry:
https://www.isa-afp.org/entries/Euler_Partition.html
I just never linked the result to formal power series.
Best regards,
Lukas
Last updated: Apr 19 2024 at 04:17 UTC