Ergodicity of the one-sided Bernoulli shift (Kolmogorov 0–1 law)

This file proves node N3 of the Bernoulli witness: the left shift shiftMap on the one-sided full shift Shift α₀ is ergodic with respect to the i.i.d. product (Bernoulli) measure bern ν = Measure.infinitePi (fun _ => ν).

The proof is the classical route through Kolmogorov's 0–1 law, not mixing.

• Ergodic = MeasurePreserving ∧ PreErgodic. The measure-preserving half is the on-main measurePreserving_shiftMap_bern.
• For PreErgodic we must show that any measurable shiftMap-invariant set has bern ν-measure 0 or 1.
• Independence of coordinates. The coordinate σ-algebras coordSigma n := MeasurableSpace.comap (fun x => x n) inferInstance are independent under bern ν (ProbabilityTheory.iIndepFun_infinitePi on the coordinate projections, then ProbabilityTheory.iIndepFun.iIndep).
• Tail-bridge (the in-repo work). A shiftMap-invariant measurable set s satisfies s = (shiftMap^[n]) ⁻¹' s for every n. Since shiftMap^[n] reads output coordinate k from input coordinate k + n ≥ n, it is measurable for the σ-algebra ⨆ i ≥ n, coordSigma i; hence s is measurable for that σ-algebra for every n, i.e. for the tail Filter.limsup coordSigma Filter.atTop = ⨅ n, ⨆ i ≥ n, coordSigma i.
• 0–1 law. ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop then forces bern ν s ∈ {0, 1}.

This discharges the standing Ergodic shiftMap μ conditional of the headline dimH_eq_ksEntropy_div_log_two.

Main result

• ergodic_shiftMap_bern : Ergodic shiftMap (bern ν).

N3 — the coordinate σ-algebras and the tail bridge

@[reducible]

def Oseledets.Multifractal.coordSigma {α₀ : Type u_1} [MeasurableSpace α₀] (n : ℕ) : MeasurableSpace (Shift α₀)

The σ-algebra generated by the n-th coordinate projection of the one-sided full shift.

Equations

• Oseledets.Multifractal.coordSigma n = MeasurableSpace.comap (fun (x : Oseledets.Multifractal.Shift α₀) => x n) inferInstance

theorem Oseledets.Multifractal.iIndep_coordSigma_bern {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : ProbabilityTheory.iIndep coordSigma (bern ν)

Independence of coordinates. Under the Bernoulli measure the coordinate σ-algebras coordSigma form an independent family. This is iIndepFun_infinitePi applied to the identity coordinate projections, converted from iIndepFun to iIndep of the generated σ-algebras.

theorem Oseledets.Multifractal.coordSigma_le {α₀ : Type u_1} [MeasurableSpace α₀] (n : ℕ) : coordSigma n ≤ inferInstance

Each coordinate σ-algebra is below the ambient σ-algebra on the full shift.

theorem Oseledets.Multifractal.measurable_shiftMap_iterate_tail {α₀ : Type u_1} [MeasurableSpace α₀] (n : ℕ) : Measurable shiftMap^[n]

The n-th shift iterate is measurable when the domain carries the σ-algebra generated by the coordinates ≥ n: its k-th output coordinate is the input coordinate k + n ≥ n.

theorem Oseledets.Multifractal.measurableSet_limsup_of_invariant {α₀ : Type u_1} [MeasurableSpace α₀] {s : Set (Shift α₀)} (hs : MeasurableSet s) (hinv : shiftMap ⁻¹' s = s) : MeasurableSet s

Tail-measurability of an invariant set. A measurable shiftMap-invariant set is measurable with respect to the tail σ-algebra Filter.limsup coordSigma Filter.atTop.

N3 — the 0–1 law and ergodicity

theorem Oseledets.Multifractal.measure_invariant_eq_zero_or_one {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] {s : Set (Shift α₀)} (hs : MeasurableSet s) (hinv : shiftMap ⁻¹' s = s) : (bern ν) s = 0 ∨ (bern ν) s = 1

Pre-ergodicity via the 0–1 law. Any measurable shiftMap-invariant set has bern ν-measure 0 or 1: it is tail-measurable, and the Bernoulli coordinates are independent.

theorem Oseledets.Multifractal.ergodic_shiftMap_bern {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : Ergodic shiftMap (bern ν)

N3 (ergodicity of the Bernoulli shift). The left shift shiftMap is ergodic with respect to the i.i.d. product measure bern ν. The measure-preserving half is measurePreserving_shiftMap_bern; pre-ergodicity is Kolmogorov's 0–1 law applied to the tail-measurable invariant sets.