The base entropy is below the entropy of the product with an identity factor

For a measure-preserving system (X, T, μ) and a probability space (Y, ν), the product transformation T × id on (X × Y, μ ⊗ ν) has the base system (X, T, μ) as a factor, via the first projection fst : X × Y → X. Since a factor's Kolmogorov–Sinai entropy never exceeds that of the total system, this gives the free inequality

h(T) ≤ h(T × id) (Oseledets.Entropy.ksEntropy_le_prod).

This is the easy half of Walters' product-entropy theorem (Walters, An Introduction to Ergodic Theory, Theorem 4.23). Combined with the reverse bound h(T × id) ≤ h(T) it yields the equality h(T × id) = h(T).

The proof pulls each finite partition R of the base back along the factor map fst. By the factor-relative entropy invariance (Oseledets.Entropy.factor_relative_eq) the partition-relative entropy h(R, T) equals h(fst⁻¹ R, T × id), and the latter is bounded above by the entropy of the product system (Oseledets.Entropy.le_ksEntropy). Taking the supremum over all base partitions R gives h(T) ≤ h(T × id).

Main results

• Oseledets.Entropy.ksEntropy_le_prod: h(T) ≤ h(T × id).

References

• Peter Walters, An Introduction to Ergodic Theory, GTM 79, Springer (1982), Theorem 4.23.

theorem Oseledets.Entropy.ksEntropy_le_prod {X : Type u_1} {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) : ksEntropy hT ≤ ksEntropy ⋯

The base entropy is below the entropy of the product with an identity factor: h(T) ≤ h(T × id).

For a measure-preserving system (X, T, μ) and a probability space (Y, ν), the first projection fst : X × Y → X is a factor map from the product system (X × Y, T × id, μ ⊗ ν) onto the base (X, T, μ) (it intertwines the dynamics, fst ∘ (T × id) = T ∘ fst, and is measure-preserving by measurePreserving_fst). Each finite measurable partition R of the base pulls back to a partition fst⁻¹ R of the product whose relative entropy agrees with that of R by the factor-relative invariance factor_relative_eq; that pulled-back relative entropy is in turn ≤ h(T × id) by le_ksEntropy. Taking the supremum over all base partitions gives the claim.

This is the free ≥-direction of Walters' product-entropy theorem (Theorem 4.23).