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

ProbabilityTheory.CondIndepFun.comp_right

PFR.ForMathlib.ConditionalIndependence · PFR/ForMathlib/ConditionalIndependence.lean:114 to 121

Source documentation

Composing independent functions with a measurable embedding of conull range gives independent functions.

Exact Lean statement

lemma CondIndepFun.comp_right {i : Ω' → Ω} (hi : MeasurableEmbedding i) (hi' : ∀ᵐ a ∂μ, a ∈ range i)
    (hf : Measurable f) (hg : Measurable g) (hh : Measurable h) (hfg : CondIndepFun f g h μ) :
    CondIndepFun (f ∘ i) (g ∘ i) (h ∘ i) (μ.comap i)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma CondIndepFun.comp_right {i : Ω' → Ω} (hi : MeasurableEmbedding i) (hi' : ∀ᵐ a ∂μ, a ∈ range i)    (hf : Measurable f) (hg : Measurable g) (hh : Measurable h) (hfg : CondIndepFun f g h μ) :    CondIndepFun (f ∘ i) (g ∘ i) (h ∘ i) (μ.comap i) := by  rw [condIndepFun_iff] at hfg ⊢  rw [← Measure.map_map hh hi.measurable, hi.map_comap, restrict_eq_self_of_ae_mem hi']  refine hfg.mono <| fun c hc ↦ ?_  rw [preimage_comp, ← comap_cond hi hi' <| hh <| .singleton _]  exact IndepFun.comp_right hi (cond_absolutelyContinuous.ae_le hi') hf hg hc