Lambert Series

This entry provides a formalisation of Lambert series, i.e. series of the form $L(a_n,q)=\sum _{n=1}^{\mathrm{\infty }}{a}_n{q}^n/(1-q^n)$ where $a_n$ is a sequence of real or complex numbers.

Proofs for all the basic properties are provided, such as:

• the precise region in which $L(a_n,q)$ converges
• the functional equation $L(a_n,\frac{1}{q})=-(\sum _{n=1}^{\mathrm{\infty }}{a}_n)-L(a_n,q)$
• the power series expansion of $L(a_n,q)$ at $q=0$
• the connection $L(a_n,q)=\sum _{k=1}^{\mathrm{\infty }}f(q^k)$ for $f(z)=\sum _{n=1}^{\mathrm{\infty }}{a}_n{z}^n$
that links a Lambert series to its “corresponding” power series
• connections to various number-theoretic functions, e.g. the divisor $\sigma$ function via $\sum _{n=1}^{\mathrm{\infty }}{\sigma }_{\alpha }(n)q^n=L(n^{\alpha },q)$

The formalisation mainly follows the chapter on Lambert series in Konrad Knopp's classic textbook Theory and Application of Infinite Series and includes all results presented therein.