Lambert Series (Q7361492)

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.