InformationTheory.Probability.TwoSidedExtension.CondExpMeasurePreserving
Mathlib-gap: condExp commutes with measure-preserving transforms #
For a measure-preserving T : Ω₁ → Ω₂ and n a sub-σ-algebra of m₂,
(μ₂[f | n]) ∘ T =ᵐ μ₁[f ∘ T | n.comap T]. Mathlib provides no direct named
version; proved via ae_eq_condExp_of_forall_setIntegral_eq. Used by
integral_MRatioLowerZ_le_one to identify shifted condProbInfty with a
condExp w.r.t. shifted(negPastSigma).
InformationTheory.Shannon.TwoSided.condExp_comp_measurePreserving
source{Ω₁ : Type u_3}
{Ω₂ : Type u_4}
[m₁ : MeasurableSpace Ω₁]
[m₂ : MeasurableSpace Ω₂]
{μ₁ : MeasureTheory.Measure Ω₁}
{μ₂ : MeasureTheory.Measure Ω₂}
[MeasureTheory.IsFiniteMeasure μ₁]
[MeasureTheory.IsFiniteMeasure μ₂]
{T : Ω₁ → Ω₂}
(h_mp : MeasureTheory.MeasurePreserving T μ₁ μ₂)
{f : Ω₂ → ℝ}
(hf : MeasureTheory.Integrable f μ₂)
(n : MeasurableSpace Ω₂)
(hn : n ≤ m₂)
: