Invariance of conditional laws

If a measure-preserving map fixes every event of a conditioning σ-algebra up to null sets, then almost every conditional law is invariant under that map. This is the invariance step in decomposing a probability law into invariant components. The conditioning σ-algebra need not be countably generated; standard Borelness is required only of the space carrying the conditional laws.

The proof uses Mathlib's kernel uniqueness (Kernel.ae_eq_of_compProd_eq): pushing forward the second coordinate of the conditional joint law leaves its values on rectangles unchanged.

theorem TauCeti.Probability.map_condExpKernel_ae_eq_of_invariant {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (hm : m ≤ mΩ) {T : Ω → Ω} (hT : MeasureTheory.MeasurePreserving T μ μ) (hinv : ∀ (s : Set Ω), MeasurableSet s → T ⁻¹' s =ᵐ[μ] s) : ∀ᵐ (x : Ω) ∂μ, MeasureTheory.Measure.map T ((ProbabilityTheory.condExpKernel μ m) x) = (ProbabilityTheory.condExpKernel μ m) x

Conditioning on events fixed almost surely by a measure-preserving transformation gives conditional laws that are almost surely invariant under that transformation.