LeanMachineLearning exposition

MeasureTheory.Integrable.congr_identDistrib🔗

Minimal Lean file

congr_identDistrib🔗

LemmaMeasureTheory.Integrable.congr_identDistrib
Details

No docstring.

🔗theorem
MeasureTheory.Integrable.congr_identDistrib.{u_1, u_2} {Ω : Type u_1}
  {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
  {μ : Measure Ω} {μ' : Measure Ω'} {X : Ω → ℝ} {Y : Ω' → ℝ}
  (hX : Integrable X μ)
  (hXY : ProbabilityTheory.IdentDistrib X Y μ μ') : Integrable Y μ'
MeasureTheory.Integrable.congr_identDistrib.{u_1,
    u_2}
  {Ω : Type u_1} {Ω' : Type u_2}
  {mΩ : MeasurableSpace Ω}
  {mΩ' : MeasurableSpace Ω'}
  {μ : Measure Ω} {μ' : Measure Ω'}
  {X : Ω → ℝ} {Y : Ω' → ℝ}
  (hX : Integrable X μ)
  (hXY :
    ProbabilityTheory.IdentDistrib X Y μ
      μ') :
  Integrable Y μ'

Code

lemma Integrable.congr_identDistrib {Ω Ω' : Type*}
    {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'}
    {μ : Measure Ω} {μ' : Measure Ω'} {X : Ω → ℝ} {Y : Ω' → ℝ}
    (hX : Integrable X μ) (hXY : IdentDistrib X Y μ μ') :
    Integrable Y μ'
Used by (1)

Actions: Source · Open Issue

Proof
by
  have hX' : Integrable id (μ.map X) := by
    rwa [integrable_map_measure (by fun_prop) hXY.aemeasurable_fst]
  rw [hXY.map_eq] at hX'
  rwa [integrable_map_measure (by fun_prop) hXY.aemeasurable_snd] at hX'