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

ProbabilityTheory.independent_copies_two

PFR.Mathlib.Probability.IdentDistrib · PFR/Mathlib/Probability/IdentDistrib.lean:246 to 260

Source documentation

For X, Y random variables, one can find independent copies X', Y' of X, Y. Version formulated in spaces with a canonical measures.

Exact Lean statement

lemma independent_copies_two {Ω : Type u} {Ω' : Type v} [MeasureSpace Ω] [MeasureSpace Ω']
    [IsProbabilityMeasure (ℙ : Measure Ω)] [IsProbabilityMeasure (ℙ : Measure Ω')]
    {X : Ω → α} {Y : Ω' → β} (hX : Measurable X) (hY : Measurable Y) :
    ∃ (Ω'' : Type (max u v)) (m'' : MeasureSpace Ω'') (X' : Ω'' → α) (Y' : Ω'' → β),
    IsProbabilityMeasure (ℙ : Measure Ω'') ∧ 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_two {Ω : Type u} {Ω' : Type v} [MeasureSpace Ω] [MeasureSpace Ω']    [IsProbabilityMeasure (ℙ : Measure Ω)] [IsProbabilityMeasure (ℙ : Measure Ω')]    {X : Ω → α} {Y : Ω' → β} (hX : Measurable X) (hY : Measurable Y) :    ∃ (Ω'' : Type (max u v)) (m'' : MeasureSpace Ω'') (X' : Ω'' → α) (Y' : Ω'' → β),    IsProbabilityMeasure (ℙ : Measure Ω'') ∧ Measurable X' ∧ Measurable Y' ∧      IndepFun X' Y' ∧ IdentDistrib X' X ∧ IdentDistrib Y' Y := by  refine ⟨Ω × Ω', by infer_instance, X ∘ Prod.fst, Y ∘ Prod.snd, by infer_instance,    hX.comp measurable_fst, hY.comp measurable_snd, ?_, ?_, ?_⟩  · exact indepFun_fst_snd.comp hX hY  · refine ⟨(hX.comp measurable_fst).aemeasurable, hX.aemeasurable, ?_⟩    have : (ℙ : Measure (Ω × Ω')) = (ℙ : Measure Ω).prod (ℙ : Measure Ω') := rfl    simp [← Measure.map_map hX measurable_fst, this]  · refine ⟨(hY.comp measurable_snd).aemeasurable, hY.aemeasurable, ?_⟩    have : (ℙ : Measure (Ω × Ω')) = (ℙ : Measure Ω).prod (ℙ : Measure Ω') := rfl    simp [← Measure.map_map hY measurable_snd, this]