Shannon entropy of a finite measurable partition

This file lays the measure-theoretic foundation for Kolmogorov–Sinai entropy by defining the Shannon entropy of a finite family of measurable cells with respect to a probability measure μ, and proving its two elementary bounds. Following the Le Maître notes on the Kolmogorov–Sinai theorem, the entropy of a partition α = (Aᵢ) is H(α) = - ∑ᵢ μ(Aᵢ) log μ(Aᵢ) = ∑ᵢ negMulLog (μ Aᵢ).toReal, the average information gained by learning which cell a μ-random point lies in.

The entropy is defined on loose data — a Fintype-indexed family of sets — so that it can be reused both for a genuine partition and for intermediate non-partition families. The companion MeasurePartition structure bundles the partition hypotheses (almost-everywhere disjoint cells covering the space) for later use.

Main definitions

• Oseledets.Entropy.entropy: the Shannon entropy ∑ i, negMulLog (μ (s i)).toReal of a finite family of cells s : ι → Set α.
• Oseledets.Entropy.MeasurePartition: a finite measurable partition of a measure space, i.e. a family of measurable, almost-everywhere disjoint cells covering the whole space.

Main results

• Oseledets.Entropy.entropy_nonneg: entropy is nonnegative for a probability measure.
• Oseledets.Entropy.entropy_le_log_card: a partition into k cells has entropy at most log k (Proposition 1 of the notes), proved by Jensen's inequality for the concave function negMulLog.

References

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

noncomputable def Oseledets.Entropy.entropy {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] (μ : MeasureTheory.Measure α) (s : ι → Set α) : ℝ

The Shannon entropy ∑ i, negMulLog (μ (s i)).toReal of a finite family of cells s : ι → Set α with respect to a measure μ. For a genuine partition this is - ∑ᵢ μ(sᵢ) log μ(sᵢ), the average information gained by learning which cell a random point lies in.

Equations

• Oseledets.Entropy.entropy μ s = ∑ i : ι, (μ (s i)).toReal.negMulLog

@[simp]

theorem Oseledets.Entropy.entropy_def {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] (μ : MeasureTheory.Measure α) (s : ι → Set α) : entropy μ s = ∑ i : ι, (μ (s i)).toReal.negMulLog

structure Oseledets.Entropy.MeasurePartition {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (ι : Type u_3) [Fintype ι] : Type (max u_1 u_3)

A finite measurable partition of a measure space (α, μ): a Fintype-indexed family of measurable cells that are pairwise almost-everywhere disjoint and cover the whole space.

• cells : ι → Set α

  The cells of the partition.

• measurable (i : ι) : MeasurableSet (self.cells i)

  Each cell is measurable.

• aedisjoint : Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) self.cells)

  The cells are pairwise almost-everywhere disjoint.

• cover : ⋃ (i : ι), self.cells i = Set.univ

  The cells cover the whole space.

noncomputable def Oseledets.Entropy.MeasurePartition.reindex {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {κ : Type u_3} [Fintype ι] [Fintype κ] {μ : MeasureTheory.Measure α} (P : MeasurePartition μ ι) (e : κ ≃ ι) : MeasurePartition μ κ

Reindex a finite measurable partition P along an equivalence e : κ ≃ ι of index types: the new cell at k is the old cell at e k. The cells are measurable, pairwise a.e. disjoint and cover the space because e is a bijection, so this is again a partition.

Equations

• P.reindex e = { cells := fun (k : κ) => P.cells (e k), measurable := ⋯, aedisjoint := ⋯, cover := ⋯ }

@[simp]

theorem Oseledets.Entropy.MeasurePartition.reindex_cells {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {κ : Type u_3} [Fintype ι] [Fintype κ] {μ : MeasureTheory.Measure α} (P : MeasurePartition μ ι) (e : κ ≃ ι) : (P.reindex e).cells = fun (k : κ) => P.cells (e k)

theorem Oseledets.Entropy.entropy_nonneg {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (s : ι → Set α) : 0 ≤ entropy μ s

Shannon entropy of a finite family of cells is nonnegative for a probability measure, since each cell has measure in [0, 1] and negMulLog is nonnegative there.

theorem Oseledets.Entropy.entropy_le_log_card {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] [Nonempty ι] (μ : MeasureTheory.Measure α) (s : ι → Set α) (hsum : ∑ i : ι, (μ (s i)).toReal = 1) : entropy μ s ≤ Real.log ↑(Fintype.card ι)

Proposition 1 (Le Maître). A finite family of k cells whose μ-measures sum to 1 (in particular, a partition of a probability space) has Shannon entropy at most log k.

This is Jensen's inequality applied to the concave function negMulLog with equal weights 1 / k: writing pᵢ = (μ (s i)).toReal, k⁻¹ * H = ∑ᵢ k⁻¹ • negMulLog pᵢ ≤ negMulLog (∑ᵢ k⁻¹ • pᵢ) = negMulLog k⁻¹ = k⁻¹ * log k.