Mathlib.CondIndep.DomainTransport
Conditional-independence transport across measurable sample-domain maps that preserve the finite measures and are mutual inverses only almost everywhere.
AeRetraction 1 core · 6 supporting This module transports conditional expectations and conditional independence between finite standard-Borel sample spaces linked by measurable maps that preserve the two measures and are mutual inverses only almost everyw ★ condIndepFun_comp_aeEquiv_iff
Conditional independence under almost-everywhere domain retractions
This module transports conditional expectations and conditional independence between finite standard-Borel sample spaces linked by measurable maps that preserve the two measures and are mutual inverses only almost everywhere. It therefore applies to a full-measure support embedded non-surjectively in an ambient sample space, not only to genuine measurable equivalences.
theorem condIndepFun_comp_aeEquiv_iff reviewed
⚑ flagged
Causalean
Let the source and target be standard Borel spaces carrying finite measures. With measurable maps in both directions, their two pushforward identities, an almost-everywhere right-inverse identity, three target random variables, and their measurability, conditional independence of the first two variables given the third is equivalent to conditional independence of their pullbacks given the pulled-back third variable.
Formal statement
Proof (Lean source)
theorem condIndepFun_comp_aeEquiv_iff
{Ω Ω' 𝒳 𝒴 𝒵 : Type*}
[mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω]
[mΩ' : MeasurableSpace Ω'] [StandardBorelSpace Ω']
[MeasurableSpace 𝒳] [MeasurableSpace 𝒴] [MeasurableSpace 𝒵]
(r : Ω → Ω') (s : Ω' → Ω) (hr : Measurable r) (hs : Measurable s)
{μ : Measure Ω} {μ' : Measure Ω'}
[IsFiniteMeasure μ] [IsFiniteMeasure μ']
(hmap_r : Measure.map r μ = μ') (hmap_s : Measure.map s μ' = μ)
(hrs : r ∘ s =ᵐ[μ'] id)
(X : Ω' → 𝒳) (Y : Ω' → 𝒴) (Z : Ω' → 𝒵)
(hX : Measurable X) (hY : Measurable Y) (hZ : Measurable Z) :
CondIndepFun
(comap (Z ∘ r) inferInstance)
(mΩ := mΩ) (hZ.comp hr).comap_le
(X ∘ r) (Y ∘ r) μ ↔
CondIndepFun
(comap Z inferInstance)
(mΩ := mΩ') hZ.comap_le X Y μ' := by
rw [ProbabilityTheory.condIndepFun_iff_condIndep,
ProbabilityTheory.condIndepFun_iff_condIndep]
simpa only [MeasurableSpace.comap_comp] using
condIndep_comap_aeEquiv_iff r s hr hs hmap_r hmap_s hrs
(comap X inferInstance)
(comap Y inferInstance)
(comap Z inferInstance)
hX.comap_le hY.comap_le hZ.comap_le
6 supporting declarations (lemmas, instances)
-
eventuallyEq_of_comp_aeRetractiontheorem — With a source-to-target map, a measurable return map, the return-map pushforward identity, an almost-everywhere right-inverse identity, and an equality after pullback, the target functions agree almost everywhere.hypothesesΩ Ω' A :r :Ω → Ω's :Ω' → Ωhs :μ :Measure Ωμ' :Measure Ω'hmap_s :Measure.map s μ' = μhrs :r ∘ s =ᵐ[μ'] idf g :Ω' → Ahfg :f ∘ r =ᵐ[μ] g ∘ rconclusionf =ᵐ[μ'] gProof (Lean source)
theorem eventuallyEq_of_comp_aeRetraction {Ω Ω' A : Type*} [MeasurableSpace Ω] [MeasurableSpace Ω'] (r : Ω → Ω') (s : Ω' → Ω) (hs : Measurable s) {μ : Measure Ω} {μ' : Measure Ω'} (hmap_s : Measure.map s μ' = μ) (hrs : r ∘ s =ᵐ[μ'] id) {f g : Ω' → A} (hfg : f ∘ r =ᵐ[μ] g ∘ r) : f =ᵐ[μ'] g := by have hfg_map : f ∘ r =ᵐ[Measure.map s μ'] g ∘ r := by rw [hmap_s] exact hfg have hfg_s : (f ∘ r) ∘ s =ᵐ[μ'] (g ∘ r) ∘ s := ae_of_ae_map hs.aemeasurable hfg_map filter_upwards [hfg_s, hrs] with y hy hry change f (r (s y)) = g (r (s y)) at hy change r (s y) = y at hry simpa [hry] using hy -
condExp_comp_of_map_eqtheorem — With a measurable source-to-target map, its pushforward identity, a target conditioning σ-algebra contained in the ambient σ-algebra, and an integrable target outcome, conditional expectation commutes almost everywhere with pullback along the map.hypothesesΩ Ω' E :r :Ω → Ω'hr :μ :Measure Ωμ' :Measure Ω'hmap_r :Measure.map r μ = μ'm :hm :m ≤ mΩ'f :Ω' → Ehf :Integrable f μ'Proof (Lean source)
theorem condExp_comp_of_map_eq {Ω Ω' E : Type*} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (r : Ω → Ω') (hr : Measurable r) {μ : Measure Ω} {μ' : Measure Ω'} [IsFiniteMeasure μ] [IsFiniteMeasure μ'] (hmap_r : Measure.map r μ = μ') (m : MeasurableSpace Ω') (hm : m ≤ mΩ') {f : Ω' → E} (hf : Integrable f μ') : @condExp Ω E (comap r m) mΩ _ _ μ (f ∘ r) =ᵐ[μ] (@condExp Ω' E m mΩ' _ _ μ' f) ∘ r := by have hcm : comap r m ≤ mΩ := (comap_mono hm).trans hr.comap_le have : IsFiniteMeasure (μ.trim hcm) := isFiniteMeasure_trim hcm have : SigmaFinite (μ.trim hcm) := inferInstance have : IsFiniteMeasure (μ'.trim hm) := isFiniteMeasure_trim hm have : SigmaFinite (μ'.trim hm) := inferInstance let g : Ω' → E := @condExp Ω' E m mΩ' _ _ μ' f have hf_map : Integrable f (@Measure.map Ω Ω' mΩ mΩ' r μ) := by rw [hmap_r] exact hf have hf_comp : Integrable (f ∘ r) μ := @Integrable.comp_aemeasurable Ω E mΩ μ _ _ Ω' mΩ' r f hf_map (@aemeasurable Ω Ω' mΩ mΩ' r μ hr) have hg_mu' : Integrable g μ' := by exact @integrable_condExp Ω' E m mΩ' μ' f _ _ _ have hg_map : Integrable g (@Measure.map Ω Ω' mΩ mΩ' r μ) := by rw [hmap_r] exact hg_mu' have hg_comp : Integrable (g ∘ r) μ := @Integrable.comp_aemeasurable Ω E mΩ μ _ _ Ω' mΩ' r g hg_map (@aemeasurable Ω Ω' mΩ mΩ' r μ hr) have hr_comap : @Measurable Ω Ω' (comap r m) m r := Measurable.of_comap_le le_rfl have hg_strong_comap : @StronglyMeasurable Ω E _ (comap r m) (g ∘ r) := (@stronglyMeasurable_condExp Ω' E m mΩ' μ' f _ _).comp_measurable hr_comap have hg_ae : @AEStronglyMeasurable Ω E _ (comap r m) mΩ (g ∘ r) μ := hg_strong_comap.aestronglyMeasurable refine (ae_eq_condExp_of_forall_setIntegral_eq hcm hf_comp (fun s _ _ ↦ hg_comp.integrableOn) (fun s hs _ ↦ ?_) hg_ae).symm rcases hs with ⟨t, ht, rfl⟩ calc ∫ x in r ⁻¹' t, g (r x) ∂μ = ∫ y in t, g y ∂(@Measure.map Ω Ω' mΩ mΩ' r μ) := (@setIntegral_map Ω E mΩ _ _ μ Ω' mΩ' r g t (hm _ ht) hg_map.aestronglyMeasurable (@aemeasurable Ω Ω' mΩ mΩ' r μ hr)).symm _ = ∫ y in t, g y ∂μ' := by rw [hmap_r] _ = ∫ y in t, f y ∂μ' := @setIntegral_condExp Ω' E m mΩ' μ' f t _ _ _ hm _ hf ht _ = ∫ y in t, f y ∂(@Measure.map Ω Ω' mΩ mΩ' r μ) := by rw [hmap_r] _ = ∫ x in r ⁻¹' t, f (r x) ∂μ := @setIntegral_map Ω E mΩ _ _ μ Ω' mΩ' r f t (hm _ ht) hf_map.aestronglyMeasurable (@aemeasurable Ω Ω' mΩ mΩ' r μ hr) -
condExpInd_preimage_of_map_eqtheorem — With a measurable source-to-target map, its pushforward identity, a target conditioning σ-algebra contained in the ambient σ-algebra, and a measurable target event, the event's conditional probability commutes almost everywhere with pullback along the map.hypothesesΩ Ω' :r :Ω → Ω'hr :μ :Measure Ωμ' :Measure Ω'hmap_r :Measure.map r μ = μ'm :hm :m ≤ mΩ't :Set Ω'ht :@MeasurableSet Ω' mΩ' tProof (Lean source)
theorem condExpInd_preimage_of_map_eq {Ω Ω' : Type*} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] (r : Ω → Ω') (hr : Measurable r) {μ : Measure Ω} {μ' : Measure Ω'} [IsFiniteMeasure μ] [IsFiniteMeasure μ'] (hmap_r : Measure.map r μ = μ') (m : MeasurableSpace Ω') (hm : m ≤ mΩ') {t : Set Ω'} (ht : @MeasurableSet Ω' mΩ' t) : @condExp Ω ℝ (comap r m) mΩ _ _ μ ((r ⁻¹' t).indicator fun _ ↦ (1 : ℝ)) =ᵐ[μ] (@condExp Ω' ℝ m mΩ' _ _ μ' (t.indicator fun _ ↦ (1 : ℝ))) ∘ r := by have h := @condExp_comp_of_map_eq Ω Ω' ℝ mΩ mΩ' _ _ _ r hr μ μ' _ _ hmap_r m hm (t.indicator fun _ ↦ (1 : ℝ)) ((integrable_const (1 : ℝ)).indicator ht) have hfun : (t.indicator fun _ ↦ (1 : ℝ)) ∘ r = (r ⁻¹' t).indicator fun _ ↦ (1 : ℝ) := by funext x by_cases hx : r x ∈ t <;> simp [Function.comp_apply, hx] simpa only [hfun] using h -
condIndep_comap_of_map_eqtheorem — With a measurable source-to-target map, its pushforward identity, three target σ-algebras contained in the target ambient σ-algebra, conditional independence on the target pulls back to conditional independence on the source.hypothesesΩ Ω' :r :Ω → Ω'hr :μ :Measure Ωμ' :Measure Ω'hmap_r :Measure.map r μ = μ'mX mY mZ :hX :mX ≤ mΩ'hY :mY ≤ mΩ'hZ :mZ ≤ mΩ'@CondIndep Ω' mZ mX mY mΩ' (by infer_instance) hZ μ' (by infer_instance)conclusion@CondIndep Ω (comap r mZ) (comap r mX) (comap r mY) mΩ (by infer_instance) ((comap_mono hZ).trans hr.comap_le) μ (by infer_instance)Proof (Lean source)
theorem condIndep_comap_of_map_eq {Ω Ω' : Type*} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [mΩ' : MeasurableSpace Ω'] [StandardBorelSpace Ω'] (r : Ω → Ω') (hr : Measurable r) {μ : Measure Ω} {μ' : Measure Ω'} [IsFiniteMeasure μ] [IsFiniteMeasure μ'] (hmap_r : Measure.map r μ = μ') (mX mY mZ : MeasurableSpace Ω') (hX : mX ≤ mΩ') (hY : mY ≤ mΩ') (hZ : mZ ≤ mΩ') : @CondIndep Ω' mZ mX mY mΩ' (by infer_instance) hZ μ' (by infer_instance) → @CondIndep Ω (comap r mZ) (comap r mX) (comap r mY) mΩ (by infer_instance) ((comap_mono hZ).trans hr.comap_le) μ (by infer_instance) := by have hcomapX : comap r mX ≤ mΩ := (comap_mono hX).trans hr.comap_le have hcomapY : comap r mY ≤ mΩ := (comap_mono hY).trans hr.comap_le have hr_ae : @AEMeasurable Ω Ω' mΩ' mΩ r μ := @aemeasurable Ω Ω' mΩ mΩ' r μ hr have transport (u : Set Ω') (hu : @MeasurableSet Ω' mΩ' u) : @condExp Ω ℝ (comap r mZ) mΩ _ _ μ ((r ⁻¹' u).indicator fun _ ↦ (1 : ℝ)) =ᵐ[μ] (@condExp Ω' ℝ mZ mΩ' _ _ μ' (u.indicator fun _ ↦ (1 : ℝ))) ∘ r := @condExpInd_preimage_of_map_eq Ω Ω' mΩ mΩ' r hr μ μ' _ _ hmap_r mZ hZ u hu rw [ProbabilityTheory.condIndep_iff _ _ _ _ hX hY, ProbabilityTheory.condIndep_iff _ _ _ _ hcomapX hcomapY] intro h s t hs ht rcases hs with ⟨s, hs, rfl⟩ rcases ht with ⟨t, ht, rfl⟩ have hs' : @MeasurableSet Ω' mΩ' s := hX s hs have ht' : @MeasurableSet Ω' mΩ' t := hY t ht have hst' : @MeasurableSet Ω' mΩ' (s ∩ t) := hs'.inter ht' have htarget := h s t hs ht let cst : Ω' → ℝ := @condExp Ω' ℝ mZ mΩ' _ _ μ' ((s ∩ t).indicator fun _ ↦ (1 : ℝ)) let cs : Ω' → ℝ := @condExp Ω' ℝ mZ mΩ' _ _ μ' (s.indicator fun _ ↦ (1 : ℝ)) let ct : Ω' → ℝ := @condExp Ω' ℝ mZ mΩ' _ _ μ' (t.indicator fun _ ↦ (1 : ℝ)) change ∀ᵐ y ∂μ', cst y = cs y * ct y at htarget have hmap : ∀ᵐ y ∂(@Measure.map Ω Ω' mΩ mΩ' r μ), cst y = cs y * ct y := by rw [hmap_r] exact htarget have htarget' : ∀ᵐ x ∂μ, cst (r x) = cs (r x) * ct (r x) := ae_of_ae_map hr_ae hmap have htarget_eq : (cst ∘ r) =ᵐ[μ] (cs ∘ r) * (ct ∘ r) := by filter_upwards [htarget'] with x hx exact hx have hinter := transport (s ∩ t) hst' have hleft := transport s hs' have hright := transport t ht' simpa only [cst, cs, ct, Set.preimage_inter, Pi.mul_apply, Function.comp_apply] using hinter.trans (htarget_eq.trans (hleft.mul hright).symm) -
condIndep_of_comap_aeRetractiontheorem — With measurable maps in both directions, their two pushforward identities, an almost-everywhere right inverse, and three target σ-algebras contained in the target ambient σ-algebra, conditional independence of the three pullback σ-algebras implies target conditional independence.hypothesesΩ Ω' :r :Ω → Ω's :Ω' → Ωhr :hs :μ :Measure Ωμ' :Measure Ω'hmap_r :Measure.map r μ = μ'hmap_s :Measure.map s μ' = μhrs :r ∘ s =ᵐ[μ'] idmX mY mZ :hX :mX ≤ mΩ'hY :mY ≤ mΩ'hZ :mZ ≤ mΩ'@CondIndep Ω (comap r mZ) (comap r mX) (comap r mY) mΩ (by infer_instance) ((comap_mono hZ).trans hr.comap_le) μ (by infer_instance)conclusion@CondIndep Ω' mZ mX mY mΩ' (by infer_instance) hZ μ' (by infer_instance)Proof (Lean source)
theorem condIndep_of_comap_aeRetraction {Ω Ω' : Type*} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [mΩ' : MeasurableSpace Ω'] [StandardBorelSpace Ω'] (r : Ω → Ω') (s : Ω' → Ω) (hr : Measurable r) (hs : Measurable s) {μ : Measure Ω} {μ' : Measure Ω'} [IsFiniteMeasure μ] [IsFiniteMeasure μ'] (hmap_r : Measure.map r μ = μ') (hmap_s : Measure.map s μ' = μ) (hrs : r ∘ s =ᵐ[μ'] id) (mX mY mZ : MeasurableSpace Ω') (hX : mX ≤ mΩ') (hY : mY ≤ mΩ') (hZ : mZ ≤ mΩ') : @CondIndep Ω (comap r mZ) (comap r mX) (comap r mY) mΩ (by infer_instance) ((comap_mono hZ).trans hr.comap_le) μ (by infer_instance) → @CondIndep Ω' mZ mX mY mΩ' (by infer_instance) hZ μ' (by infer_instance) := by have hcomapX : comap r mX ≤ mΩ := (comap_mono hX).trans hr.comap_le have hcomapY : comap r mY ≤ mΩ := (comap_mono hY).trans hr.comap_le have transport (u : Set Ω') (hu : @MeasurableSet Ω' mΩ' u) : @condExp Ω ℝ (comap r mZ) mΩ _ _ μ ((r ⁻¹' u).indicator fun _ ↦ (1 : ℝ)) =ᵐ[μ] (@condExp Ω' ℝ mZ mΩ' _ _ μ' (u.indicator fun _ ↦ (1 : ℝ))) ∘ r := @condExpInd_preimage_of_map_eq Ω Ω' mΩ mΩ' r hr μ μ' _ _ hmap_r mZ hZ u hu rw [ProbabilityTheory.condIndep_iff _ _ _ _ hcomapX hcomapY, ProbabilityTheory.condIndep_iff _ _ _ _ hX hY] intro h u v hu hv have hpre := h (r ⁻¹' u) (r ⁻¹' v) ⟨u, hu, rfl⟩ ⟨v, hv, rfl⟩ have hu' : @MeasurableSet Ω' mΩ' u := hX u hu have hv' : @MeasurableSet Ω' mΩ' v := hY v hv have huv' : @MeasurableSet Ω' mΩ' (u ∩ v) := hu'.inter hv' have hinter := transport (u ∩ v) huv' have hleft := transport u hu' have hright := transport v hv' have hpull := hinter.symm.trans (hpre.trans (hleft.mul hright)) let cuv : Ω' → ℝ := @condExp Ω' ℝ mZ mΩ' _ _ μ' ((u ∩ v).indicator fun _ ↦ (1 : ℝ)) let cu : Ω' → ℝ := @condExp Ω' ℝ mZ mΩ' _ _ μ' (u.indicator fun _ ↦ (1 : ℝ)) let cv : Ω' → ℝ := @condExp Ω' ℝ mZ mΩ' _ _ μ' (v.indicator fun _ ↦ (1 : ℝ)) change (cuv ∘ r) =ᵐ[μ] ((fun y ↦ cu y * cv y) ∘ r) at hpull change cuv =ᵐ[μ'] fun y ↦ cu y * cv y exact @eventuallyEq_of_comp_aeRetraction Ω Ω' ℝ mΩ mΩ' r s hs μ μ' hmap_s hrs cuv (fun y ↦ cu y * cv y) hpull -
condIndep_comap_aeEquiv_ifftheorem — Let the source and target be standard Borel spaces carrying finite measures. With measurable maps in both directions, their two pushforward identities, an almost-everywhere right-inverse identity, and three target σ-algebras contained in the target ambient σ-algebra, target conditional independence is equivalent to conditional independence of the three pullback σ-algebras.hypothesesProof (Lean source)
theorem condIndep_comap_aeEquiv_iff {Ω Ω' : Type*} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] [mΩ' : MeasurableSpace Ω'] [StandardBorelSpace Ω'] (r : Ω → Ω') (s : Ω' → Ω) (hr : Measurable r) (hs : Measurable s) {μ : Measure Ω} {μ' : Measure Ω'} [IsFiniteMeasure μ] [IsFiniteMeasure μ'] (hmap_r : Measure.map r μ = μ') (hmap_s : Measure.map s μ' = μ) (hrs : r ∘ s =ᵐ[μ'] id) (mX mY mZ : MeasurableSpace Ω') (hX : mX ≤ mΩ') (hY : mY ≤ mΩ') (hZ : mZ ≤ mΩ') : @CondIndep Ω (comap r mZ) (comap r mX) (comap r mY) mΩ (by infer_instance) ((comap_mono hZ).trans hr.comap_le) μ (by infer_instance) ↔ @CondIndep Ω' mZ mX mY mΩ' (by infer_instance) hZ μ' (by infer_instance) := by constructor · exact condIndep_of_comap_aeRetraction (mΩ := mΩ) (mΩ' := mΩ') (r := r) (s := s) (μ := μ) (μ' := μ') hr hs hmap_r hmap_s hrs (mX := mX) (mY := mY) (mZ := mZ) hX hY hZ · exact condIndep_comap_of_map_eq (mΩ := mΩ) (mΩ' := mΩ') (r := r) (μ := μ) (μ' := μ') hr hmap_r (mX := mX) (mY := mY) (mZ := mZ) hX hY hZ