Source indexedlemma · leanprover/lean4:v4.33.0-rc1

MeasureTheory.Measure.map_prod_comap_swap

PFR.Mathlib.MeasureTheory.Measure.Prod · PFR/Mathlib/MeasureTheory/Measure/Prod.lean:15 to 24

Source documentation

The law of $(X, Z)$ is the image of the law of $(Z,X)$ .

Exact Lean statement

lemma map_prod_comap_swap (hX : Measurable X) (hZ : Measurable Z) (μ : Measure Ω) :
    (μ.map (fun ω ↦ (X ω, Z ω))).comap Prod.swap = μ.map (fun ω ↦ (Z ω, X ω))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma map_prod_comap_swap (hX : Measurable X) (hZ : Measurable Z) (μ : Measure Ω) :    (μ.map (fun ω ↦ (X ω, Z ω))).comap Prod.swap = μ.map (fun ω ↦ (Z ω, X ω)) := by  ext s hs  rw [Measure.map_apply (hZ.prodMk hX) hs, Measure.comap_apply _ Prod.swap_injective _ _ hs]  · rw [Measure.map_apply (hX.prodMk hZ)]    · congr!      ext ω      simp only [Set.image_swap_eq_preimage_swap, Set.mem_preimage, Prod.swap_prod_mk]    · exact MeasurableEquiv.prodComm.measurableEmbedding.measurableSet_image' hs  · exact fun t ht ↦ MeasurableEquiv.prodComm.measurableEmbedding.measurableSet_image' ht