Manuel Eberl
Archive of Formal Proofs 2023.
Abstract
This entry provides a definition of the Polylogarithm function, commonly denoted as Li(a,z). Here, z is a complex number and a an integer parameter. This function can be defined by a power series for |z| < 1 and analytically extended to the entire complex plane, except for a branch cut on the reals ≥ 1. Several basic properties are also proven, such as the relationship to the Eulerian polynomials, the derivative formula, the relationship to the ‘normal’ logarithm, and the duplication formula.
BibTex
@article{Polylog-AFP, author = {Manuel Eberl}, title = {The Polylogarithm Function}, journal = {Archive of Formal Proofs}, month = {November}, year = {2023}, note = {\url{https://isa-afp.org/entries/Polylog.html}, Formal proof development}, ISSN = {2150-914x},}