Lapalace Distribution

Stream: Is there code for X?

[Reuven Peleg]

The Laplace Distribution which can be described as the difference between two independent variates with identical exponential distributions, plays a major role in differential privacy, among other fields. Does someone know about an existing LEAN definition of it (and proofs for PMF, expectation and variance) somewhere already?
I tried Google, the docs at Mathlib/Probability/Distributions, and some LLM-assisted search but found nothing.

[Etienne Marion]

I am pretty sure we do not have it.