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

ProbabilityTheory.identDistrib_ulift_self

PFR.Mathlib.Probability.IdentDistrib · PFR/Mathlib/Probability/IdentDistrib.lean:179 to 189

Mathematical statement

Exact Lean statement

lemma identDistrib_ulift_self {X : Ω → α} (hX : Measurable X) :
    IdentDistrib X (X ∘ ULift.down) μ (μ.comap ULift.down)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma identDistrib_ulift_self {X : Ω → α} (hX : Measurable X) :    IdentDistrib X (X ∘ ULift.down) μ (μ.comap ULift.down) := by  have hX' : Measurable (X ∘ ULift.down : ULift Ω → α) := hX.comp measurable_down  refine ⟨hX.aemeasurable, hX'.aemeasurable, ?_⟩  ext s hs  rw [Measure.map_apply (μ := (μ.comap ULift.down)) hX' hs,    Measure.comap_apply _ ULift.down_injective _ _ (hX' hs), Set.preimage_comp,    Set.image_preimage_eq _ ULift.down_surjective, Measure.map_apply hX hs]  intro s hs  change MeasurableSet (ULift.down ⁻¹' (ULift.down '' s))  rwa [Set.preimage_image_eq _ ULift.down_injective]