### 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.

### License

BSD License

### Topics

- Mathematics/Analysis

### Session Lambert_Series

- Lambert_Series_Library
- Number_Theoretic_Functions_Extras
- Summation_Tests_More
- Lambert_Series

### Depends on

- Dirichlet Series
- The Polylogarithm Function

### Auto-related entries

- Irrationality Criteria for Series by Erdős and Straus

## Cite

×

Lambert_Series-AFP

    @article{Lambert_Series-AFP,
      author  = {Manuel Eberl},
      title   = {Lambert Series},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Lambert_Series.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest