Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: The Rogers–Ramanujan Identitie...


view this post on Zulip Email Gateway (Jan 24 2025 at 13:55):

From: Lawrence Paulson <lp15@cam.ac.uk>
I’m happy to announce a major new development by Manuel Eberl: The Rogers–Ramanujan Identities, based on two additional new entries: Theta Functions and Combinatorial q-Analogues. He formalises the identities following the proof given in Andrews and Eriksson book Integer Partitions, using the Jacobi triple product. The other entries provide, among many other things, the Ramanujan theta function, the Jacobi theta function, Euler's pentagonal number theorem and the q-binomial theorem.

https://www.isa-afp.org/entries/Rogers_Ramanujan.html
https://www.isa-afp.org/entries/Theta_Functions.html
https://www.isa-afp.org/entries/Combinatorial_Q_Analogues.html

Larry


Last updated: Jan 30 2025 at 04:21 UTC