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

### License

BSD License

### Topics

- Mathematics/Analysis

### Session Lambert_W

- Lambert_W
- Lambert_W_MacLaurin_Series

### Depends on

- Bernoulli Numbers
- Stirling’s formula

## Cite

×

Lambert_W-AFP

    @article{Lambert_W-AFP,
      author  = {Manuel Eberl},
      title   = {The Lambert W Function on the Reals},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Lambert_W.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- May 12, 2020 : Isabelle2020
- Apr 29, 2020 : Isabelle2020