Syntax for "follows distribution"

Stream: new members

[Ryan Whitty]

Hi! I'm trying to state/prove a theorem with a hypothesis that looks something like "Suppose X follows the uniform distribution over some set S." That is,

$$X \sim Uniform(S)$$

I'm getting caught up on how to express this hypothesis, specifically the idea that some object "follows" a distribution in Lean. Currently I'm trying to use PMF.uniformOfFinset to represent my distribution, but I'm not sure this is the correct approach. Thanks for the help :)

[Rémy Degenne]

You could use ProbabilityTheory.uniformOn for the uniform measure over a finite set.
The way to write that X has that distribution in a measurable space with probability measure P is P.map X = uniformOn S.

Take a look at the blog post https://leanprover-community.github.io/blog/posts/basic-probability-in-mathlib/ for other common questions of the type "how do I express the probability related thing X in Mathlib?".

[Kexing Ying]

Note that for continuous uniform distributions we have IsUniform

[Ryan Whitty]

Thanks so much, this helps a lot!