Manuel Eberl
Archive of Formal Proofs 2023.
pdf 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},}