English
For a finite set s, uniformOn s is the probability measure on Ω defined by the counting measure conditioned on s; equivalently, for any t, uniformOn s(t) = |s ∩ t| / |s|.
Русский
Для конечного множества s равномерное распределение на s — это вероятность, получаемая из счетной меры, условной относительно s; то есть для любого t: uniformOn s(t) = |s ∩ t| / |s|.
LaTeX
$$$\forall t,\ uniformOn(s)(t) = \frac{\#(s \cap t)}{\#s}$, когда $s$ конечно.$$
Lean4
/-- Given a set `s`, `uniformOn s` is the uniform measure on `s`, defined as the counting measure
conditioned by `s`. One should think of `uniformOn s t` as the proportion of `s` that is contained
in `t`.
This is a probability measure when `s` is finite and nonempty and is given by
`ProbabilityTheory.uniformOn_isProbabilityMeasure`. -/
def uniformOn (s : Set Ω) : Measure Ω :=
Measure.count[|s]
