Lambert W function

DefinitionLambert map#✓fully proved

The Lambert map is the function \(h(y) = y e^y\) of a real variable \(y\).

The inverse of \(h\) restricted to \(y > -1\) is the principal real branch of the Lambert W function.

public noncomputable def lambertMap (y : ℝ) : ℝ :=
  y * Real.exp y
Sources
  • Ouellet JIS VOL20 ou2.tex lines 426-432.
Used by 9
Used byLower-branch preimages of the Lambert map · Principal-branch preimages of the Lambert map · Existence of the Lambert sequences · Lambert bounds for the left factorial · Two-parameter Lambert bounds for the left factorial · The golden factorial exponent exceeds the Lambert sequence · Floor formulas for the left factorial · Partial exponential sums at the Lambert sequence · A linear lower bound for the Lambert sequence

TheoremPrincipal-branch preimages of the Lambert map#✓fully proved

Let \(h(y) = y e^y\) be the Lambert map on the real numbers. Every real \(x > -e^{-1}\) has exactly one preimage \(y > -1\) under \(h\), that is, there is exactly one real number \(y > -1\) with \(y e^y = x\).

public theorem existsUnique_lambertMap_preimage (x : ℝ)
    (hx : -Real.exp (-1) < x) :
    ∃! y : { y : ℝ // -1 < y }, lambertMap y.val = x
Uses 1
Statement usesLambert map

TheoremLower-branch preimages of the Lambert map#✓fully proved

Let \(h(y) = y e^y\) be the Lambert map on the real numbers. Every real \(x\) with \(-e^{-1} \le x < 0\) has exactly one preimage \(y \le -1\) under \(h\), that is, there is exactly one real number \(y \le -1\) with \(y e^y = x\).

This preimage is the value at \(x\) of the lower real branch \(W_{-1}\) of the Lambert W function. Existence uses \(h(-1) = -e^{-1}\), \(h(y) \to 0\) as \(y \to -\infty\) and the intermediate value theorem; uniqueness uses \(h'(y) = e^y (1 + y) < 0\) for \(y < -1\).

public theorem existsUnique_lambertMap_lower_preimage {x : ℝ}
    (hx1 : -Real.exp (-1) ≤ x) (hx0 : x < 0) :
    ∃! y : { y : ℝ // y ≤ -1 }, lambertMap y.val = x
Sources
  • Petojević, Gorjanac Ranitović, Rastovac and Mandić, The Golden Ratio, Factorials, and the Lambert W Function, Journal of Integer Sequences 27 (2024), Article 24.5.7, Section 3.1 (the lower branch W₋₁).
Uses 1 · Used by 1
Statement usesLambert map
Used byExistence of the Lambert sequences
3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.