theorem ProbabilityTheory.uniformOn_apply_singleton_of_mem {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} {x : Ω} (hx : x ∈ s) (hs : s.Finite) : (ProbabilityTheory.uniformOn s) {x} = 1 / ↑(Nat.card ↑s)

theorem ProbabilityTheory.uniformOn_apply_singleton_of_not_mem {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} {x : Ω} (hx : x ∉ s) : (ProbabilityTheory.uniformOn s) {x} = 0

theorem ProbabilityTheory.uniformOn_apply_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t : Set Ω} (hst : s ∩ t = ∅) : (ProbabilityTheory.uniformOn s) t = 0

theorem ProbabilityTheory.uniformOn_of_infinite {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (hs : s.Infinite) : ProbabilityTheory.uniformOn s = 0

theorem ProbabilityTheory.uniformOn_apply {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (hs : s.Finite) (t : Set Ω) : (ProbabilityTheory.uniformOn s) t = ↑(Nat.card ↑(s ∩ t)) / ↑(Nat.card ↑s)

instance ProbabilityTheory.uniformOn.instIsProbabilityMeasure {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} [Nonempty ↑s] [Finite ↑s] : MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.uniformOn s)

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.map_uniformOn_apply {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [MeasurableSpace Ω'] [MeasurableSingletonClass Ω'] {s : Set Ω} {f : Ω → Ω'} (hmes : Measurable f) (hf : Function.Injective f) {t : Set Ω'} (ht : MeasurableSet t) : (MeasureTheory.Measure.map f (ProbabilityTheory.uniformOn s)) t = (ProbabilityTheory.uniformOn (f '' s)) t

theorem ProbabilityTheory.map_uniformOn {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [MeasurableSpace Ω'] [MeasurableSingletonClass Ω'] {s : Set Ω} {f : Ω → Ω'} (hmes : Measurable f) (hf : Function.Injective f) : MeasureTheory.Measure.map f (ProbabilityTheory.uniformOn s) = ProbabilityTheory.uniformOn (f '' s)