LeanMachineLearning exposition

ProbabilityTheory.identDistrib_map_right_iff🔗

Minimal Lean file

identDistrib_map_right_iff🔗

LemmaProbabilityTheory.identDistrib_map_right_iff
Details

No docstring.

🔗theorem
ProbabilityTheory.identDistrib_map_right_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 X Y μ (MeasureTheory.Measure.map f ν) ↔
    IdentDistrib X (Y ∘ f) μ ν
ProbabilityTheory.identDistrib_map_right_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 X Y μ
      (MeasureTheory.Measure.map f ν) ↔
    IdentDistrib X (Y ∘ f) μ ν

Code

lemma identDistrib_map_right_iff {X : Ω → E} {Y : Ω' → E} {f : Ω → Ω'}
    (hf : AEMeasurable f ν) (hX : AEMeasurable X μ) (hY : AEMeasurable Y (ν.map f)) :
    IdentDistrib X Y μ (ν.map f) ↔ IdentDistrib X (Y ∘ f) μ ν
Used by (1)

Actions: Source · Open Issue

Proof
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · constructor
    · exact hX
    · fun_prop
    · rw [h.map_eq, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hf]
  · constructor
    · exact hX
    · fun_prop
    · rw [h.map_eq, AEMeasurable.map_map_of_aemeasurable hY hf]