structure ProbabilityTheory.IsUniform {Ω : Type uΩ} {S : Type uS} [mΩ : MeasurableSpace Ω] (H : Set S) (X : Ω → S) (μ : MeasureTheory.Measure Ω := by volume_tac) : Prop

The assertion that the law of $X$ is the uniform probability measure on a finite set $H$. While in applications $H$ will be non-empty finite set, $X$ measurable, and and $\mu$ a probability measure, it could be technically convenient to have a definition that works even without these hypotheses. (For instance, isUniform would be well-defined, but false, for infinite H).

This should probably be refactored, requiring instead that μ.map X = uniformOn H.

• eq_of_mem ⦃x : S⦄ (hx : x ∈ H) ⦃y : S⦄ (hy : y ∈ H) : μ (X ⁻¹' {x}) = μ (X ⁻¹' {y})
• measure_preimage_compl : μ (X ⁻¹' Hᶜ) = 0

theorem ProbabilityTheory.isUniform_uniformOn {Ω : Type uΩ} [mΩ : MeasurableSpace Ω] [MeasurableSingletonClass Ω] {A : Set Ω} : IsUniform A id (uniformOn A)

theorem ProbabilityTheory.exists_isUniform {S : Type uS} [MeasurableSpace S] [MeasurableSingletonClass S] (H : Finset S) (h : H.Nonempty) : ∃ (Ω : Type uS) (x : MeasurableSpace Ω) (X : Ω → S) (μ : MeasureTheory.Measure Ω), MeasureTheory.IsProbabilityMeasure μ ∧ Measurable X ∧ IsUniform (↑H) X μ ∧ (∀ (ω : Ω), X ω ∈ H) ∧ FiniteRange X

Uniform distributions exist.

theorem ProbabilityTheory.IsUniform.comp {Ω : Type uΩ} {S : Type uS} {T : Type uT} [mΩ : MeasurableSpace Ω] {X : Ω → S} {μ : MeasureTheory.Measure Ω} [DecidableEq T] {H : Finset S} (h : IsUniform (↑H) X μ) {f : S → T} (hf : Function.Injective f) : IsUniform (↑(Finset.image f H)) (f ∘ X) μ

The image of a uniform random variable under an injective map is uniform on the image.

theorem ProbabilityTheory.exists_isUniform_measureSpace {S : Type uS} [MeasurableSpace S] [MeasurableSingletonClass S] (H : Finset S) (h : H.Nonempty) : ∃ (Ω : Type uS) (mΩ : MeasureTheory.MeasureSpace Ω) (U : Ω → S), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧ Measurable U ∧ IsUniform (↑H) U MeasureTheory.volume ∧ (∀ (ω : Ω), U ω ∈ H) ∧ FiniteRange U

Uniform distributions exist, version giving a measure space

theorem ProbabilityTheory.exists_isUniform_measureSpace' {S : Type uS} [MeasurableSpace S] [MeasurableSingletonClass S] (H : Set S) (hH : H.Finite) (h'H : H.Nonempty) : ∃ (Ω : Type uS) (mΩ : MeasureTheory.MeasureSpace Ω) (U : Ω → S), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume ∧ Measurable U ∧ IsUniform H U MeasureTheory.volume ∧ (∀ (ω : Ω), U ω ∈ H) ∧ FiniteRange U

Uniform distributions exist, version with a Finite set rather than a Finset and giving a measure space

theorem ProbabilityTheory.IsUniform.ae_mem {Ω : Type uΩ} {S : Type uS} [mΩ : MeasurableSpace Ω] {X : Ω → S} {μ : MeasureTheory.Measure Ω} {H : Set S} (h : IsUniform H X μ) : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ H

A uniform random variable on H almost surely takes values in H.

theorem ProbabilityTheory.IsUniform.nonempty {Ω : Type uΩ} {S : Type uS} [mΩ : MeasurableSpace Ω] {X : Ω → S} {μ : MeasureTheory.Measure Ω} {H : Finset S} (h : IsUniform (↑H) X μ) [hμ : NeZero μ] : H.Nonempty

Uniform random variables only exist for non-empty sets H.

theorem ProbabilityTheory.IsUniform.measure_preimage_of_nmem {Ω : Type uΩ} {S : Type uS} [mΩ : MeasurableSpace Ω] {X : Ω → S} {μ : MeasureTheory.Measure Ω} {H : Set S} (h : IsUniform H X μ) {s : S} (hs : s ∉ H) : μ (X ⁻¹' {s}) = 0

A "unit test" for the definition of uniform distribution.

theorem ProbabilityTheory.IsUniform.measureReal_preimage_of_nmem {Ω : Type uΩ} {S : Type uS} [mΩ : MeasurableSpace Ω] {X : Ω → S} {μ : MeasureTheory.Measure Ω} {H : Set S} (h : IsUniform H X μ) {s : S} (hs : s ∉ H) : μ.real (X ⁻¹' {s}) = 0

Another "unit test" for the definition of uniform distribution.

theorem ProbabilityTheory.IsUniform.measure_preimage_of_mem {Ω : Type uΩ} {S : Type uS} [mΩ : MeasurableSpace Ω] {X : Ω → S} {μ : MeasureTheory.Measure Ω} [MeasurableSpace S] [DiscreteMeasurableSpace S] {H : Finset S} (h : IsUniform (↑H) X μ) (hX : Measurable X) {s : S} (hs : s ∈ H) : μ (X ⁻¹' {s}) = μ Set.univ / ↑(Nat.card { x : S // x ∈ H })

A "unit test" for the definition of uniform distribution.

theorem ProbabilityTheory.IsUniform.measureReal_preimage_of_mem {Ω : Type uΩ} {S : Type uS} [mΩ : MeasurableSpace Ω] {X : Ω → S} {μ : MeasureTheory.Measure Ω} [MeasurableSpace S] [DiscreteMeasurableSpace S] {H : Finset S} [MeasureTheory.IsProbabilityMeasure μ] (h : IsUniform (↑H) X μ) (hX : Measurable X) {s : S} (hs : s ∈ H) : μ.real (X ⁻¹' {s}) = 1 / ↑(Nat.card { x : S // x ∈ H })

A "unit test" for the definition of uniform distribution.

theorem ProbabilityTheory.IsUniform.measureReal_preimage_of_mem' {Ω : Type uΩ} {S : Type uS} [mΩ : MeasurableSpace Ω] {X : Ω → S} {μ : MeasureTheory.Measure Ω} [MeasurableSpace S] [DiscreteMeasurableSpace S] {H : Finset S} [MeasureTheory.IsProbabilityMeasure μ] (h : IsUniform (↑H) X μ) (hX : Measurable X) {s : S} (hs : s ∈ H) : (MeasureTheory.Measure.map X μ).real {s} = 1 / ↑(Nat.card { x : S // x ∈ H })

theorem ProbabilityTheory.IsUniform.measure_preimage {Ω : Type uΩ} {S : Type uS} [mΩ : MeasurableSpace Ω] {X : Ω → S} {μ : MeasureTheory.Measure Ω} [MeasurableSpace S] [DiscreteMeasurableSpace S] {H : Finset S} (h : IsUniform (↑H) X μ) (hX : Measurable X) (H' : Set S) : μ (X ⁻¹' H') = μ Set.univ * ↑(Nat.card ↑(H' ∩ ↑H)) / ↑(Nat.card { x : S // x ∈ H })

$\mathbb{P}(U_H\in H^{\prime })={\displaystyle \frac{|H^{\prime }\cap H|}{|H|}}$

theorem ProbabilityTheory.IsUniform.measureReal_preimage {Ω : Type uΩ} {S : Type uS} [mΩ : MeasurableSpace Ω] {X : Ω → S} {μ : MeasureTheory.Measure Ω} [MeasurableSpace S] [DiscreteMeasurableSpace S] {H : Finset S} (h : IsUniform (↑H) X μ) (hX : Measurable X) (H' : Set S) : μ.real (X ⁻¹' H') = μ.real Set.univ * ↑(Nat.card ↑(H' ∩ ↑H)) / ↑(Nat.card { x : S // x ∈ H })

$\mathbb{P}(U_H\in H^{\prime })={\displaystyle \frac{|H^{\prime }\cap H|}{|H|}}$

theorem ProbabilityTheory.IsUniform.nonempty_preimage_of_mem {Ω : Type uΩ} {S : Type uS} [mΩ : MeasurableSpace Ω] {X : Ω → S} {μ : MeasureTheory.Measure Ω} [MeasurableSpace S] [DiscreteMeasurableSpace S] [NeZero μ] {H : Finset S} (h : IsUniform (↑H) X μ) (hX : Measurable X) {s : S} (hs : s ∈ H) : (X ⁻¹' {s}).Nonempty

theorem ProbabilityTheory.IsUniform.full_measure {Ω : Type uΩ} {S : Type uS} [mΩ : MeasurableSpace Ω] {X : Ω → S} {μ : MeasureTheory.Measure Ω} {H : Set S} [MeasurableSpace S] [DiscreteMeasurableSpace S] (h : IsUniform H X μ) (hX : Measurable X) : (MeasureTheory.Measure.map X μ) H = μ Set.univ

theorem ProbabilityTheory.IsUniform.of_identDistrib {Ω : Type uΩ} {S : Type uS} [mΩ : MeasurableSpace Ω] {X : Ω → S} {μ : MeasureTheory.Measure Ω} {H : Set S} [MeasurableSpace S] [DiscreteMeasurableSpace S] {Ω' : Type u_1} [MeasurableSpace Ω'] (h : IsUniform H X μ) {X' : Ω' → S} {μ' : MeasureTheory.Measure Ω'} (h' : IdentDistrib X X' μ μ') (hH : MeasurableSet H) : IsUniform H X' μ'

A copy of a uniform random variable is also uniform.

theorem ProbabilityTheory.IsUniform.measure_preimage_ne_zero {Ω : Type uΩ} {S : Type uS} [mΩ : MeasurableSpace Ω] {X : Ω → S} {μ : MeasureTheory.Measure Ω} [MeasurableSpace S] [DiscreteMeasurableSpace S] {H : Finset S} [NeZero μ] (h : IsUniform (↑H) X μ) (hX : Measurable X) {H' : Set S} (h' : (H' ∩ ↑H).Nonempty) : μ (X ⁻¹' H') ≠ 0

$\mathbb{P}(U_H\in H^{\prime })\ne 0$ if $H^{\prime }$ intersects $H$ and the measure is non-zero.

theorem ProbabilityTheory.IsUniform.restrict {Ω : Type uΩ} {S : Type uS} [mΩ : MeasurableSpace Ω] {X : Ω → S} {μ : MeasureTheory.Measure Ω} [MeasurableSpace S] [DiscreteMeasurableSpace S] {H : Set S} (h : IsUniform H X μ) (hX : Measurable X) (H' : Set S) : IsUniform (H' ∩ H) X μ[|X ⁻¹' H']

If $X$ is uniform w.r.t. $\mu$ on $H$, then $X$ is uniform w.r.t. $\mu$ conditioned by $H^{\prime }$ on $H^{\prime }\cap H$.

theorem ProbabilityTheory.IdentDistrib.of_isUniform {Ω : Type uΩ} {S : Type uS} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {H : Set S} [MeasurableSpace S] [DiscreteMeasurableSpace S] {Ω' : Type u_1} [MeasurableSpace Ω'] {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ'] [Finite ↑H] [Countable S] {X : Ω → S} {X' : Ω' → S} (hX : Measurable X) (hX' : Measurable X') (hX_unif : IsUniform H X μ) (hX'_unif : IsUniform H X' μ') : IdentDistrib X X' μ μ'

theorem ProbabilityTheory.IsUniform.map_eq_uniformOn {Ω : Type uΩ} {S : Type uS} [mΩ : MeasurableSpace Ω] {X : Ω → S} {μ : MeasureTheory.Measure Ω} [MeasurableSpace S] [DiscreteMeasurableSpace S] [Countable S] [MeasureTheory.IsProbabilityMeasure μ] {H : Set S} (h : IsUniform H X μ) (hX : Measurable X) (hH : H.Finite) (h'H : H.Nonempty) : MeasureTheory.Measure.map X μ = uniformOn H

theorem ProbabilityTheory.isUniform_iff_map_eq_uniformOn {S : Type uS} {H : Set S} [MeasurableSpace S] [DiscreteMeasurableSpace S] [Finite ↑H] {Ω : Type u_1} [mΩ : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [Countable S] [MeasureTheory.IsProbabilityMeasure μ] {U : Ω → S} (hU : Measurable U) : IsUniform H U μ ↔ MeasureTheory.Measure.map U μ = uniformOn H

A random variable is uniform iff its distribution is.