Cell-measure sum and joins of finite measurable partitions

This file continues the measure-theoretic foundation for Kolmogorov–Sinai entropy started in Oseledets.Entropy.Partition. It records that the cells of a MeasurePartition of a probability space have μ-measures summing to 1, and introduces the cell family joinCells s t of the join (common refinement) α ∨ β of two partitions, whose cells are the intersections Aᵢ ∩ Bⱼ.

Following the Le Maître notes on the Kolmogorov–Sinai theorem, the join keeps all index pairs (i, j) and allows null cells, so it is indexed by ι × κ.

Main definitions

• Oseledets.Entropy.joinCells: the family (i, j) ↦ s i ∩ t j of intersection cells of two families.

Main results

• Oseledets.Entropy.MeasurePartition.sum_toReal_measure_eq_one: the cell measures of a partition of a probability space sum to 1.
• Oseledets.Entropy.entropy_le_log_card_partition: a partition into k cells has entropy at most log k.

References

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

theorem Oseledets.Entropy.MeasurePartition.sum_toReal_measure_eq_one {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurePartition μ ι) : ∑ i : ι, (μ (P.cells i)).toReal = 1

The μ-measures of the cells of a finite measurable partition of a probability space sum to the total mass 1. The cells are measurable, pairwise almost-everywhere disjoint, and cover the whole space, so finite additivity of μ over an a.e.-disjoint null-measurable family gives ∑ i, μ (cells i) = μ univ = 1.

theorem Oseledets.Entropy.entropy_le_log_card_partition {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] [Nonempty ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurePartition μ ι) : entropy μ P.cells ≤ Real.log ↑(Fintype.card ι)

Corollary of Proposition 1 (Le Maître). A finite measurable partition of a probability space into k cells has Shannon entropy at most log k.

def Oseledets.Entropy.joinCells {α : Type u_1} {ι : Type u_2} {κ : Type u_3} (s : ι → Set α) (t : κ → Set α) : ι × κ → Set α

The cell family (i, j) ↦ s i ∩ t j underlying the join (common refinement) α ∨ β of two families of cells s : ι → Set α and t : κ → Set α.

Equations

• Oseledets.Entropy.joinCells s t p = s p.1 ∩ t p.2

@[simp]

theorem Oseledets.Entropy.joinCells_apply {α : Type u_1} {ι : Type u_2} {κ : Type u_3} (s : ι → Set α) (t : κ → Set α) (p : ι × κ) : joinCells s t p = s p.1 ∩ t p.2