First-return level sets and tower primitives (Rokhlin tower, issue #15)

This file develops the first-return level-set machinery underlying the Rokhlin (Kakutani) tower lemma. For a measurable automorphism e : α ≃ᵐ α of a standard Borel probability space and a measurable set A, the first-return level set returnLevel e A k collects the points of A whose orbit first returns to A at time exactly k.

Main definitions

• Oseledets.Krieger.returnLevel e A k — points x ∈ A with eᵏ x ∈ A and eⁱ x ∉ A for all 1 ≤ i < k.

Main results

• measurableSet_returnLevel — returnLevel e A k is measurable when A is.
• measure_iterate_image — iterating a measure-preserving automorphism preserves measure of images (the "tower floor" measure primitive).
• disjoint_iterate_image — iterating an injection preserves disjointness of images.
• returnLevels_cover — Poincaré recurrence: a.e. point of A first returns, so A is, up to a null set, the disjoint union ⋃ k, returnLevel e A (k+1) of its first-return level sets.
• tsum_returnLevel_eq — the weak partition identity ∑' k, μ (returnLevel e A (k+1)) = μ A.

Index convention

returnLevel e A 0 = A is degenerate (the "first return before time 0" conditions are vacuous), so genuine first-return decompositions are indexed by returnLevel e A (k+1) for k : ℕ, i.e. by return times ≥ 1. Downstream tower constructions should index floors by k : ℕ via returnLevel e A (k+1) (return time k + 1).

Implementation notes

Only the weak partition identity ∑' k, μ (returnLevel e A (k+1)) = μ A (tsum_returnLevel_eq) is established here, which is all the Rokhlin tower construction needs. Kac's full return-time theorem (∑' k, (k+1) · μ (returnLevel e A (k+1)) = μ (⋃ orbit)) is not required.

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

The first-return level set: points x ∈ A whose orbit under e returns to A for the first time at time exactly k, i.e. eᵏ x ∈ A while eⁱ x ∉ A for every 1 ≤ i < k.

Note returnLevel e A 0 = A is degenerate (the intermediate conditions are vacuous); the genuine first-return decomposition is indexed by returnLevel e A (k+1), return times ≥ 1.

Equations

• Oseledets.Krieger.returnLevel e A k = A ∩ (⇑e)^[k] ⁻¹' A ∩ {x : α | ∀ (i : ℕ), 1 ≤ i → i < k → (⇑e)^[i] x ∉ A}

theorem Oseledets.Krieger.noEarlierReturn_eq {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) (k : ℕ) : {x : α | ∀ (i : ℕ), 1 ≤ i → i < k → (⇑e)^[i] x ∉ A} = ⋂ i ∈ Finset.Ico 1 k, ((⇑e)^[i] ⁻¹' A)ᶜ

The "no earlier return" factor of returnLevel written as a bounded intersection of measurable preimage complements.

theorem Oseledets.Krieger.measurableSet_returnLevel {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) {A : Set α} (hA : MeasurableSet A) (k : ℕ) : MeasurableSet (returnLevel e A k)

F3a. The first-return level set is measurable whenever A is.

theorem Oseledets.Krieger.measure_iterate_image {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (e : α ≃ᵐ α) (he : MeasureTheory.MeasurePreserving (⇑e) μ μ) (i : ℕ) {B : Set α} (hB : MeasurableSet B) : μ ((⇑e)^[i] '' B) = μ B

T1. Iterating a measure-preserving automorphism preserves the measure of images: μ (eⁱ '' B) = μ B. (The "tower floor" measure primitive.)

theorem Oseledets.Krieger.disjoint_iterate_image {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (i : ℕ) {s t : Set α} (h : Disjoint s t) : Disjoint ((⇑e)^[i] '' s) ((⇑e)^[i] '' t)

T2. Iterating an injection preserves disjointness of images.

theorem Oseledets.Krieger.pairwise_disjoint_returnLevel {α : Type u_1} [MeasurableSpace α] (e : α ≃ᵐ α) (A : Set α) : Pairwise (Function.onFun Disjoint fun (k : ℕ) => returnLevel e A (k + 1))

The first-return level sets returnLevel e A (k+1) are pairwise disjoint: distinct first-return times.

theorem Oseledets.Krieger.returnLevels_cover {α : 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)

F3b. First-return cover (Poincaré recurrence): a.e. point of A returns to A, hence A agrees, up to a null set, with the union of its first-return level sets ⋃ k, returnLevel e A (k+1) over return times ≥ 1.

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

F3c. Weak partition identity: the first-return level sets partition A up to a null set, so their measures sum to μ A. (This is all the Rokhlin tower needs; Kac's full theorem is not.)