Monotonicity of the Kolmogorov–Sinai entropy under refinement by a join

For a measure-preserving transformation T and two finite measurable partitions α and β, the join α ∨ β refines α (every α-cell is a union of (α ∨ β)-cells). This file proves that the partition-relative Kolmogorov–Sinai entropy is monotone under this refinement: h(α, T) ≤ h(α ∨ β, T).

This is the entropy-increases-under-refinement half of the variational picture, complementing the subadditivity h(α ∨ β, T) ≤ h(α, T) + h(β, T) (ksEntropyPartition_join_le): together they sandwich the join entropy between max (h(α, T), h(β, T)) and h(α, T) + h(β, T).

The dynamical statement reduces, cell by cell, to a static refinement bound H(α) ≤ H(α ∨ β) (entropy_le_entropy_join). At the scalar level this is the superadditivity of negMulLog over a finite sum: for nonnegative reals x with sum s, negMulLog s ≤ ∑ⱼ negMulLog (x j) (negMulLog_sum_le_sum_negMulLog), because each term obeys x j · log (x j) ≤ x j · log s by monotonicity of log on 0 < x j ≤ s (the x j = 0 terms contribute 0), so ∑ⱼ x j · log (x j) ≤ s · log s; negating gives the claim. Applying it to each α-row of the joint cell measures μ(Aᵢ ∩ Bⱼ), whose β-marginal is μ(Aᵢ) (MeasurePartition.measure_eq_sum_inter), yields H(α) ≤ H(α ∨ β).

The dynamical step then mirrors ksEntropySeq_join_le: reindexing the n-fold join of α ∨ β by Equiv.arrowProdEquivProdArrow exhibits its entropy as the static join entropy of the two n-fold joins (ksJoinCells_joinCells), so the static refinement bound gives the per-n inequality ksEntropySeq α n ≤ ksEntropySeq (α ∨ β) n; dividing by n and passing both Fekete limits (tendsto_ksEntropySeq, le_of_tendsto_of_tendsto') gives the dynamical statement.

Main results

• Oseledets.Entropy.negMulLog_sum_le_sum_negMulLog: negMulLog (∑ⱼ x j) ≤ ∑ⱼ negMulLog (x j) for a nonnegative family.
• Oseledets.Entropy.entropy_le_entropy_join: the static refinement bound H(α) ≤ H(α ∨ β).
• Oseledets.Entropy.ksEntropySeq_le_join: the per-n bound ksEntropySeq α n ≤ ksEntropySeq (α ∨ β) n.
• Oseledets.Entropy.ksEntropyPartition_le_join: h(α, T) ≤ h(α ∨ β, T), monotonicity of the Kolmogorov–Sinai entropy under refinement by a join.

References

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

theorem Oseledets.Entropy.negMulLog_sum_le_sum_negMulLog {ω : Type u_4} [Fintype ω] (x : ω → ℝ) (hx : ∀ (j : ω), 0 ≤ x j) : (∑ j : ω, x j).negMulLog ≤ ∑ j : ω, (x j).negMulLog

Superadditivity of negMulLog over a finite sum. For a nonnegative family x : ω → ℝ with total s = ∑ⱼ x j, the value of negMulLog at the sum is at most the sum of the values: negMulLog (∑ⱼ x j) ≤ ∑ⱼ negMulLog (x j). Equivalently s · log s ≤ ∑ⱼ x j · log (x j): each term obeys x j · log (x j) ≤ x j · log s by monotonicity of log on 0 < x j ≤ s, with the x j = 0 terms contributing 0 on both sides.

theorem Oseledets.Entropy.entropy_le_entropy_join {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [MeasurableSpace α] [Fintype ι] [Fintype κ] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurePartition μ ι) (Q : MeasurePartition μ κ) : entropy μ P.cells ≤ entropy μ (joinCells P.cells Q.cells)

Static refinement bound: entropy increases under joins. For two finite measurable partitions P (= α) and Q (= β) of a probability space, the entropy of the join dominates the entropy of either factor: H(α) ≤ H(α ∨ β).

Each α-cell measure splits along β as μ(Aᵢ) = ∑ⱼ μ(Aᵢ ∩ Bⱼ) (MeasurePartition.measure_eq_sum_inter); the scalar superadditivity negMulLog_sum_le_sum_negMulLog applied to the i-th row of the joint cell measures bounds negMulLog (μ(Aᵢ).toReal) by ∑ⱼ negMulLog (μ(Aᵢ ∩ Bⱼ).toReal), and summing over i (regrouping the product index ι × κ by Fintype.sum_prod_type) gives the claim.

theorem Oseledets.Entropy.ksEntropySeq_le_join {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [MeasurableSpace α] [Fintype ι] [Fintype κ] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) (Q : MeasurePartition μ κ) (n : ℕ) : ksEntropySeq hT P n ≤ ksEntropySeq hT (joinPartition P Q) n

Per-n refinement bound. The n-fold dynamical-join entropy of α is at most that of the join α ∨ β: H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α) ≤ H(⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ(α ∨ β)).

Reindexing the product index Fin n → ι × κ by Equiv.arrowProdEquivProdArrow and using the cell identity ksJoinCells_joinCells, the (α ∨ β)-join entropy equals the static join entropy of the two n-fold joins; the static refinement bound entropy_le_entropy_join then dominates the n-fold join entropy of α.

theorem Oseledets.Entropy.ksEntropyPartition_le_join {α : Type u_1} {ι : Type u_2} {κ : Type u_3} [MeasurableSpace α] [Fintype ι] [Fintype κ] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) (Q : MeasurePartition μ κ) : ksEntropyPartition hT P ≤ ksEntropyPartition hT (joinPartition P Q)

Monotonicity of the Kolmogorov–Sinai entropy under refinement by a join: h(α, T) ≤ h(α ∨ β, T).

The join α ∨ β refines α, so its long-run entropy rate dominates. The per-n bound ksEntropySeq_le_join divided by n reads ksEntropySeq α n / n ≤ ksEntropySeq (α ∨ β) n / n. Each averaged sequence converges to its Kolmogorov–Sinai entropy by tendsto_ksEntropySeq, so passing the pointwise inequality to the two Fekete limits (le_of_tendsto_of_tendsto') gives the claim.