Lambert Series

This entry provides a formalisation of Lambert series, i.e. series of the form $L(a_n, q) = \sum_{n=1}^\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}^\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}^\infty f(q^k)$ for $f(z) = \sum_{n=1}^\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}^\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.