Frozen-factor product entropy: the rectangle partition

For a measure-preserving system (X, T, μ) and a probability space (Y, ν), consider the frozen product transformation T × id on (X × Y, μ ⊗ ν). Given finite measurable partitions ξ of X and η of Y, the rectangle partition (fst⁻¹ ξ) ∨ (snd⁻¹ η) of X × Y has cells ξᵢ × ηⱼ. This file proves that the Kolmogorov–Sinai entropy of this rectangle partition relative to T × id equals the base entropy of ξ relative to T:

h((fst⁻¹ ξ) ∨ (snd⁻¹ η), T × id) = h(ξ, T) (ksEntropyPartition_rectangle_eq).

This is one component of the product-entropy upper bound h(T × id) ≤ h(T) (Walters, An Introduction to Ergodic Theory, Theorem 4.23).

The proof is a sandwich. The projection fst : (X × Y, T × id) → (X, T) is a factor map, so the factor-relative invariance factor_relative_eq gives h(fst⁻¹ ξ, T × id) = h(ξ, T). Likewise snd : (X × Y, T × id) → (Y, id) is a factor map, so h(snd⁻¹ η, T × id) = h(η, id), and the identity map has zero partition entropy (ksEntropyPartition_id_eq_zero). Refinement monotonicity ksEntropyPartition_le_join and join subadditivity ksEntropyPartition_join_le then squeeze: h(fst⁻¹ ξ) ≤ h(rect) ≤ h(fst⁻¹ ξ) + h(snd⁻¹ η) = h(ξ, T) + 0.

Main results

• Oseledets.Entropy.ksEntropySeq_id_of_pos: for n ≥ 1, the n-fold iterated-join entropy under the identity map equals the static entropy H(η).
• Oseledets.Entropy.ksEntropyPartition_id_eq_zero: the identity map has zero partition entropy.
• Oseledets.Entropy.ksEntropyPartition_rectangle_eq: the frozen-factor rectangle entropy equals the base entropy.

References

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

theorem Oseledets.Entropy.ksEntropySeq_id_of_pos {Y : Type u_1} {κ : Type u_2} [MeasurableSpace Y] [Fintype κ] {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure ν] (η : MeasurePartition ν κ) {n : ℕ} (hn : 1 ≤ n) : ksEntropySeq ⋯ η n = entropy ν η.cells

Identity-map iterated-join entropy. For n ≥ 1, the n-fold iterated-join entropy of a partition η under the identity transformation equals the static Shannon entropy H(η).

Under the identity, Tᵏ = id, so the cell of the iterated join at f : Fin n → κ collapses to ⋂ₖ η_{f k}. For a non-constant f two coordinates pick almost-everywhere disjoint cells, so the intersection is null and contributes 0; for a constant f ≡ j (with n ≥ 1) the intersection is η_j. Summing over the constant indices recovers H(η).

theorem Oseledets.Entropy.ksEntropyPartition_id_eq_zero {Y : Type u_1} {κ : Type u_2} [MeasurableSpace Y] [Fintype κ] {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure ν] (η : MeasurePartition ν κ) : ksEntropyPartition ⋯ η = 0

The identity map has zero partition entropy. The iterated-join entropy sequence is eventually the constant H(η) (ksEntropySeq_id_of_pos), so dividing by n and passing to the Fekete limit gives 0.

theorem Oseledets.Entropy.ksEntropyPartition_rectangle_eq {Y : Type u_1} {κ : Type u_2} [MeasurableSpace Y] [Fintype κ] {X : Type u_3} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν] {T : X → X} (hT : MeasureTheory.MeasurePreserving T μ μ) {ι : Type u_4} [Fintype ι] (ξ : MeasurePartition μ ι) (η : MeasurePartition ν κ) : ksEntropyPartition ⋯ (joinPartition (MeasurePartition.pulledBack ⋯ ξ) (MeasurePartition.pulledBack ⋯ η)) = ksEntropyPartition hT ξ

Frozen-factor rectangle entropy. Let (X, T, μ) be a measure-preserving system and (Y, ν) a probability space. For finite measurable partitions ξ of X and η of Y, the Kolmogorov–Sinai entropy of the rectangle partition (fst⁻¹ ξ) ∨ (snd⁻¹ η) relative to the frozen product T × id equals the base entropy of ξ relative to T: h((fst⁻¹ ξ) ∨ (snd⁻¹ η), T × id) = h(ξ, T).

The two projections fst and snd are factor maps of the frozen system, so by factor_relative_eq the pulled-back partitions have entropies h(ξ, T) and h(η, id) = 0 (ksEntropyPartition_id_eq_zero); refinement monotonicity and join subadditivity then sandwich the rectangle entropy between h(ξ, T) and h(ξ, T) + 0.