Conditional expectation and conditional independence along a factor map

If T carries P to μ, then conditioning under μ on a sub-σ-algebra m is computed under P by conditioning on the pullback algebra m.comap T:

(μ[g | m]) ∘ T =ᵐ[P] P[g ∘ T | m.comap T]

and consequently mutual conditional independence of a family under μ pulls back to mutual conditional independence of the composed family under P, conditioned on the pullback algebra.

This is how facts proved on a factor — here, a marginal of a coupling — are consumed on the coupling itself: every function in sight factors through the projection, and the conditioning algebra travels by comap. Mathlib's CondIndepFun.comp composes on the codomain side only; the domain-side transport along a measure-preserving map is what this file adds.

Proof

The usual uniqueness argument, with the transported function as candidate: (μ[g | m]) ∘ T is m.comap T-strongly measurable outright, and its integral over a pullback set T ⁻¹' s is computed by the change-of-variables formula, setIntegral_condExp on the factor, and the same formula back. No structure on the fibres of T is used.

Contents

• MeasureTheory.condExp_comp_measurePreserving;
• ProbabilityTheory.condExp_set_comp_measurePreserving — the single-event form, shared by both independence transports;
• ProbabilityTheory.condIndepFun_comp_measurePreserving — the two-function transport;
• ProbabilityTheory.iCondIndepFun_comp_measurePreserving — the family transport.

[StandardBorelSpace] hypotheses appear only on the conditional-independence statements, forced by Mathlib defining conditional independence through condExpKernel; the conditional-expectation transport itself is for arbitrary finite measures.

theorem MeasureTheory.condExp_comp_measurePreserving {α : Type u_1} {β : Type u_2} {E : Type u_3} {m : MeasurableSpace β} [mα : MeasurableSpace α] [mβ : MeasurableSpace β] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {P : Measure α} {μ : Measure β} {T : α → β} [IsFiniteMeasure μ] (hT : MeasurePreserving T P μ) (hm : m ≤ mβ) {g : β → E} (hg : Integrable g μ) : μ[g | m] ∘ T =ᵐ[P] P[g ∘ T | MeasurableSpace.comap T m]

Conditional expectation along a factor map. If T carries P to μ, conditioning under μ on m and transporting agrees a.e. with conditioning the transported function under P on the pullback algebra m.comap T.

theorem ProbabilityTheory.condExp_set_comp_measurePreserving {α : Type u_1} {β : Type u_2} {m' : MeasurableSpace β} [mα : MeasurableSpace α] [mβ : MeasurableSpace β] {P : MeasureTheory.Measure α} {μ : MeasureTheory.Measure β} [MeasureTheory.IsFiniteMeasure μ] {T : α → β} (hT : MeasureTheory.MeasurePreserving T P μ) (hm' : m' ≤ mβ) {E : Set β} (hE : MeasurableSet E) : P[(T ⁻¹' E).indicator fun (ω : α) => 1 | MeasurableSpace.comap T m'] =ᵐ[P] μ[E.indicator fun (ω : β) => 1 | m'] ∘ T

The single-event form: the conditional probability of a pulled-back event, conditioned on the pullback algebra, is the transported conditional probability of the event. No standard Borel hypothesis — this is pure conditional expectation.

theorem ProbabilityTheory.condIndepFun_comp_measurePreserving {α : Type u_1} {β : Type u_2} {m' : MeasurableSpace β} [mα : MeasurableSpace α] [mβ : MeasurableSpace β] [StandardBorelSpace α] [StandardBorelSpace β] {P : MeasureTheory.Measure α} {μ : MeasureTheory.Measure β} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure μ] {T : α → β} (hT : MeasureTheory.MeasurePreserving T P μ) (hm' : m' ≤ mβ) {γ : Type u_3} {γ' : Type u_4} {mγ : MeasurableSpace γ} {mγ' : MeasurableSpace γ'} {f : β → γ} {g : β → γ'} (hf : Measurable f) (hg : Measurable g) (h : CondIndepFun m' hm' f g μ) : CondIndepFun (MeasurableSpace.comap T m') ⋯ (f ∘ T) (g ∘ T) P

Conditional independence of a pair pulls back along a factor map: two functions conditionally independent under the factor law, given m', compose with the factor map to functions conditionally independent under the source law, given the pullback algebra.

theorem ProbabilityTheory.iCondIndepFun_comp_measurePreserving {α : Type u_1} {β : Type u_2} {m' : MeasurableSpace β} [mα : MeasurableSpace α] [mβ : MeasurableSpace β] [StandardBorelSpace α] [StandardBorelSpace β] {P : MeasureTheory.Measure α} {μ : MeasureTheory.Measure β} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure μ] {T : α → β} (hT : MeasureTheory.MeasurePreserving T P μ) (hm' : m' ≤ mβ) {ι : Type u_3} {γ : ι → Type u_4} [mγ : (i : ι) → MeasurableSpace (γ i)] {Y : (i : ι) → β → γ i} (hY : ∀ (i : ι), Measurable (Y i)) (h : iCondIndepFun m' hm' Y μ) : iCondIndepFun (MeasurableSpace.comap T m') ⋯ (fun (i : ι) => Y i ∘ T) P

Mutual conditional independence pulls back along a factor map. A family that is mutually conditionally independent under the factor law, given m', is — after composing with the factor map — mutually conditionally independent under the source law, given the pullback algebra m'.comap T.