Documentation

Oseledets.Krieger.Krieger

Krieger's finite generator theorem — headline assembly (Krieger M3) #

This file states and proves the headline assembly of Krieger's finite generator theorem (issue #15), reducing it to the upstream Rokhlin-tower / name-count coding construction through the recovery core of Oseledets.Krieger.Coding.

The theorem #

Let e : α ≃ᵐ α be an ergodic, aperiodic, measure-preserving automorphism of a standard-Borel probability space (α, μ), with finite Kolmogorov–Sinai entropy h. If k : ℕ satisfies Real.log k > h, then e admits a finite two-sided generator of size ≤ k: a partition P : MeasurePartition μ (Fin k) that is IsGeneratingTwoSidedMod0 (generates mod 0).

The proof has three layers, of which this file is the top:

Why mod 0 #

Generators in ergodic theory always generate the σ-algebra up to null sets (mod 0): the Krieger construction produces an a.e.-defined, a.e.-invertible code, which recovers each generator cell only modulo a μ-null set. Against an honest standard-Borel (non-μ-complete) mα this cannot establish a literal σ-algebra equality, so the headline is — faithfully — phrased with the mod-0 conditions IsGeneratingTwoSidedMod0 / CodesTwoSidedMod0 (the μ-completion of the two-sided saturation is the full ambient). See Oseledets.Krieger.Coding for the mod-0 development and Oseledets.Krieger.isGeneratingTwoSidedMod0_of_literal for faithfulness (literal ⟹ mod 0).

What is proved here, and what is supplied #

The recovery half — that a mod-0 code of a mod-0 two-sided generator is a mod-0 two-sided generator — is proved unconditionally in Oseledets.Krieger.Coding and is wired in here. The coding-existence half — that log k > h (plus ergodicity, aperiodicity, the Rokhlin tower and the name count) yields a Fin k-valued mod-0 code of a two-sided generator — is the genuine combinatorial crux of Krieger's theorem; it is consumed here through the named hypothesis KriegerCodingData (the existence of the coded partition), exactly the object the M1+M2 layers produce. Both packaged forms are provided:

Main definitions #

Main results #

References #

source
def Oseledets.Krieger.Aperiodic {α : Type u_1} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (μ : MeasureTheory.Measure α) :
Prop

A.e.-aperiodicity of the automorphism e. For every nonzero integer n, the set of n-periodic points {x | eⁿ x = x} is μ-null. Equivalently: μ-a.e. point has trivial stabiliser under the ℤ-action n ↦ eⁿ. This is the standard measure-theoretic aperiodicity hypothesis under which Rokhlin's lemma (the M1 tower) holds; for an ergodic automorphism of a non-atomic probability space it is automatic, but it is kept explicit here as the hypothesis the tower construction consumes.

Equations
Instances For
    source
    structure Oseledets.Krieger.KriegerCodingData {α : Type u_1} [mα : MeasurableSpace α] (e : α ≃ᵐ α) (μ : MeasureTheory.Measure α) (k : ℕ) :
    Type (max u_1 (u_2 + 1))

    The coding data produced by the Krieger combinatorics (M1 + M2). Bundles the measure-preservation of e, a countable index type κ with a family of cells Q that two-sidedly generates (α, e, μ) mod 0 (Oseledets.Krieger.IsGeneratingTwoSidedMod0c, the Countable-layer condition), together with a Fin k-valued partition P that codes the countable Q two-sidedly mod 0 across the two layers (the two-sided P-itinerary recovers each Q-cell up to a μ-null set, Oseledets.Krieger.CodesTwoSidedMod0c).

    This is exactly the object the unconditional Krieger construction yields when Real.log k > h: Q is the countable finite-entropy two-sided generator produced by the Keane–Serafin / Downarowicz half (Oseledets.Krieger.exists_countable_twoSided_generator, sub-problem A), and P is the column-coding Fin k partition built from the ≤ kᴺ name bound (sub-problem B), which recovers the countable Q-name only a.e. The two saturation layers — the Countable layer of Generator.lean for Q and the Fintype layer of Coding.lean for P — are bridged by CodesTwoSidedMod0c. The headline turns a KriegerCodingData into a finite mod-0 two-sided generator by the cross-layer recovery Oseledets.Krieger.IsGeneratingTwoSidedMod0c.of_codesc. The measure-preservation mp is carried because that recovery needs it: preimage under the iterates eⁿ must commute with the μ-completion.

    • mp : MeasureTheory.MeasurePreserving (⇑e) μ μ

      e is measure preserving (needed for mod-0 shift-invariance of the saturation).

    • κ : Type u_2

      The (countable) index type of the auxiliary generator Q.

    • countableκ : Countable self.κ

      κ is countable — Q is a countable (finite-entropy) generator.

    • gen : self.κ → Set α

      A countable family of cells that two-sidedly generates the dynamics mod 0.

    • gen_measurable (i : self.κ) : MeasurableSet (self.gen i)

      Each cell of the countable generator is measurable.

    • code : Entropy.MeasurePartition μ (Fin k)

      The candidate Fin k-valued coding partition.

    • gen_generating : IsGeneratingTwoSidedMod0c μ e self.gen

      The countable generator Q = gen two-sidedly generates (α, e, μ) mod 0.

    • code_codes : CodesTwoSidedMod0c e self.gen self.code

      The coding partition P = code codes the countable Q two-sidedly mod 0 (cross-layer): its two-sided itinerary recovers each cell of Q up to a μ-null set.

    Instances For
      source
      theorem Oseledets.Krieger.krieger_finite_generator_of_coding {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} {e : α ≃ᵐ α} {k : ℕ} (D : KriegerCodingData e μ k) :
      ∃ (P : Entropy.MeasurePartition μ (Fin k)), IsGeneratingTwoSidedMod0 e P

      The recovery assembly of Krieger's theorem. Given coding data D — a Fin k-valued partition D.code that two-sidedly codes, mod 0, the countable mod-0 two-sided generator D.gen — the coding partition itself is a finite mod-0 two-sided generator. This is the unconditional top layer: it is exactly the cross-layer recovery Oseledets.Krieger.CodesTwoSidedMod0c.isGeneratingTwoSidedMod0 applied to D, repackaged as an existence statement (bridging the Countable generator layer to the Fintype coding layer).

      No entropy, ergodicity, or aperiodicity hypotheses enter here: those are consumed upstream, in producing the coding data D. This lemma is the pure recovery content of Krieger's theorem.

      source
      theorem Oseledets.Krieger.krieger_finite_generator {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {e : α ≃ᵐ α} (_he : MeasureTheory.MeasurePreserving (⇑e) μ μ) (_herg : Ergodic (⇑e) μ) (_hap : Aperiodic e μ) {k : ℕ} {h : ℝ} (_hk : Real.log ↑k > h) (hcode : KriegerCodingData e μ k) :
      ∃ (P : Entropy.MeasurePartition μ (Fin k)), IsGeneratingTwoSidedMod0 e P

      Krieger's finite generator theorem (headline assembly).

      Let e : α ≃ᵐ α be an ergodic, aperiodic, measure-preserving automorphism of a standard-Borel probability space (α, μ) with Kolmogorov–Sinai entropy h := (ksEntropy he).toReal. If k : ℕ satisfies Real.log k > h, and the Krieger coding construction supplies a Fin k-valued mod-0 code of a mod-0 two-sided generator (KriegerCodingData e μ k), then e admits a finite two-sided generator of size ≤ k, mod 0: a partition P : MeasurePartition μ (Fin k) with IsGeneratingTwoSidedMod0 e P (the μ-completion of its two-sided saturation is the full ambient σ-algebra). The mod-0 conclusion is the standard, faithful form of Krieger's theorem: ergodic-theory generators generate up to null sets (see Oseledets.Krieger.Coding).

      The dynamical hypotheses (herg, hap, he) and the entropy threshold hk : Real.log k > h are precisely the inputs the upstream M1 (Rokhlin tower) and M2 (name count) layers consume to produce the coding data hcode; carried here, they make the statement faithful to Krieger's theorem while the assembly itself reduces to the unconditional recovery krieger_finite_generator_of_coding. (When M1+M2 are wired in, hcode is discharged from herg, hap, he, and hk, yielding the unconditional theorem.)