Source indexedlemma · leanprover/lean4:v4.33.0-rc1

ProbabilityTheory.exists_isUniform_measureSpace'

PFR.ForMathlib.Uniform · PFR/ForMathlib/Uniform.lean:90 to 99

Source documentation

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

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma exists_isUniform_measureSpace' {S : Type uS} [MeasurableSpace S]    [MeasurableSingletonClass S] (H : Set S) (hH : H.Finite) (h'H : H.Nonempty) :    ∃ (Ω : Type uS) (mΩ : MeasureSpace Ω) (U : Ω → S),    IsProbabilityMeasure (ℙ : Measure Ω) ∧ Measurable U ∧ IsUniform H U      ∧ (∀ ω, U ω ∈ H) ∧ FiniteRange U := by  set Hf := hH.toFinset  have hHf : Hf.Nonempty := by simpa [Hf] using h'H  obtain ⟨Ω, mΩ, U, hμ, hmes, hunif, hrange, hfin⟩ := exists_isUniform_measureSpace Hf hHf  simp only [Finite.coe_toFinset, Finite.mem_toFinset, Hf] at hunif hrange  exact ⟨Ω, mΩ, U, hμ, hmes, hunif, hrange, hfin⟩