The coding layer for Krieger's finite generator theorem: two-sided recovery (Krieger M3) #

This file is the σ-algebra recovery core of Krieger's finite generator theorem. The classical proof (Krieger 1970; Einsiedler–Lindenstrauss–Ward Entropy in Ergodic Theory §3) builds a finite Fin k-valued partition P by coding the columns of a Rokhlin tower so that the two-sided P-itinerary of a.e. point recovers its full itinerary under a fixed countable generator Q. The combinatorial heart — that log k > h forces the number of N-names to be ≤ kᴺ up to ε, so a Fin k code exists — is supplied upstream (the name-count layer M2, the Rokhlin tower M1). What remains, and is proved here unconditionally, is the recovery half: once a candidate code P has the property that every cell of Q is recovered, mod 0, by the two-sided P-saturation, P two-sidedly generates mod 0 whenever Q does.

Why mod 0: generators in ergodic theory generate up to null sets #

The classical Krieger construction produces a code map that is defined and invertible only μ-almost everywhere, so it recovers each generator cell only modulo a μ-null set. This is not an artefact of the formalization: in ergodic theory a "generator" always means mod 0 — a partition generates the σ-algebra up to null sets — because the ambient σ-algebra mα of a standard-Borel space is not μ-complete, so an a.e.-defined code can never establish a literal σ-algebra equality with mα. (See Glasner, Ergodic Theory via Joinings; Einsiedler– Lindenstrauss–Ward, Entropy in Ergodic Theory, Ch. 2 on generators; Downarowicz §4.2, where the strong-generator condition is 𝓑 = σ(⋃ₙ Tⁿ α) mod μ.) The literal equality twoSidedSat e P = mα is therefore too strong / non-standard, and the unconditional Krieger construction provably cannot discharge it; the mod-0 condition is the faithful one.

We formalize "mod 0" with Mathlib's MeasureTheory.eventuallyMeasurableSpace m₀ (ae μ): the σ-algebra of sets that are =ᵐ[μ]-equal to an m₀-measurable set (the μ-completion of the sub-σ-algebra m₀). Crucially this keeps every statement at the level of an order relation ≤ between MeasurableSpace α values, with the ambient measure μ fixed against mα — so the proofs never rewrite the σ-algebra index of μ (which would break, since Measure α is indexed by its MeasurableSpace).

The two-sided saturation and its (literal and mod-0) shift-invariance #

For e : α ≃ᵐ α and a finite partition P, write twoSidedSat e P := ⨆ n : ℤ, comap (eⁿ) σ(P) for the σ-algebra generated by the whole two-sided P-itinerary. The single structural fact that drives everything is shift-invariance: pulling twoSidedSat e P back by any iterate eᵐ lands inside twoSidedSat e P again, because reindexing the ℤ-supremum n ↦ n + m is a bijection of ℤ (comap_twoSidedSat_le). This is precisely where two-sidedness (⨆ over ℤ, not ℕ) is load-bearing: a forward ℕ-supremum is not shift-invariant under the backward iterate e⁻¹.

The mod-0 layer lifts this: for a measure-preserving e, preimage under eᵐ commutes with the μ-completion (comap_eventuallyMeasurableSpace_le, using that a measure-preserving map is quasi-measure-preserving so s =ᵐ t ⟹ f⁻¹s =ᵐ f⁻¹t), and the completion is monotone and idempotent (eventuallyMeasurableSpace_mono, eventuallyMeasurableSpace_idem). These give mod-0 shift-invariance (comap_eventuallyMeasurableSpace_twoSidedSat_le) and the mod-0 recovery monotonicity (twoSidedSat_mono_of_codes), so a mod-0 generator Q lifts to a mod-0 generator P (IsGeneratingTwoSidedMod0.of_codes).

The coding interface consumed by the headline #

The upstream coding construction is exposed to the headline through the predicate CodesTwoSidedMod0 e Q P, which packages the mod-0 recovery hypothesis σ(Q) ≤ eventuallyMeasurableSpace (twoSidedSat e P) (ae μ) — every cell of Q is, mod 0, in the two-sided P-saturation. The headline (Oseledets.Krieger.krieger_finite_generator) takes the existence of a Fin k-valued P with CodesTwoSidedMod0 e Q P (the conclusion of the M1+M2 combinatorics) and concludes IsGeneratingTwoSidedMod0 e P via CodesTwoSidedMod0.isGeneratingTwoSidedMod0.

For the symbolic-code construction (C1–C3) the convenient sufficient condition is provided by codesTwoSidedMod0_of_aeRecovery: it suffices to exhibit, for each cell of Q, a twoSidedSat e P-measurable set =ᵐ[μ]-equal to it — exactly what an a.e.-injective measurable code recovering the Q-name produces.

Main definitions #

Oseledets.Krieger.twoSidedSat: the two-sided itinerary σ-algebra ⨆ n : ℤ, comap (eⁿ) σ(P).
Oseledets.Krieger.IsGeneratingTwoSidedMod0: P two-sidedly generates mod 0.
Oseledets.Krieger.CodesTwoSidedMod0: P's two-sided itinerary recovers each cell of Q mod 0.

Main results #

Oseledets.Krieger.comap_twoSidedSat_le: (literal) shift-invariance of the two-sided saturation.
Oseledets.Krieger.comap_eventuallyMeasurableSpace_twoSidedSat_le: mod-0 shift-invariance.
Oseledets.Krieger.twoSidedSat_mono_of_codes: mod-0 recovery monotonicity.
Oseledets.Krieger.IsGeneratingTwoSidedMod0.of_codes: recovery lifts a mod-0 two-sided generator.
Oseledets.Krieger.CodesTwoSidedMod0.isGeneratingTwoSidedMod0: a mod-0 code of a mod-0 two-sided generator is a mod-0 two-sided generator.
Oseledets.Krieger.isGeneratingTwoSidedMod0_of_literal: faithfulness — the (non-standard) literal condition is stronger than the (standard) mod-0 one.
Oseledets.Krieger.codesTwoSidedMod0_of_aeRecovery: the convenient sufficient condition the symbolic-code layer discharges.

References #

Wolfgang Krieger, On entropy and generators of measure-preserving transformations, Trans. Amer. Math. Soc. 149 (1970), 453–464.
Manfred Einsiedler, Elon Lindenstrauss and Thomas Ward, Entropy in Ergodic Theory and Homogeneous Dynamics (book in progress), Ch. 2 (generators, mod 0) and §3 (the Krieger generator theorem).
Eli Glasner, Ergodic Theory via Joinings, Math. Surveys Monogr. 101, AMS (2003) — Krieger chapter (generators are mod 0).
Tomasz Downarowicz, Entropy in Dynamical Systems, Cambridge (2011), §4.2 (the strong-generator condition holds mod μ).