### Abstract

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.