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

ProbabilityTheory.independent_copies

PFR.Mathlib.Probability.IdentDistrib · PFR/Mathlib/Probability/IdentDistrib.lean:233 to 242

Source documentation

For X, Y random variables, one can find independent copies X', Y' of X, Y.

Exact Lean statement

lemma independent_copies {X : Ω → α} {Y : Ω' → β} (hX : Measurable X) (hY : Measurable Y)
    (μ : Measure Ω) (μ' : Measure Ω') [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] :
    ∃ ν : Measure (α × β), ∃ X' : α × β → α, ∃ Y' : α × β → β, IsProbabilityMeasure ν
      ∧ Measurable X' ∧ Measurable Y' ∧ IndepFun X' Y' ν
      ∧ IdentDistrib X' X ν μ ∧ IdentDistrib Y' Y ν μ'

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma independent_copies {X : Ω → α} {Y : Ω' → β} (hX : Measurable X) (hY : Measurable Y)    (μ : Measure Ω) (μ' : Measure Ω') [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] :    ∃ ν : Measure (α × β), ∃ X' : α × β → α, ∃ Y' : α × β → β, IsProbabilityMeasure ν      ∧ Measurable X' ∧ Measurable Y' ∧ IndepFun X' Y' ν      ∧ IdentDistrib X' X ν μ ∧ IdentDistrib Y' Y ν μ' := by  have := Measure.isProbabilityMeasure_map hX.aemeasurable (μ := μ)  have := Measure.isProbabilityMeasure_map hY.aemeasurable (μ := μ')  exact ⟨(μ.map X).prod (μ'.map Y), _, _, inferInstance, measurable_fst, measurable_snd,    indepFun_fst_snd, ⟨measurable_fst.aemeasurable, hX.aemeasurable, by simp⟩,    measurable_snd.aemeasurable, hY.aemeasurable, by simp⟩