Ergodicity of the two-sided Bernoulli shift (mixing via cylinder approximation)

This file proves that the invertible left shift biShiftEquiv on the two-sided full shift BiShift α₀ is ergodic with respect to the i.i.d. product (Bernoulli) measure bernZ ν = Measure.infinitePi (fun _ : ℤ => ν).

Why not Kolmogorov 0–1?

The one-sided proof (Oseledets/Multifractal/BernoulliErgodic.lean) routes through Kolmogorov's 0–1 law on the forward tail ⨅_n ⨆_{i ≥ n} coordSigma i. That argument relies on the iterate shiftMap^[n] x k = x (k + n) with k ∈ ℕ reading only the coordinates {k + n : k ≥ 0} = [n, ∞), so an invariant set lands in the forward tail. For the two-sided shift the iterate biShiftEquiv^[n] x k = x (k + n) with k ∈ ℤ reads {k + n : k ∈ ℤ} = ℤ — all coordinates — so an invariant set is not tail-measurable and the 0–1-law-on-the-tail does not apply.

The honest route: mixing by cylinder approximation

This is the standard textbook proof. Let A be a measurable biShiftEquiv-invariant set and write μ = bernZ ν, T = biShiftEquiv.

• Approximation. Every measurable A is approximated in symmetric difference by a finite-block cylinder C (a set measurable with respect to the coordinates in a finite block J ⊆ ℤ): ∀ ε > 0, ∃ C ∈ blockAlg, μ (C ∆ A) < ε. This is Mathlib's MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetRing, applied to the ring blockAlg of finite-block sets, which generates the product σ-algebra and contains univ.
• Independence of separated blocks. For n large, the block J of C and the block J + n of T^[n] ⁻¹' C are disjoint, so the two sets are independent under the i.i.d. measure (ProbabilityTheory.indep_iSup_of_disjoint applied to the independent coordinate σ-algebras): μ (C ∩ T^[n] ⁻¹' C) = μ C · μ (T^[n] ⁻¹' C) = (μ C)² (the last step by measure preservation).
• Pushing through. μ A = μ (A ∩ T^[n] ⁻¹' A) by invariance, and intersections are stable in symmetric difference, so μ A and (μ C)² differ by O(ε), while μ A and μ C differ by ε. Letting ε → 0 gives (μ A) = (μ A)², hence μ A ∈ {0, 1} ⟹ ergodicity.

Main result

• ergodic_biShiftEquiv_bernZ : Ergodic biShiftEquiv (bernZ ν).

The integer-coordinate σ-algebras and their independence

@[reducible]

def Oseledets.Multifractal.coordSigmaZ {α₀ : Type u_1} [MeasurableSpace α₀] (n : ℤ) : MeasurableSpace (BiShift α₀)

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

Equations

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

theorem Oseledets.Multifractal.iIndep_coordSigmaZ_bernZ {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : ProbabilityTheory.iIndep coordSigmaZ (bernZ ν)

Independence of coordinates. Under the two-sided Bernoulli measure the coordinate σ-algebras coordSigmaZ 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.coordSigmaZ_le {α₀ : Type u_1} [MeasurableSpace α₀] (n : ℤ) : coordSigmaZ n ≤ inferInstance

Each integer-coordinate σ-algebra is below the ambient product σ-algebra.

The finite-block σ-algebra and the ring of cylinders

@[reducible]

def Oseledets.Multifractal.piBlock {α₀ : Type u_1} [MeasurableSpace α₀] (J : Finset ℤ) : MeasurableSpace (BiShift α₀)

The σ-algebra of events depending only on the coordinates in a finite block J ⊆ ℤ: the supremum of the coordinate σ-algebras over J.

Equations

• Oseledets.Multifractal.piBlock J = ⨆ i ∈ J, Oseledets.Multifractal.coordSigmaZ i

theorem Oseledets.Multifractal.piBlock_le {α₀ : Type u_1} [MeasurableSpace α₀] (J : Finset ℤ) : piBlock J ≤ inferInstance

Each finite-block σ-algebra is below the ambient product σ-algebra.

theorem Oseledets.Multifractal.piBlock_mono {α₀ : Type u_1} [MeasurableSpace α₀] {J K : Finset ℤ} (h : J ⊆ K) : piBlock J ≤ piBlock K

Enlarging the block enlarges the block σ-algebra.

theorem Oseledets.Multifractal.coordSigmaZ_le_piBlock_singleton {α₀ : Type u_1} [MeasurableSpace α₀] (i : ℤ) : coordSigmaZ i ≤ piBlock {i}

A single coordinate σ-algebra sits inside the block over the singleton block.

def Oseledets.Multifractal.blockAlg {α₀ : Type u_1} [MeasurableSpace α₀] : Set (Set (BiShift α₀))

The ring of finite-block cylinders: the sets that are measurable with respect to some finite block of coordinates. This is the ring fed to the symmetric-difference approximation lemma.

Equations

• Oseledets.Multifractal.blockAlg = {s : Set (Oseledets.Multifractal.BiShift α₀) | ∃ (J : Finset ℤ), MeasurableSet s}

theorem Oseledets.Multifractal.mem_blockAlg {α₀ : Type u_1} [MeasurableSpace α₀] {s : Set (BiShift α₀)} : s ∈ blockAlg ↔ ∃ (J : Finset ℤ), MeasurableSet s

Membership unfolding for the finite-block ring.

theorem Oseledets.Multifractal.mem_blockAlg_of_piBlock {α₀ : Type u_1} [MeasurableSpace α₀] {J : Finset ℤ} {s : Set (BiShift α₀)} (hs : MeasurableSet s) : s ∈ blockAlg

A block-J measurable set is a member of the finite-block ring.

theorem Oseledets.Multifractal.isSetRing_blockAlg {α₀ : Type u_1} [MeasurableSpace α₀] : MeasureTheory.IsSetRing blockAlg

The finite-block ring is a genuine ring of sets: it contains ∅ and is closed under union and set difference. Two block-measurable sets are jointly measurable over the union of their blocks, where a sub-σ-algebra is closed under all Boolean operations.

theorem Oseledets.Multifractal.pi_eq_iSup_coordSigmaZ {α₀ : Type u_1} [MeasurableSpace α₀] : inferInstance = ⨆ (i : ℤ), coordSigmaZ i

The ambient product σ-algebra is the supremum of the integer-coordinate σ-algebras.

theorem Oseledets.Multifractal.generateFrom_blockAlg {α₀ : Type u_1} [MeasurableSpace α₀] : inferInstance = MeasurableSpace.generateFrom blockAlg

The finite-block ring generates the ambient product σ-algebra. The product σ-algebra is the supremum of the coordinate σ-algebras, each of which is generated by a singleton-block cylinder, so the generated σ-algebra is exactly MeasurableSpace.pi.

theorem Oseledets.Multifractal.univ_mem_blockAlg {α₀ : Type u_1} [MeasurableSpace α₀] : Set.univ ∈ blockAlg

The whole space is a finite-block cylinder (the empty block), so the ring covers the space — the nondegeneracy hypothesis of the approximation lemma.

Cylinder approximation of an arbitrary measurable set

theorem Oseledets.Multifractal.exists_blockAlg_symmDiff_lt {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] {A : Set (BiShift α₀)} (hA : MeasurableSet A) {ε : ENNReal} (hε : 0 < ε) : ∃ C ∈ blockAlg, (bernZ ν) (symmDiff C A) < ε

Cylinder approximation. Any measurable set is approximated, in symmetric difference, by a finite-block cylinder. This is Mathlib's exists_measure_symmDiff_lt_of_generateFrom_isSetRing specialized to the finite-block ring (which contains univ, so the space is covered modulo 0, and which generates the product σ-algebra).

The shifted block of a cylinder under an iterate of the shift

theorem Oseledets.Multifractal.biShiftMap_iterate_apply' {α₀ : Type u_1} (k : ℕ) (x : BiShift α₀) (i : ℤ) : biShiftMap^[k] x i = x (i + ↑k)

The k-th iterate of the two-sided shift advances every (integer) index by k: biShiftMap^[k] x i = x (i + k). (Local copy, to avoid importing the entropy module.)

def Oseledets.Multifractal.blockShiftEmb (k : ℕ) : ℤ ↪ ℤ

The block-translation embedding i ↦ i + k of ℤ into itself, used to re-index a finite block under the iterate biShiftMap^[k].

Equations

• Oseledets.Multifractal.blockShiftEmb k = { toFun := fun (i : ℤ) => i + ↑k, inj' := ⋯ }

@[simp]

theorem Oseledets.Multifractal.blockShiftEmb_apply (k : ℕ) (i : ℤ) : (blockShiftEmb k) i = i + ↑k

theorem Oseledets.Multifractal.comap_iterate_coordSigmaZ {α₀ : Type u_1} [MeasurableSpace α₀] (k : ℕ) (i : ℤ) : MeasurableSpace.comap biShiftMap^[k] (coordSigmaZ i) = coordSigmaZ (i + ↑k)

Pulling back the i-th coordinate σ-algebra along biShiftMap^[k] gives the (i + k)-th coordinate σ-algebra: eval i ∘ biShiftMap^[k] = eval (i + k) since biShiftMap^[k] x i = x (i+k).

theorem Oseledets.Multifractal.comap_iterate_piBlock {α₀ : Type u_1} [MeasurableSpace α₀] (k : ℕ) (J : Finset ℤ) : MeasurableSpace.comap biShiftMap^[k] (piBlock J) = piBlock (Finset.map (blockShiftEmb k) J)

Pulling back a single block-summand ⨆ (_ : i ∈ J), coordSigmaZ i along biShiftMap^[k] re-indexes the coordinate to i + k.

theorem Oseledets.Multifractal.measurableSet_preimage_iterate_piBlock {α₀ : Type u_1} [MeasurableSpace α₀] (k : ℕ) {J : Finset ℤ} {C : Set (BiShift α₀)} (hC : MeasurableSet C) : MeasurableSet (biShiftMap^[k] ⁻¹' C)

Shifted-cylinder measurability. If C is a block-J cylinder, then its preimage under the iterate biShiftMap^[k] is a block-(J + k) cylinder.

Independence of separated blocks

theorem Oseledets.Multifractal.piBlock_eq_iSup_coe {α₀ : Type u_1} [MeasurableSpace α₀] (J : Finset ℤ) : piBlock J = ⨆ i ∈ ↑J, coordSigmaZ i

The finite-block σ-algebra over J is the supremum of the coordinate σ-algebras over J viewed as a set of indices, the form consumed by ProbabilityTheory.indep_iSup_of_disjoint.

theorem Oseledets.Multifractal.measure_inter_of_disjoint_blocks {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] {J K : Finset ℤ} (hJK : Disjoint J K) {C D : Set (BiShift α₀)} (hC : MeasurableSet C) (hD : MeasurableSet D) : (bernZ ν) (C ∩ D) = (bernZ ν) C * (bernZ ν) D

Independence of disjoint blocks. If the blocks J and K are disjoint, then a block-J cylinder C and a block-K cylinder D are independent under the two-sided Bernoulli measure: bernZ ν (C ∩ D) = bernZ ν C · bernZ ν D. This is the i.i.d. independence of the coordinate σ-algebras (iIndep_coordSigmaZ_bernZ) grouped over the disjoint index blocks (indep_iSup_of_disjoint).

theorem Oseledets.Multifractal.exists_disjoint_shifted_block (J : Finset ℤ) : ∃ (N : ℕ), ∀ (k : ℕ), N ≤ k → Disjoint J (Finset.map (blockShiftEmb k) J)

For any finite block J, all sufficiently large forward shifts of J are disjoint from J: there is N so that Disjoint J (J.map (blockShiftEmb k)) for every k ≥ N. Concretely, pick N beyond the diameter of J.

The mixing squeeze and pre-ergodicity

theorem Oseledets.Multifractal.symmDiff_inter_subset {α₀ : Type u_1} (C D A B : Set (BiShift α₀)) : symmDiff (C ∩ D) (A ∩ B) ⊆ symmDiff C A ∪ symmDiff D B

The symmetric difference of two intersections is contained in the union of the corresponding symmetric differences: (C ∩ D) ∆ (A ∩ B) ⊆ (C ∆ A) ∪ (D ∆ B).

theorem Oseledets.Multifractal.measureReal_invariant_sq {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] {A : Set (BiShift α₀)} (hA : MeasurableSet A) (hinv : ⇑biShiftEquiv ⁻¹' A = A) : (bernZ ν).real A * (bernZ ν).real A = (bernZ ν).real A

The mixing squeeze. For a measurable biShiftEquiv-invariant set A, the real measure a = bernZ ν A satisfies |a - a²| ≤ 4 ε for every ε > 0, hence a = a². The cylinder C that ε-approximates A is independent of its own large forward shift (disjoint blocks), giving (bernZ ν C).real² = bernZ ν (C ∩ shift⁻¹ C), while invariance gives a = bernZ ν (A ∩ shift⁻¹ A); the two intersections differ by 2 ε in measure and C, A differ by ε.

Pre-ergodicity and the main result

theorem Oseledets.Multifractal.measure_invariant_eq_zero_or_one_bernZ {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] {A : Set (BiShift α₀)} (hA : MeasurableSet A) (hinv : ⇑biShiftEquiv ⁻¹' A = A) : (bernZ ν) A = 0 ∨ (bernZ ν) A = 1

Pre-ergodicity via mixing. Any measurable biShiftEquiv-invariant set has bernZ ν-measure 0 or 1. The real measure a satisfies a² = a (the mixing squeeze), so a ∈ {0, 1}; lifting back to ENNReal gives bernZ ν A ∈ {0, 1}.

theorem Oseledets.Multifractal.ergodic_biShiftEquiv_bernZ {α₀ : Type u_1} [MeasurableSpace α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] : Ergodic (⇑biShiftEquiv) (bernZ ν)

Ergodicity of the two-sided Bernoulli shift. The invertible left shift biShiftEquiv is ergodic with respect to the i.i.d. product (Bernoulli) measure bernZ ν. The measure-preserving half is measurePreserving_biShiftEquiv_bernZ; pre-ergodicity is the mixing argument (measure_invariant_eq_zero_or_one_bernZ) — the honest, textbook route via cylinder approximation, since the two-sided shift's invariant sets are not tail-measurable and Kolmogorov's 0–1 law does not apply.