Pullback partitions

This file provides the pullback partition T⁻¹ β of a finite measurable partition β along a measure-preserving transformation T, and the T-invariance of its Shannon entropy. These feed the dynamical refinement ⋁ₖ₌₀ⁿ⁻¹ T⁻ᵏ α and the Fekete limit h(α, T), which are built in Oseledets.Entropy.KSEntropy (using the flat Fin n-indexed iterated join ksJoin).

It continues the measure-theoretic foundation for Kolmogorov–Sinai entropy started in Oseledets.Entropy.Partition, Oseledets.Entropy.Join, Oseledets.Entropy.Subadditive, and Oseledets.Entropy.Subadditive2.

Main definitions

• Oseledets.Entropy.MeasurePartition.pullback: the partition T⁻¹ β whose cells are the preimages T⁻¹ Bⱼ, for a measure-preserving T.

Main results

• Oseledets.Entropy.entropy_pullback: the pullback partition has the same entropy as the original, H(T⁻¹ β) = H(β) (the T-invariance of partition entropy).

References

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

noncomputable def Oseledets.Entropy.MeasurePartition.pullback {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) : MeasurePartition μ ι

The pullback partition T⁻¹ β of a finite measurable partition β = P along a measure-preserving transformation T : α → α: the partition whose cell at index i is the preimage T⁻¹ (P.cells i). Each cell is measurable (preimage of a measurable set under the measurable T); the family is pairwise almost-everywhere disjoint (the preimage of an a.e.-disjoint pair is a.e. disjoint, since T preserves measures); and the cells cover the space (the preimage of the cover ⋃ i, P.cells i = univ is univ).

Equations

• Oseledets.Entropy.MeasurePartition.pullback hT P = { cells := fun (i : ι) => T ⁻¹' P.cells i, measurable := ⋯, aedisjoint := ⋯, cover := ⋯ }

@[simp]

theorem Oseledets.Entropy.MeasurePartition.pullback_cells {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) : (pullback hT P).cells = fun (i : ι) => T ⁻¹' P.cells i

theorem Oseledets.Entropy.entropy_pullback {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (P : MeasurePartition μ ι) : entropy μ (MeasurePartition.pullback hT P).cells = entropy μ P.cells

T-invariance of partition entropy. The pullback partition T⁻¹ β along a measure-preserving T has the same Shannon entropy as β, since T preserves the measure of each cell. This is entropy_comp_preimage specialized to the cells of a partition.