The Kolmogorov–Sinai generator theorem h(T) = h(T, P)

This file proves the Kolmogorov–Sinai generator theorem: for a measure-preserving transformation T of a standard Borel probability space and a one-sided generating finite partition P (IsGenerating μ T P, i.e. the forward-T-saturated σ-algebra generated by P is the ambient σ-algebra mα), the entropy of the system is already attained on P: h(T) = h(T, P).

The classical statement is Oseledets.Entropy.Generator left as a hypothesis-form interface; here it is proved by assembling the issue-#13 unconditional Abramov–Rokhlin machinery.

Proof outline (Route A)

le_antisymm of two inequalities:

• h(T, P) ≤ h(T) is free (le_ksEntropy).

• h(T) ≤ h(T, P). Since ksEntropy hT = ⨆ over finite partitions, by iSup_le it reduces to the crux ∀ m (Q : MeasurePartition μ (Fin m)), h(T, Q) ≤ h(T, P). For the crux, apply the unconditional Abramov–Rokhlin partition identity abramovRokhlin_partition to the refined partition R := joinPartition Q P over the factor P, conditioning on the full σ-algebra mα. Three ingredients:

  1. condEntropy_full_eq_zero: the conditional Shannon entropy against mα of any measurable partition vanishes (a measurable function is its own conditional expectation w.r.t. the full σ-algebra, so each kernel cell mass is 0 or 1 a.e. and negMulLog of {0, 1} is 0).
  2. The saturation witness from hgen : IsGenerating μ T P (via iSup_generatedSigmaAlgebra_ksJoin_eq): ⨆ n σ(P-join) = mα. This is load-bearing — the moving-index limit underlying abramovRokhlin_partition is false without saturation.
  3. The structural refinement witness: each cell of the (Q ∨ P)-join lies (exactly, hence a.e.) inside a single P-join cell, via the second-coordinate projection.

  Combining (1)–(3): h(R, T) = h(P, T) + h(R, T | mα) = h(P, T) + 0, while ksEntropyPartition_le_join gives h(Q, T) ≤ h(R, T) = h(Q ∨ P, T). Hence h(Q, T) ≤ h(P, T).

Main results

• Oseledets.Entropy.condEntropy_full_eq_zero: H(R | mα) = 0 for the full σ-algebra (N6.1).
• Oseledets.Entropy.ksEntropyPartition_le_of_generating: the crux — h(T, Q) ≤ h(T, P) for a generating P and any finite partition Q.
• Oseledets.Entropy.ksEntropy_eq_ksEntropyPartition_of_generating: the headline generator theorem h(T) = h(T, P).

References

• François Le Maître, Notes on the Kolmogorov–Sinai theorem (2017), §2.
• Peter Walters, An Introduction to Ergodic Theory, GTM 79, Springer (1982), Ch. 4.

theorem Oseledets.Entropy.condEntropy_full_eq_zero {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [StandardBorelSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (R : MeasurePartition μ ι) : condEntropy μ mα R.cells = 0

N6.1 — the conditional Shannon entropy against the full σ-algebra vanishes. condEntropy μ mα R.cells = 0 for any finite measurable partition R.

A measurable function is its own conditional expectation with respect to the full σ-algebra mα (condExp_of_stronglyMeasurable with hm = le_rfl). Hence for each cell the regular-conditional kernel mass (condExpKernel μ mα ω).real (R.cells i) equals the indicator 𝟙_{R.cells i} ω μ-a.e. (condExpKernel_ae_eq_condExp), which is 0 or 1; the Shannon term negMulLog is then negMulLog 0 = 0 or negMulLog 1 = 0. The whole integrand vanishes μ-a.e., so the integral is 0.

theorem Oseledets.Entropy.ksJoin_joinPartition_subset {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [Fintype ι] {κ : Type u_3} [Fintype κ] {μ : MeasureTheory.Measure α} {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) (Q : MeasurePartition μ κ) (P : MeasurePartition μ ι) (n : ℕ) (f : Fin n → κ × ι) : (ksJoin hT (joinPartition Q P) n).cells f ⊆ (ksJoin hT P n).cells fun (k : Fin n) => (f k).2

Structural refinement of the (Q ∨ P)-join over the P-join. Each cell of the n-fold join of joinPartition Q P is contained in the n-fold join cell of P indexed by the second-coordinate projection: with g n f := fun k => (f k).2, (ksJoin hT (joinPartition Q P) n).cells f ⊆ (ksJoin hT P n).cells (g n f).

Each (Q ∨ P)-join cell is ⋂ₖ T⁻ᵏ(Q_{(f k).1} ∩ P_{(f k).2}), contained in ⋂ₖ T⁻ᵏ(P_{(f k).2}), the P-join cell at k ↦ (f k).2.

theorem Oseledets.Entropy.MeasurePartition.index_nonempty {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (R : MeasurePartition μ ι) : Nonempty ι

The index of a partition of a probability space is nonempty. A probability space is nonempty (nonempty_of_isProbabilityMeasure), so the cover ⋃ i, R.cells i = univ is a nonempty set; an empty index type would force the union to be empty, a contradiction.

theorem Oseledets.Entropy.ksEntropyPartition_le_of_generating {α : Type u_1} [mα : MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) {n : ℕ} (P : MeasurePartition μ (Fin n)) (hgen : IsGenerating μ T P) {m : ℕ} (Q : MeasurePartition μ (Fin m)) : ksEntropyPartition hT Q ≤ ksEntropyPartition hT P

N6.2 — the crux of the generator theorem. For a generating partition P and any finite partition Q, the partition-relative entropy of Q is dominated by that of P: h(T, Q) ≤ h(T, P).

Work with the join R := joinPartition Q P. Monotonicity under refinement gives h(Q, T) ≤ h(R, T) (ksEntropyPartition_le_join). The unconditional Abramov–Rokhlin partition identity abramovRokhlin_partition, applied with the refined partition R over the factor P and conditioning on the full σ-algebra mα, splits h(R, T) = h(P, T) + h(R, T | mα). The saturation witness ⨆ n σ(P-join) = mα is supplied by hgen (via iSup_generatedSigmaAlgebra_ksJoin_eq), the refinement witness by ksJoin_joinPartition_subset, and the relative term h(R, T | mα) ≤ H(R | mα) = 0 by condEntropy_full_eq_zero. Hence h(R, T) = h(P, T), so h(Q, T) ≤ h(P, T).

theorem Oseledets.Entropy.ksEntropy_eq_ksEntropyPartition_of_generating {α : Type u_1} [mα : MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) {n : ℕ} (P : MeasurePartition μ (Fin n)) (hgen : IsGenerating μ T P) : ksEntropy hT = ↑(ksEntropyPartition hT P)

The Kolmogorov–Sinai generator theorem (issue-#13 capstone): for a one-sided generating finite partition P of a standard Borel probability space, the Kolmogorov–Sinai entropy of the system equals the partition-relative entropy of P: h(T) = h(T, P).

le_antisymm of the free bound h(T, P) ≤ h(T) (le_ksEntropy) and the reverse h(T) ≤ h(T, P). The latter unfolds the supremum defining ksEntropy and reduces by iSup_le to the crux ksEntropyPartition_le_of_generating, coerced to EReal. No ergodicity is needed; the StandardBorelSpace and IsProbabilityMeasure instances are load-bearing (kernel disintegration), and the saturation supplied by hgen is what makes the moving-index Abramov–Rokhlin limit valid.