The skyscraper over a base set and the tiling-a.e. theorem (Rokhlin tower, issue #15)

For a measurable automorphism e : α ≃ᵐ α of a standard Borel probability space and a measurable base set A, the skyscraper over A is the disjoint union of the towers above the first-return level sets of A,

skyscraper e A = ⋃ k, ⋃ j ≤ k, eʲ '' (returnLevel e A (k+1)).

This file establishes the two structural facts the Rokhlin (Kakutani) tower lemma needs from the skyscraper:

• its floors are pairwise disjoint (the crux disjoint_skyscraper_floors), and
• it covers almost every point when 0 < μ A (the tiling theorem skyscraper_ae_univ).

Main definitions

• Oseledets.Krieger.skyscraper e A — the skyscraper over A.
• Oseledets.Krieger.sweepOut e A — the forward sweep-out ⋃ j, eʲ '' A.
• Oseledets.Krieger.preimageSweep e A — the orbit-hits-A set ⋃ n, eⁿ ⁻¹' A.

Main results

• disjoint_skyscraper_floors — distinct skyscraper floors eʲ '' (returnLevel e A (k+1)) are disjoint; this is the combinatorial crux of the tower construction.
• skyscraper_ae_univ — when 0 < μ A, the skyscraper covers almost every point. Its proof factors through the ergodicity of the sweep-out (sweepOut_ae_univ) and a re-basing argument (sweepOut_diff_skyscraper_subset) that consumes Poincaré recurrence.

Implementation notes

returnLevel e A (k+1) has return time k+1, so its "no earlier return" condition forbids returns at times 1 ≤ i ≤ k; a floor of column k+1 is eʲ '' (returnLevel e A (k+1)) with j ≤ k.

The skyscraper and its membership characterization

def Oseledets.Krieger.skyscraper {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) : Set α

The skyscraper over A: the union of the towers above the first-return level sets, ⋃ k, ⋃ j ≤ k, eʲ '' (returnLevel e A (k+1)).

Equations

• Oseledets.Krieger.skyscraper e A = ⋃ (k : ℕ), ⋃ j ∈ Finset.range (k + 1), (⇑e)^[j] '' Oseledets.Krieger.returnLevel e A (k + 1)

theorem Oseledets.Krieger.mem_skyscraper_iff {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) (y : α) : y ∈ skyscraper e A ↔ ∃ (k : ℕ), ∃ j ≤ k, ∃ x ∈ returnLevel e A (k + 1), (⇑e)^[j] x = y

Membership: y is in the skyscraper iff there are j ≤ k and x ∈ returnLevel e A (k+1) with y = eʲ x.

theorem Oseledets.Krieger.measurableSet_iterate_image {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (j : ℕ) {s : Set α} (hs : MeasurableSet s) : MeasurableSet ((⇑e)^[j] '' s)

Image of a measurable set under a forward iterate is measurable. eʲ '' s rewrites to the preimage (e.symm)ʲ ⁻¹' s (the same trick as measure_iterate_image), which is measurable.

theorem Oseledets.Krieger.measurableSet_skyscraper {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) {A : Set α} (hA : MeasurableSet A) : MeasurableSet (skyscraper e A)

The skyscraper is measurable: it is a countable union of measurable floors.

The sweep-out sets and ergodicity

def Oseledets.Krieger.sweepOut {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) : Set α

The backward sweep-out: points whose backward orbit hits A (= forward image of A).

Equations

• Oseledets.Krieger.sweepOut e A = ⋃ (j : ℕ), (⇑e)^[j] '' A

def Oseledets.Krieger.preimageSweep {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) : Set α

Forward sweep-out via preimages (the orbit-hits-A set).

Equations

• Oseledets.Krieger.preimageSweep e A = ⋃ (n : ℕ), (⇑e)^[n] ⁻¹' A

theorem Oseledets.Krieger.measurableSet_preimageSweep {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) {A : Set α} (hA : MeasurableSet A) : MeasurableSet (preimageSweep e A)

preimageSweep is measurable.

theorem Oseledets.Krieger.preimage_preimageSweep_subset {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) : ⇑e ⁻¹' preimageSweep e A ⊆ preimageSweep e A

e ⁻¹' preimageSweep ⊆ preimageSweep: orbit-hits-A is forward sub-invariant.

theorem Oseledets.Krieger.skyscraper_subset_sweepOut {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) : skyscraper e A ⊆ sweepOut e A

EASY HALF: every skyscraper floor eʲ '' (returnLevel e A (k+1)) sits inside eʲ '' A, hence inside sweepOut.

theorem Oseledets.Krieger.image_sweepOut_subset {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) : ⇑e '' sweepOut e A ⊆ sweepOut e A

e '' sweepOut ⊆ sweepOut: the orbit-forward set is image-sub-invariant.

theorem Oseledets.Krieger.measurableSet_sweepOut {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) {A : Set α} (hA : MeasurableSet A) : MeasurableSet (sweepOut e A)

sweepOut is measurable.

theorem Oseledets.Krieger.preimageSweep_ae_univ {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (e : α ≃ᵐ α) (herg : Ergodic (⇑e) μ) {A : Set α} (hA : MeasurableSet A) (hApos : 0 < μ A) : preimageSweep e A =ᵐ[μ] Set.univ

Ergodicity (preimage version): if 0 < μ A then a.e. point's forward orbit hits A, i.e. preimageSweep e A =ᵐ univ. Uses Ergodic.ae_empty_or_univ_of_preimage_ae_le.

theorem Oseledets.Krieger.sweepOut_ae_univ {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (e : α ≃ᵐ α) (herg : Ergodic (⇑e) μ) {A : Set α} (hA : MeasurableSet A) (hApos : 0 < μ A) : sweepOut e A =ᵐ[μ] Set.univ

Ergodicity (image version): 0 < μ A ⟹ sweepOut e A =ᵐ univ.

theorem Oseledets.Krieger.measure_nonReturning_eq_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (e : α ≃ᵐ α) (he : MeasureTheory.MeasurePreserving (⇑e) μ μ) {A : Set α} (hA : MeasurableSet A) : μ (A \ ⋃ (k : ℕ), returnLevel e A (k + 1)) = 0

The non-returning bases D := A \ ⋃ k, rl(k+1) are null (Poincaré, via returnLevels_cover).

theorem Oseledets.Krieger.sweepOut_diff_skyscraper_subset {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) : sweepOut e A \ skyscraper e A ⊆ ⋃ (j : ℕ), (⇑e)^[j] '' (A \ ⋃ (k : ℕ), returnLevel e A (k + 1))

The re-basing inclusion. An uncovered sweep-out point re-bases to a non-returning base: sweepOut \ skyscraper ⊆ ⋃ j, eʲ '' D where D := A \ ⋃ k, rl(k+1).

For y = eʲ x with x ∈ A, let j₀ be the least m with (e.symm)ᵐ y ∈ A and set x₀ = (e.symm)^[j₀] y ∈ A. By minimality x₀ has no forward return in (0, j₀]. Either x₀ first-returns at some r > j₀ (then y is genuine floor j₀ of column r, so y ∈ skyscraper, excluded), or x₀ never returns and x₀ ∈ D, so y = e^[j₀] x₀ ∈ e^[j₀] '' D.

theorem Oseledets.Krieger.skyscraper_ae_univ {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (e : α ≃ᵐ α) (he : MeasureTheory.MeasurePreserving (⇑e) μ μ) (herg : Ergodic (⇑e) μ) {A : Set α} (hA : MeasurableSet A) (hApos : 0 < μ A) : skyscraper e A =ᵐ[μ] Set.univ

Tiling theorem. When 0 < μ A, the skyscraper covers almost every point: skyscraper e A =ᵐ univ. Indeed skyscraper ⊆ sweepOut =ᵐ univ, and sweepOut \ skyscraper is null by the re-basing inclusion together with μ (eʲ '' D) = μ D = 0.

The crux: skyscraper floors are pairwise disjoint

theorem Oseledets.Krieger.disjoint_skyscraper_floors {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) {j₁ k₁ j₂ k₂ : ℕ} (hj₁ : j₁ ≤ k₁) (hj₂ : j₂ ≤ k₂) (hne : (j₁, k₁) ≠ (j₂, k₂)) : Disjoint ((⇑e)^[j₁] '' returnLevel e A (k₁ + 1)) ((⇑e)^[j₂] '' returnLevel e A (k₂ + 1))

The crux. Skyscraper floors are pairwise disjoint across all (j, k): for (j₁, k₁) ≠ (j₂, k₂) with j₁ ≤ k₁ and j₂ ≤ k₂, the floors eʲ¹ '' (returnLevel e A (k₁+1)) and eʲ² '' (returnLevel e A (k₂+1)) are disjoint.