Partition-relative entropy of a uniform-join system

This is the abstract, system-independent half of the Rokhlin-equality computation for the doubling map. It isolates the only fact about the dynamics that is needed: if, for a measure-preserving transformation T and a finite partition α indexed by a type ι of cardinality b, every cell of the n-fold join ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α has the same measure b⁻ⁿ, then the iterated-join entropy is exactly n · log b and the partition-relative Kolmogorov–Sinai entropy is h(α, T) = log b.

For the doubling map with the binary partition (b = 2) this gives h(α, T) = log 2, the concrete realization of Pesin's equality on a real expanding system; the dynamical input — that the n-fold join cells are the 2ⁿ dyadic arcs of length 2⁻ⁿ — is supplied in Oseledets.Examples.Rokhlin.DoublingCrux.

Main results

• Oseledets.Examples.Rokhlin.entropy_uniform_join: if every join cell has measure b⁻ⁿ and there are bⁿ of them, then ksEntropySeq hT P n = n · Real.log b.
• Oseledets.Examples.Rokhlin.ksEntropyPartition_of_uniform: under the same uniform-measure hypothesis for every n, ksEntropyPartition hT P = Real.log b.

References

• François Le Maître, Notes on the Kolmogorov–Sinai theorem (2017), §1.
• V. A. Rokhlin, Lectures on the entropy theory of measure-preserving transformations (1967).

theorem Oseledets.Examples.Rokhlin.entropy_uniform_join {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] [Nonempty ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : Entropy.MeasurePartition μ ι) (n : ℕ) (huniform : ∀ (f : Fin n → ι), μ ((Entropy.ksJoin hT P n).cells f) = (↑(Fintype.card ι) ^ n)⁻¹) : Entropy.ksEntropySeq hT P n = ↑n * Real.log ↑(Fintype.card ι)

Exact iterated-join entropy of a uniform join. Suppose every cell of the n-fold join ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α has the same measure (b ^ n)⁻¹, where b = Fintype.card ι ≥ 1. Since the join is indexed by Fin n → ι, a type of cardinality b ^ n, the entropy is a sum of b ^ n equal terms negMulLog (b ^ n)⁻¹ = (b ^ n)⁻¹ · n · log b, totalling n · log b.

theorem Oseledets.Examples.Rokhlin.ksEntropyPartition_of_uniform {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] [Nonempty ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : Entropy.MeasurePartition μ ι) (huniform : ∀ (n : ℕ) (f : Fin n → ι), μ ((Entropy.ksJoin hT P n).cells f) = (↑(Fintype.card ι) ^ n)⁻¹) : Entropy.ksEntropyPartition hT P = Real.log ↑(Fintype.card ι)

Partition-relative Kolmogorov–Sinai entropy of a uniform-join system. If for every n the n-fold join ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α has all its cells of equal measure (Fintype.card ι ^ n)⁻¹, then the partition-relative entropy is h(α, T) = Real.log (Fintype.card ι). The averaged entropy sequence ksEntropySeq n / n is the constant log b for n ≥ 1 (entropy_uniform_join), hence tends to log b; but it also tends to ksEntropyPartition (tendsto_ksEntropySeq), so the two limits agree.