Exponential Distribution

Stream: mathlib4

[Joakim Björnander]

Hi,

I'm relatively new to Lean. I noticed there is no exponential distribution in Mathlib.Probability.Distributions, so I thought it would be a good first contribution to Mathlib4. Is there anything I should be aware of as a first-time contributor?

I'm planning to follow the structure of Mathlib.Probability.Distributions.Gaussian.Real. The scope I have in mind:

1. Define the PDF and the measure via withDensity
2. Prove it's a probability measure
3. Prove basic properties (mean, variance, MGF, memoryless property, CDF)

I've already done most of this as a personal exercise, so I have working proofs to start from.

[Rémy Degenne]

Hi! It looks like there is already code for the exponential distribution: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Probability/Distributions/Exponential.html

[Rémy Degenne]

but we don't have all the properties you mentioned

[Joakim Björnander]

Apologies. I should have checked more carefully before posting. Would completing this file with the basic properties be a welcome first-time contributor PR?

[Rémy Degenne]

Yes, adding more of the basic properties would be a welcome PR!

[Rémy Degenne]

Something else I'd like to see at some point is a PR in which some of the probability distributions are actually used for something else. I think that only the uniform and Gaussian distributions are ever used elsewhere in Mathlib.

[Joakim Björnander]

Made PR https://github.com/leanprover-community/mathlib4/pull/35504