Lambert W function & sinc integral

Stream: Is there code for X?

[Snir Broshi]

Are the Lambert W function or the integral of sinc defined/used in Mathlib?

I think they are reasonably well known functions that probably belong in Mathlib/Analysis/SpecialFunctions/.

If they don't exist yet, is there interest in proving properties about them, such as the ones listed in the Wikipedia links above? e.g. Taylor series, bounds, special values

[Kenny Lau]

I'd be interested (but I don't do analysis)

[Aaron Liu]

The W function has lots of branches, which one should be picked?

[Snir Broshi]

The branches are in correspondence with integers, so I think all of them.
They're usually denoted $W_k(z)$, so we can do Complex.LambertW k z