
The
Lambert
W
Function
on
the
Reals
Title: 
The Lambert W Function on the Reals 
Author:

Manuel Eberl

Submission date: 
20200424 
Abstract: 
The Lambert W function is a multivalued
function defined as the inverse function of x
↦ x
e^{x}. Besides numerous
applications in combinatorics, physics, and engineering, it also
frequently occurs when solving equations containing both
e^{x} and
x, or both x and log
x. This article provides a
definition of the two realvalued branches
W_{0}(x)
and
W_{1}(x)
and proves various properties such as basic identities and
inequalities, monotonicity, differentiability, asymptotic expansions,
and the MacLaurin series of
W_{0}(x)
at x = 0. 
BibTeX: 
@article{Lambert_WAFP,
author = {Manuel Eberl},
title = {The Lambert W Function on the Reals},
journal = {Archive of Formal Proofs},
month = apr,
year = 2020,
note = {\url{http://isaafp.org/entries/Lambert_W.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Bernoulli, Stirling_Formula 
