(★) Conditional-expectation equivariance under a measure-preserving map (TWO-SIDED)

This scratch module settles the architectural crux of GitHub issue #13.

For a measure-preserving T : Ω → Ω and a sub-σ-algebra 𝒜, the conditional-expectation equivariance

μ⟦T⁻¹' B | 𝒜⟧  =ᵐ[μ]  (μ⟦B | 𝒜⟧) ∘ T          (★)

holds under the TWO-SIDED invariance hypothesis T⁻¹𝒜 =ᵐ[μ] 𝒜, encoded here as: every 𝒜-set A is μ-a.e. equal to T⁻¹' A' for some 𝒜-set A' (the "pull-back surjectivity" direction), together with T being 𝒜/𝒜-measurable (the easy one-sided direction comap T 𝒜 ≤ 𝒜, giving g := μ⟦B|𝒜⟧ ∘ T its 𝒜-measurability).

Here μ⟦s | m⟧ is Mathlib's condExp m μ (Set.indicator s (fun _ ↦ (1 : ℝ))).

This is the correct M2 lemma. The one-sided hypothesis comap T 𝒜 ≤ 𝒜 alone is NOT enough: for a genuine NON-invertible factor map there is an explicit Markov counterexample where (★) — and even condEntropy_pullback itself — fails (see the report accompanying this module).

The proof is the uniqueness characterisation ae_eq_condExp_of_forall_setIntegral_eq: we exhibit g := μ⟦B|𝒜⟧ ∘ T as a candidate for μ⟦T⁻¹'B | 𝒜⟧ and check the three hypotheses, the last of which (the set-integral identity over all A ∈ 𝒜) is exactly where two-sided invariance is used.

theorem Oseledets.Entropy.measurableSet_preimage_of_measurePreserving {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {T : Ω → Ω} (hT : MeasureTheory.MeasurePreserving T μ μ) {B : Set Ω} (hB : MeasurableSet B) : MeasurableSet (T ⁻¹' B)

T⁻¹' B is measurable when T is measure-preserving and B is measurable.

theorem Oseledets.Entropy.integrable_comp_self {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {T : Ω → Ω} (hT : MeasureTheory.MeasurePreserving T μ μ) {f : Ω → ℝ} (hf : MeasureTheory.Integrable f μ) : MeasureTheory.Integrable (fun (ω : Ω) => f (T ω)) μ

Integrability is preserved under precomposition with a measure-preserving self-map.

theorem Oseledets.Entropy.integral_comp_self {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {T : Ω → Ω} (hT : MeasureTheory.MeasurePreserving T μ μ) {f : Ω → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) : ∫ (ω : Ω), f (T ω) ∂μ = ∫ (ω : Ω), f ω ∂μ

Change of variables for a measure-preserving self-map: ∫ f(T ω) dμ = ∫ f dμ.

theorem Oseledets.Entropy.setIntegral_comp_preimage {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {T : Ω → Ω} (hT : MeasureTheory.MeasurePreserving T μ μ) {f : Ω → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f μ) {A' : Set Ω} (hA' : MeasurableSet A') : ∫ (ω : Ω) in T ⁻¹' A', f (T ω) ∂μ = ∫ (ω : Ω) in A', f ω ∂μ

The change-of-variables building block on T-preimages of measurable sets: ∫_{T⁻¹A'} f(T ω) dμ = ∫_{A'} f dμ.

theorem Oseledets.Entropy.condExp_indicator_preimage_comp {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {𝒜 : MeasurableSpace Ω} {T : Ω → Ω} [MeasureTheory.IsProbabilityMeasure μ] (hm : 𝒜 ≤ mΩ) (hT : MeasureTheory.MeasurePreserving T μ μ) (hTA : Measurable T) (hpull : ∀ (A : Set Ω), MeasurableSet A → ∃ (A' : Set Ω), MeasurableSet A' ∧ A =ᵐ[μ] T ⁻¹' A') {B : Set Ω} (hB : MeasurableSet B) : μ[(T ⁻¹' B).indicator fun (ω : Ω) => 1 | 𝒜] =ᵐ[μ] fun (ω : Ω) => μ[B.indicator fun (ω : Ω) => 1 | 𝒜] (T ω)

(★) conditional-expectation equivariance under a measure-preserving map, two-sided.

If T is μ-preserving, 𝒜 ≤ mΩ, T is 𝒜/𝒜-measurable (one-sided comap T 𝒜 ≤ 𝒜), and every 𝒜-set is μ-a.e. a T-preimage of an 𝒜-set (the surjective/two-sided direction T⁻¹𝒜 =ᵐ 𝒜), then for every measurable B

μ⟦T⁻¹' B | 𝒜⟧  =ᵐ[μ]  (μ⟦B | 𝒜⟧) ∘ T.