LeanMachineLearning exposition

ProbabilityTheory.iIndepFun_map_iff🔗

Minimal Lean file

iIndepFun_map_iff🔗

LemmaProbabilityTheory.iIndepFun_map_iff
Details

No docstring.

🔗theorem
ProbabilityTheory.iIndepFun_map_iff.{u_2, u_3, u_4, u_5} {Ω : Type u_2}
  {Ω' : Type u_3} {E : Type u_4} {ι : Type u_5} [Countable ι]
  {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
  {mE : MeasurableSpace E} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {X : ι → Ω' → E} {f : Ω → Ω'}
  (hf : AEMeasurable f μ)
  (hX : ∀ (n : ι), AEMeasurable (X n) (MeasureTheory.Measure.map f μ)) :
  iIndepFun X (MeasureTheory.Measure.map f μ) ↔
    iIndepFun (fun n => X n ∘ f) μ
ProbabilityTheory.iIndepFun_map_iff.{u_2,
    u_3, u_4, u_5}
  {Ω : Type u_2} {Ω' : Type u_3}
  {E : Type u_4} {ι : Type u_5}
  [Countable ι] {mΩ : MeasurableSpace Ω}
  {mΩ' : MeasurableSpace Ω'}
  {mE : MeasurableSpace E}
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ]
  {X : ι → Ω' → E} {f : Ω → Ω'}
  (hf : AEMeasurable f μ)
  (hX :
    ∀ (n : ι),
      AEMeasurable (X n)
        (MeasureTheory.Measure.map f μ)) :
  iIndepFun X
      (MeasureTheory.Measure.map f μ) ↔
    iIndepFun (fun n => X n ∘ f) μ

Code

lemma iIndepFun_map_iff [IsProbabilityMeasure μ] {X : ι → Ω' → E} {f : Ω → Ω'}
    (hf : AEMeasurable f μ) (hX : ∀ n, AEMeasurable (X n) (μ.map f)) :
    iIndepFun X (μ.map f) ↔ iIndepFun (fun n ↦ X n ∘ f) μ

Actions: Source · Open Issue

Proof
by
  have := Measure.isProbabilityMeasure_map hf (μ := μ)
  rw [iIndepFun_iff_map_fun_eq_infinitePi_map₀' hX,
    iIndepFun_iff_map_fun_eq_infinitePi_map₀' (by fun_prop)]
  rw [AEMeasurable.map_map_of_aemeasurable (by fun_prop) hf]
  congr! 3
  rw [AEMeasurable.map_map_of_aemeasurable (hX _) hf]