Abstract

This entry provides a formalisation of Lambert series, i.e. series of the form ∑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 the series converges, the functional equation it satisfies under the map f(q) = 1/q, the power series expansion at q = 0, expressing a Lambert series in terms of the associated ‘normal’ power series, and connections to various number-theoretic functions like the divisor σ function.

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.

BibTeX

@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},
}