The uniform measure on a finite type

Evaluation of ProbabilityTheory.uniformOn on a finset or on Set.univ at singletons, finite sets and predicates, in ℝ≥0∞ and on reals, and the almost-everywhere filter of the uniform measure on a finite type.

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

theorem MeasureTheory.uniformOn_finset_real_singleton {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] [DecidableEq W] (A : Finset W) (w : W) : (ProbabilityTheory.uniformOn ↑A).real {w} = if w ∈ A then (↑A.card)⁻¹ else 0

theorem MeasureTheory.uniformOn_finset_real_singleton_le_iff {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] [DecidableEq W] {A B : Finset W} {w : W} (hA : w ∈ A) (hB : w ∈ B) : (ProbabilityTheory.uniformOn ↑A).real {w} ≤ (ProbabilityTheory.uniformOn ↑B).real {w} ↔ B.card ≤ A.card

theorem MeasureTheory.uniformOn_finset_real_singleton_lt_of_ssubset {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] [DecidableEq W] {A B : Finset W} {w : W} (h : B ⊂ A) (hw : w ∈ B) : (ProbabilityTheory.uniformOn ↑A).real {w} < (ProbabilityTheory.uniformOn ↑B).real {w}

theorem MeasureTheory.uniformOn_real_apply_of_finite {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] {s : Set W} (hs : s.Finite) (e : Set W) : (ProbabilityTheory.uniformOn s).real e = ↑(s ∩ e).ncard / ↑s.ncard

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

theorem MeasureTheory.uniformOn_finset_real_setOf {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] [Finite W] (A : Finset W) (p : W → Prop) [DecidablePred p] : (ProbabilityTheory.uniformOn ↑A).real {w : W | p w} = ↑(Finset.filter p A).card / ↑A.card

theorem MeasureTheory.uniformOn_absolutelyContinuous_of_subset {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] {A B : Set W} (hB : B.Finite) (hAB : A ⊆ B) : (ProbabilityTheory.uniformOn A).AbsolutelyContinuous (ProbabilityTheory.uniformOn B)

Proportions of a finite set

On a finite set s the uniform measure gives t the proportion |s ∩ t| / |s|, so a bound on the measure is a bound on |s ∩ t| scaled by |s|.

theorem MeasureTheory.uniformOn_apply_of_finite {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] {s : Set W} (hs : s.Finite) (t : Set W) : (ProbabilityTheory.uniformOn s) t = ↑(s ∩ t).ncard / ↑s.ncard

theorem MeasureTheory.uniformOn_finset_setOf {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] (F : Finset W) (p : W → Prop) [DecidablePred p] : (ProbabilityTheory.uniformOn ↑F) {x : W | p x} = ↑(Finset.filter p F).card / ↑F.card

theorem MeasureTheory.le_uniformOn_iff {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] {s t : Set W} (hs : s.Finite) (hne : s.Nonempty) {θ : ENNReal} : θ ≤ (ProbabilityTheory.uniformOn s) t ↔ θ * ↑s.ncard ≤ ↑(s ∩ t).ncard

theorem MeasureTheory.uniformOn_cond {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] {s t : Set W} (hs : s.Finite) (ht : MeasurableSet t) : (ProbabilityTheory.uniformOn s)[|t] = ProbabilityTheory.uniformOn (s ∩ t)

theorem MeasureTheory.uniformOn_univ_cond {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] [Finite W] (A : Set W) : (ProbabilityTheory.uniformOn Set.univ)[|A] = ProbabilityTheory.uniformOn A

theorem MeasureTheory.uniformOn_eq_one_iff {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] {s t : Set W} (hs : s.Finite) (hne : s.Nonempty) : (ProbabilityTheory.uniformOn s) t = 1 ↔ s ⊆ t

theorem MeasureTheory.uniformOn_eq_inv_ncard_iff {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] {s t : Set W} (hs : s.Finite) (hne : s.Nonempty) : (ProbabilityTheory.uniformOn s) t = (↑s.ncard)⁻¹ ↔ (s ∩ t).ncard = 1

The uniform measure on a finite type

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_ae_iff {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] [Fintype W] {p : W → Prop} : (∀ᵐ (w : W) ∂ProbabilityTheory.uniformOn Set.univ, p w) ↔ ∀ (w : W), p w

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_univ_real_apply {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] [Fintype W] (A : Set W) : (ProbabilityTheory.uniformOn Set.univ).real A = ↑A.ncard / ↑(Fintype.card W)

theorem MeasureTheory.uniformOn_univ_le_iff {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] [Fintype W] [Nonempty W] {A B : Set W} : (ProbabilityTheory.uniformOn Set.univ) A ≤ (ProbabilityTheory.uniformOn Set.univ) B ↔ A.ncard ≤ B.ncard