LeanMachineLearning exposition

ProbabilityTheory.identDistrib_map_left_iff🔗

Minimal Lean file

identDistrib_map_left_iff🔗

LemmaProbabilityTheory.identDistrib_map_left_iff
Details

No docstring.

🔗theorem
ProbabilityTheory.identDistrib_map_left_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 Ω} {X : Ω → E} {Y : Ω' → E} {f : Ω → Ω'}
  (hf : AEMeasurable f ν) (hX : AEMeasurable X μ)
  (hY : AEMeasurable Y (MeasureTheory.Measure.map f ν)) :
  IdentDistrib Y X (MeasureTheory.Measure.map f ν) μ ↔
    IdentDistrib (Y ∘ f) X ν μ
ProbabilityTheory.identDistrib_map_left_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 Ω}
  {X : Ω → E} {Y : Ω' → E} {f : Ω → Ω'}
  (hf : AEMeasurable f ν)
  (hX : AEMeasurable X μ)
  (hY :
    AEMeasurable Y
      (MeasureTheory.Measure.map f ν)) :
  IdentDistrib Y X
      (MeasureTheory.Measure.map f ν) μ ↔
    IdentDistrib (Y ∘ f) X ν μ

Code

lemma identDistrib_map_left_iff {X : Ω → E} {Y : Ω' → E} {f : Ω → Ω'}
    (hf : AEMeasurable f ν) (hX : AEMeasurable X μ) (hY : AEMeasurable Y (ν.map f)) :
    IdentDistrib Y X (ν.map f) μ ↔ IdentDistrib (Y ∘ f) X ν μ
Body uses (2)

Actions: Source · Open Issue

Proof
by
  rw [identDistrib_comm Y, identDistrib_comm _ X]
  exact identDistrib_map_right_iff hf hX hY