Generating partitions and the supplied-generator entropy interface

A finite measurable partition P of a measure-preserving system (α, T, μ) is a generator (or generating partition) when the dynamics, refined under the forward iterates of T, recovers the whole measurable structure: the smallest T-pullback-stable σ-algebra containing the σ-algebra σ(P) generated by the cells of P is the ambient σ-algebra mα.

The classical Kolmogorov–Sinai theorem then asserts the entropy reduction h(T) = h(P, T) for any generator P: the supremum defining the entropy of the system is already attained on a single generating partition. Proving that theorem is a substantial undertaking; this file deliberately does not prove it. Following the verified design plan for the Abramov–Rokhlin assembly (issue #13), the M6 conditional-entropy layer ships under supplied generator-reduction equalities rather than a generator theorem. Accordingly this file provides:

• the IsGenerating predicate, stated in the honest exact-equality σ-algebra form, together with cheap, true API (σ(P) ≤ the generated σ-algebra, refinement monotonicity);
• a thin hypothesis-form wrapper ksEntropy_eq_ksEntropyPartition_of_reduction that names and exposes the generator-reduction equality h(T) = h(P, T) in exactly the shape the Abramov–Rokhlin assembly consumes, and a bundling structure IsGeneratingWithReduction carrying a generator together with its (supplied) reduction equality.

Design note: which σ-algebra equation?

The generated invariant σ-algebra is taken as ⨆ n, comap (T^[n]) σ(P), the supremum over the forward iterates T^[n] of the pulled-back generating σ-algebra σ(P) = generateFrom (range P.cells). This is the standard one-sided generator condition for a (possibly non-invertible) endomorphism: a point's whole μ-essential coordinates are recovered from the observable P and its forward time-translates. The exact equality with mα is clean to state and is the form used by the Kolmogorov–Sinai theorem; a ≤ mα direction always holds (IsGenerating is then the reverse saturation), so the predicate is genuinely a hypothesis, not a triviality.

Main definitions

• Oseledets.Entropy.IsGenerating: P generates the dynamics — the smallest forward-T-invariant σ-algebra containing σ(P) is the ambient σ-algebra.
• Oseledets.Entropy.IsGeneratingWithReduction: a generator bundled with its supplied generator-reduction equality h(T) = h(P, T).

Main results

• Oseledets.Entropy.generateFrom_cells_le_generated: σ(P) ≤ ⨆ n, comap (T^[n]) σ(P), the cheap inclusion of the static generating σ-algebra into the forward-saturated one.
• Oseledets.Entropy.IsGenerating.le: a generating partition's forward-saturated σ-algebra is the ambient σ-algebra (unfolded form).
• Oseledets.Entropy.ksEntropy_eq_ksEntropyPartition_of_reduction: the hypothesis-form wrapper exposing a supplied generator reduction h(T) = h(P, T).

References

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

@[reducible]

def Oseledets.Entropy.generatedSigmaAlgebra {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [Fintype ι] (μ : MeasureTheory.Measure α) (P : MeasurePartition μ ι) : MeasurableSpace α

The σ-algebra σ(P) = generateFrom (range P.cells) generated by the cells of a finite partition P. This is the static observable σ-algebra: the smallest σ-algebra making membership in each cell of P measurable. Marked @[reducible] since its value is a MeasurableSpace (a class type), so it must unfold for instance resolution and definitional rewriting.

Equations

• Oseledets.Entropy.generatedSigmaAlgebra μ P = MeasurableSpace.generateFrom (Set.range P.cells)

theorem Oseledets.Entropy.generatedSigmaAlgebra_reindex {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [Fintype ι] {κ : Type u_3} [Fintype κ] {μ : MeasureTheory.Measure α} (P : MeasurePartition μ ι) (e : κ ≃ ι) : generatedSigmaAlgebra μ (P.reindex e) = generatedSigmaAlgebra μ P

Reindexing leaves the generated σ-algebra unchanged. The cell family is merely permuted, so its range — and hence the σ-algebra it generates — is the same.

def Oseledets.Entropy.IsGenerating {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [Fintype ι] (μ : MeasureTheory.Measure α) (T : α → α) (P : MeasurePartition μ ι) : Prop

P is a generating partition (a generator) for the measure-preserving system (α, T, μ) when the smallest forward-T-pullback-stable σ-algebra containing the generated σ-algebra σ(P) is the ambient measurable structure mα: ⨆ n, comap (T^[n]) σ(P) = mα.

This is the standard one-sided generator condition for a (possibly non-invertible) endomorphism: the whole measurable structure is recovered from the observable P together with its forward time-translates T^[n]. The Kolmogorov–Sinai theorem then gives the entropy reduction h(T) = h(P, T); that theorem is not proved here — this predicate is the hypothesis the supplied-generator entropy interface (issue #13, Abramov–Rokhlin) consumes.

Equations

• Oseledets.Entropy.IsGenerating μ T P = (⨆ (n : ℕ), MeasurableSpace.comap T^[n] (Oseledets.Entropy.generatedSigmaAlgebra μ P) = mα)

theorem Oseledets.Entropy.generateFrom_cells_le_generated {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [Fintype ι] (μ : MeasureTheory.Measure α) (T : α → α) (P : MeasurePartition μ ι) : generatedSigmaAlgebra μ P ≤ ⨆ (n : ℕ), MeasurableSpace.comap T^[n] (generatedSigmaAlgebra μ P)

The static generating σ-algebra σ(P) sits inside the forward-saturated σ-algebra ⨆ n, comap (T^[n]) σ(P): the n = 0 term is comap (T^[0]) σ(P) = comap id σ(P) = σ(P), which is bounded above by the supremum. This is the always-available ≤ half; IsGenerating is the nontrivial reverse saturation up to the full ambient σ-algebra.

theorem Oseledets.Entropy.IsGenerating.le {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} {T : α → α} {P : MeasurePartition μ ι} (h : IsGenerating μ T P) : ⨆ (n : ℕ), MeasurableSpace.comap T^[n] (generatedSigmaAlgebra μ P) = mα

Unfolded form of IsGenerating: a generating partition's forward-saturated σ-algebra equals the ambient measurable structure. This is just the definition, named for convenient consumption by the Abramov–Rokhlin assembly.

theorem Oseledets.Entropy.generated_mono {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} {T : α → α} {P Q : MeasurePartition μ ι} (hPQ : generatedSigmaAlgebra μ P ≤ generatedSigmaAlgebra μ Q) : ⨆ (n : ℕ), MeasurableSpace.comap T^[n] (generatedSigmaAlgebra μ P) ≤ ⨆ (n : ℕ), MeasurableSpace.comap T^[n] (generatedSigmaAlgebra μ Q)

Refinement monotonicity of the generated σ-algebra. If the cells of P all lie in the σ-algebra generated by a finer partition Q (σ(P) ≤ σ(Q)), then Q's forward-saturated σ-algebra contains P's. In particular, if P already generates the dynamics, so does any refinement Q of P. The pullback comap (T^[n]) is monotone in its σ-algebra argument, and iSup is monotone, so the saturation is monotone in σ(·).

theorem Oseledets.Entropy.IsGenerating.mono_refine {α : Type u_1} {ι : Type u_2} [mα : MeasurableSpace α] [Fintype ι] {μ : MeasureTheory.Measure α} {T : α → α} (hT : Measurable T) {P Q : MeasurePartition μ ι} (hPQ : generatedSigmaAlgebra μ P ≤ generatedSigmaAlgebra μ Q) (hP : IsGenerating μ T P) : IsGenerating μ T Q

A refinement of a generator is a generator: if σ(P) ≤ σ(Q) and P generates, then Q generates. The ambient σ-algebra mα always dominates Q's forward saturation (each cell of Q is measurable, so σ(Q) ≤ mα, hence every comap (T^[n]) σ(Q) ≤ mα); combined with the lower bound from P's saturation via generated_mono, antisymmetry pins it to mα.

structure Oseledets.Entropy.IsGeneratingWithReduction {α : Type u_1} [mα : MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (T : α → α) (hT : MeasureTheory.MeasurePreserving T μ μ) (n : ℕ) : Type u_1

A generator bundled with its supplied reduction equality. Carries a Fin n-indexed generating partition P together with the (externally supplied) Kolmogorov–Sinai reduction h(T) = h(P, T) for the system. The Abramov–Rokhlin assembly (issue #13, M6) consumes one of these for each of the two systems T, S instead of invoking a generator theorem — exactly the supplied-generator interface mandated by the design plan.

• partition : MeasurePartition μ (Fin n)

  The candidate generating partition.

• generating : IsGenerating μ T self.partition

  The partition generates the dynamics.

• reduction : ksEntropy hT = ↑(ksEntropyPartition hT self.partition)

  The supplied Kolmogorov–Sinai entropy-reduction equality h(T) = h(P, T).

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

Hypothesis-form generator reduction. Given the Kolmogorov–Sinai reduction h(T) = h(P, T) as a hypothesis, this lemma simply names and re-exposes it in the form the Abramov–Rokhlin assembly consumes. It does not prove the reduction (the generator theorem is not formalized here); it is the consumable interface for a supplied generator-reduction equality.

theorem Oseledets.Entropy.IsGeneratingWithReduction.ksEntropy_eq {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {T : α → α} {hT : MeasureTheory.MeasurePreserving T μ μ} {n : ℕ} (G : IsGeneratingWithReduction μ T hT n) : ksEntropy hT = ↑(ksEntropyPartition hT G.partition)

Extract the reduction equality from a bundled generator-with-reduction in the consumable form. A trivial projection, provided so the Abramov–Rokhlin assembly can take an IsGeneratingWithReduction and immediately obtain h(T) = h(P, T).