Joint pull-back of conditional entropy (issue #13, lemma B4)

This file proves the joint change of variables for conditional entropy: for a measure-preserving map S (in the application S = T^[n]), pulling back BOTH the partition P AND the conditioning σ-algebra 𝒜 by the same map leaves the conditional entropy unchanged:

H(S⁻¹P | S⁻¹𝒜) = H(P | 𝒜),

where S⁻¹𝒜 is the comap σ-algebra MeasurableSpace.comap S 𝒜.

This is distinct from condEntropy_pullback (Oseledets.Entropy.CondPullback), which fixes the conditioning σ-algebra 𝒜 and therefore needs the two-sided invariance hypotheses (𝒜/𝒜-measurability of T and the pull-back surjectivity). Here, conditioning on the pulled back σ-algebra comap S 𝒜 makes every hypothesis automatic: a comap S 𝒜-set is literally S ⁻¹' A' for an 𝒜-set A' (MeasurableSpace.measurableSet_comap), and S is automatically comap S 𝒜 / 𝒜-measurable. No two-sided assumption is required.

Main results

• Oseledets.Entropy.condExp_indicator_preimage_comap: conditional-expectation equivariance for the comap σ-algebra, μ⟦S⁻¹B | comap S 𝒜⟧ =ᵐ[μ] (μ⟦B | 𝒜⟧) ∘ S, with NO two-sided hypothesis.
• Oseledets.Entropy.condExpKernel_preimage_comap_toReal_ae_eq: the kernel-level form (κ_{comap S 𝒜}(ω, S⁻¹B)).toReal =ᵐ[μ] (κ_𝒜(S ω, B)).toReal.
• Oseledets.Entropy.condEntropy_comap_preimage: the single-map joint pull-back H(S⁻¹P | comap S 𝒜) = H(P | 𝒜).
• Oseledets.Entropy.condEntropy_comap_pullback: the iterated form for S = T^[n].

References

• François Le Maître, Notes on the Kolmogorov–Sinai theorem (2017), §1.

theorem Oseledets.Entropy.condExp_indicator_preimage_comap {α : Type u_1} {𝒜 : MeasurableSpace α} [mα : MeasurableSpace α] {T : α → α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (hm : 𝒜 ≤ mα) (hS : MeasureTheory.MeasurePreserving T μ μ) {B : Set α} (hB : MeasurableSet B) : μ[(T ⁻¹' B).indicator fun (ω : α) => 1 | MeasurableSpace.comap T 𝒜] =ᵐ[μ] fun (ω : α) => μ[B.indicator fun (ω : α) => 1 | 𝒜] (T ω)

(★) Conditional-expectation equivariance for the comap σ-algebra. For a measure-preserving S : α → α, a sub-σ-algebra 𝒜 ≤ mα, and a measurable set B,

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

Unlike condExp_indicator_preimage_comp, this needs NO two-sided invariance hypothesis: a comap S 𝒜-set is literally S ⁻¹' A' for an 𝒜-set A' (MeasurableSpace.measurableSet_comap), so the set-integral identity that characterises the conditional expectation holds by the measure-preserving change of variables alone. The candidate g := (μ⟦B | 𝒜⟧) ∘ S is comap S 𝒜-strongly-measurable because S is automatically comap S 𝒜 / 𝒜-measurable.

theorem Oseledets.Entropy.condExpKernel_preimage_comap_toReal_ae_eq {α : Type u_1} {𝒜 : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] {T : α → α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (hm : 𝒜 ≤ mα) (hS : MeasureTheory.MeasurePreserving T μ μ) {B : Set α} (hB : MeasurableSet B) : (fun (ω : α) => (((ProbabilityTheory.condExpKernel μ (MeasurableSpace.comap T 𝒜)) ω) (T ⁻¹' B)).toReal) =ᵐ[μ] fun (ω : α) => (((ProbabilityTheory.condExpKernel μ 𝒜) (T ω)) B).toReal

Kernel equivariance for the comap σ-algebra. For a measure-preserving S : α → α, a sub-σ-algebra 𝒜 ≤ mα, and a measurable set B,

(κ_{comap S 𝒜}(ω, S⁻¹B)).toReal  =ᵐ[μ]  (κ_𝒜(S ω, B)).toReal,

where κ_𝒜 = condExpKernel μ 𝒜. The proof bridges each kernel to a conditional expectation via condExpKernel_ae_eq_condExp, applies the comap equivariance condExp_indicator_preimage_comap, and transports the B-side identity through the measure-preserving change of variables with Measure.QuasiMeasurePreserving.ae_eq_comp.

theorem Oseledets.Entropy.condEntropy_comap_preimage {α : Type u_1} {ι : Type u_2} {𝒜 : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] {T : α → α} [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (hm : 𝒜 ≤ mα) (hS : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) : (condEntropy μ (MeasurableSpace.comap T 𝒜) fun (i : ι) => T ⁻¹' P.cells i) = condEntropy μ 𝒜 P.cells

Joint pull-back of conditional entropy (single map). For a measure-preserving S : α → α and a sub-σ-algebra 𝒜 ≤ mα, pulling back BOTH the finite partition P and the conditioning σ-algebra 𝒜 by the same map S leaves the conditional entropy unchanged:

H(S⁻¹P | comap S 𝒜) = H(P | 𝒜).

The condEntropy integrand at (S⁻¹P, comap S 𝒜) is, by the comap kernel equivariance condExpKernel_preimage_comap_toReal_ae_eq applied to each cell, μ-a.e. equal to the integrand at (P, 𝒜) precomposed with S; the measure-preserving change of variables integral_comp_self then leaves the integral unchanged. No two-sided invariance hypothesis is needed.

theorem Oseledets.Entropy.condEntropy_comap_pullback {α : Type u_1} {ι : Type u_2} {𝒜 : MeasurableSpace α} [mα : MeasurableSpace α] [StandardBorelSpace α] {T : α → α} [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (hm : 𝒜 ≤ mα) (hT : MeasureTheory.MeasurePreserving T μ μ) (n : ℕ) (P : MeasurePartition μ ι) : (condEntropy μ (MeasurableSpace.comap T^[n] 𝒜) fun (i : ι) => T^[n] ⁻¹' P.cells i) = condEntropy μ 𝒜 P.cells

Joint pull-back of conditional entropy (iterated form). For a measure-preserving T : α → α, a sub-σ-algebra 𝒜 ≤ mα, and n : ℕ, pulling back BOTH the finite partition P and the conditioning σ-algebra 𝒜 by T^[n] leaves the conditional entropy unchanged:

H(T⁻ⁿP | comap (T^[n]) 𝒜) = H(P | 𝒜).

This is condEntropy_comap_preimage applied to the measure-preserving iterate T^[n] (MeasurePreserving.iterate). Unlike condEntropy_pullback_iterate, no two-sided invariance hypothesis (𝒜/𝒜-measurability or pull-back surjectivity of T) is required, because the conditioning σ-algebra is itself pulled back along T^[n].