Documentation

PFR.ForMathlib.Uniform

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

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 $μ$ 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⦄, x H∀ ⦃y : S⦄, y Hμ (X ⁻¹' {x}) = μ (X ⁻¹' {y})
  • measure_preimage_compl : μ (X ⁻¹' H) = 0
Instances For
    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 ProbabilityTheory.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 : ProbabilityTheory.IsUniform (↑H) X μ) {f : ST} (hf : Function.Injective f) :

    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) ( : MeasureTheory.MeasureSpace Ω) (U : ΩS), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume Measurable U ProbabilityTheory.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) ( : MeasureTheory.MeasureSpace Ω) (U : ΩS), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume Measurable U ProbabilityTheory.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 : ProbabilityTheory.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 : ProbabilityTheory.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 : ProbabilityTheory.IsUniform H X μ) {s : S} (hs : sH) :
    μ (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 : ProbabilityTheory.IsUniform H X μ) {s : S} (hs : sH) :
    μ.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 : ProbabilityTheory.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 : ProbabilityTheory.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 : ProbabilityTheory.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 : ProbabilityTheory.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') = \dfrac{|H' \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 : ProbabilityTheory.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') = \dfrac{|H' \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 : ProbabilityTheory.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 : ProbabilityTheory.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 : ProbabilityTheory.IsUniform H X μ) {X' : Ω'S} {μ' : MeasureTheory.Measure Ω'} (h' : ProbabilityTheory.IdentDistrib X X' μ μ') (hH : MeasurableSet H) :

    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 : ProbabilityTheory.IsUniform (↑H) X μ) (hX : Measurable X) {H' : Set S} (h' : (H' H).Nonempty) :
    μ (X ⁻¹' H') 0

    $\mathbb{P}(U_H \in H') \neq 0$ if $H'$ 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 : ProbabilityTheory.IsUniform H X μ) (hX : Measurable X) (H' : Set S) :

    If $X$ is uniform w.r.t. $\mu$ on $H$, then $X$ is uniform w.r.t. $\mu$ conditioned by $H'$ on $H' \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 : ProbabilityTheory.IsUniform H X μ) (hX'_unif : ProbabilityTheory.IsUniform H X' μ') :

    A random variable is uniform iff its distribution is.