LeanMachineLearning exposition

ProbabilityTheory.IndepFun_map_iff🔗

Minimal Lean file

IndepFun_map_iff🔗

LemmaProbabilityTheory.IndepFun_map_iff
Details

No docstring.

🔗theorem
ProbabilityTheory.IndepFun_map_iff.{u_2, u_3, u_4} {Ω : Type u_2}
  {Ω' : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω}
  {mΩ' : MeasurableSpace Ω'} {mE : MeasurableSpace E}
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ]
  {X Y : Ω' → E} {f : Ω → Ω'} (hf : AEMeasurable f μ)
  (hX : AEMeasurable X (MeasureTheory.Measure.map f μ))
  (hY : AEMeasurable Y (MeasureTheory.Measure.map f μ)) :
  IndepFun X Y (MeasureTheory.Measure.map f μ) ↔
    IndepFun (X ∘ f) (Y ∘ f) μ
ProbabilityTheory.IndepFun_map_iff.{u_2,
    u_3, u_4}
  {Ω : Type u_2} {Ω' : Type u_3}
  {E : Type u_4} {mΩ : MeasurableSpace Ω}
  {mΩ' : MeasurableSpace Ω'}
  {mE : MeasurableSpace E}
  {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ]
  {X Y : Ω' → E} {f : Ω → Ω'}
  (hf : AEMeasurable f μ)
  (hX :
    AEMeasurable X
      (MeasureTheory.Measure.map f μ))
  (hY :
    AEMeasurable Y
      (MeasureTheory.Measure.map f μ)) :
  IndepFun X Y
      (MeasureTheory.Measure.map f μ) ↔
    IndepFun (X ∘ f) (Y ∘ f) μ

Code

lemma IndepFun_map_iff [IsFiniteMeasure μ] {X : Ω' → E} {Y : Ω' → E} {f : Ω → Ω'}
    (hf : AEMeasurable f μ) (hX : AEMeasurable X (μ.map f)) (hY : AEMeasurable Y (μ.map f)) :
    X ⟂ᵢ[μ.map f] Y ↔ (X ∘ f) ⟂ᵢ[μ] (Y ∘ f)

Actions: Source · Open Issue

Proof
by
  rw [indepFun_iff_map_prod_eq_prod_map_map hX hY,
    indepFun_iff_map_prod_eq_prod_map_map (by fun_prop) (by fun_prop)]
  rw [AEMeasurable.map_map_of_aemeasurable hY hf, AEMeasurable.map_map_of_aemeasurable hX hf,
    AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
  rfl