Existence of Random Variables

This file contains lemmas that state the existence of random variables with given distributions and a given dependency structure (currently only mutual independence is considered).

theorem Measure.exists_hasLaw {𝓧 : Type u} {m𝓧 : MeasurableSpace 𝓧} (μ : MeasureTheory.Measure 𝓧) : ∃ (Ω : Type u) (x : MeasurableSpace Ω) (P : MeasureTheory.Measure Ω) (X : Ω → 𝓧), Measurable X ∧ ProbabilityTheory.HasLaw X μ P

theorem ProbabilityTheory.exists_hasLaw_indepFun {ι : Type v} (𝓧 : ι → Type u) {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} (μ : (i : ι) → MeasureTheory.Measure (𝓧 i)) [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] : ∃ (Ω : Type (max u v)) (x : MeasurableSpace Ω) (P : MeasureTheory.Measure Ω) (X : (i : ι) → Ω → 𝓧 i), (∀ (i : ι), Measurable (X i)) ∧ (∀ (i : ι), HasLaw (X i) (μ i) P) ∧ iIndepFun X P ∧ MeasureTheory.IsProbabilityMeasure P

theorem ProbabilityTheory.exists_iid (ι : Type v) {𝓧 : Type u} {m𝓧 : MeasurableSpace 𝓧} (μ : MeasureTheory.Measure 𝓧) [MeasureTheory.IsProbabilityMeasure μ] : ∃ (Ω : Type (max u v)) (x : MeasurableSpace Ω) (P : MeasureTheory.Measure Ω) (X : ι → Ω → 𝓧), (∀ (i : ι), Measurable (X i)) ∧ (∀ (i : ι), HasLaw (X i) μ P) ∧ iIndepFun X P ∧ MeasureTheory.IsProbabilityMeasure P