The Lambert WFunction on the Reals

 Title: The Lambert W Function on the Reals Author: Manuel Eberl Submission date: 2020-04-24 Abstract: The Lambert W function is a multi-valued function defined as the inverse function of x ↦ x ex. Besides numerous applications in combinatorics, physics, and engineering, it also frequently occurs when solving equations containing both ex and x, or both x and log x. This article provides a definition of the two real-valued branches W0(x) and W-1(x) and proves various properties such as basic identities and inequalities, monotonicity, differentiability, asymptotic expansions, and the MacLaurin series of W0(x) at x = 0. BibTeX: @article{Lambert_W-AFP, author = {Manuel Eberl}, title = {The Lambert W Function on the Reals}, journal = {Archive of Formal Proofs}, month = apr, year = 2020, note = {\url{http://isa-afp.org/entries/Lambert_W.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Bernoulli, Stirling_Formula