The uniform measure on a finite type #
Evaluation of ProbabilityTheory.uniformOn on a finset or on Set.univ at singletons and
finite sets, in ℝ≥0∞ and on reals.
theorem
MeasureTheory.uniformOn_finset_apply_singleton
{W : Type u_1}
[MeasurableSpace W]
[MeasurableSingletonClass W]
[DecidableEq W]
(A : Finset W)
(w : W)
:
(ProbabilityTheory.uniformOn ↑A) {w} = if w ∈ A then (↑A.card)⁻¹ else 0
The uniform measure on a finset at a singleton: 1 / #A on A and 0 off it.
theorem
MeasureTheory.uniformOn_univ_apply_singleton
{W : Type u_1}
[MeasurableSpace W]
[MeasurableSingletonClass W]
[Fintype W]
(w : W)
:
(ProbabilityTheory.uniformOn Set.univ) {w} = (↑(Fintype.card W))⁻¹
theorem
MeasureTheory.uniformOn_univ_singleton_ne_zero
{W : Type u_1}
[MeasurableSpace W]
[MeasurableSingletonClass W]
[Fintype W]
(w : W)
:
(ProbabilityTheory.uniformOn Set.univ) {w} ≠ 0
theorem
MeasureTheory.uniformOn_univ_singleton_eq
{W : Type u_1}
[MeasurableSpace W]
[MeasurableSingletonClass W]
[Fintype W]
(w w' : W)
:
(ProbabilityTheory.uniformOn Set.univ) {w} = (ProbabilityTheory.uniformOn Set.univ) {w'}
theorem
MeasureTheory.uniformOn_univ_real_singleton
{W : Type u_1}
[MeasurableSpace W]
[MeasurableSingletonClass W]
[Fintype W]
(w : W)
:
(ProbabilityTheory.uniformOn Set.univ).real {w} = (↑(Fintype.card W))⁻¹
theorem
MeasureTheory.uniformOn_univ_real_coe_finset
{W : Type u_1}
[MeasurableSpace W]
[MeasurableSingletonClass W]
[Fintype W]
(s : Finset W)
:
(ProbabilityTheory.uniformOn Set.univ).real ↑s = ↑s.card / ↑(Fintype.card W)
theorem
MeasureTheory.uniformOn_real_apply
{W : Type u_1}
[MeasurableSpace W]
[MeasurableSingletonClass W]
[Finite W]
(s e : Set W)
:
(ProbabilityTheory.uniformOn s).real e = ↑(s ∩ e).ncard / ↑s.ncard
The uniform measure on a set at a set, on reals: the proportion of the atoms of s lying
in e, with 0 / 0 = 0 when s is empty.