The suspension (mapping-torus) of a measure-preserving map

This module builds the suspension (also called the mapping torus or flow under a roof function) of a measure-preserving base map T : X ≃ᵐ X with a strictly positive roof function τ : X → ℝ. The suspension carries the natural one-parameter flow [x, s] ↦ [x, s + t], and it is the standard device for transferring the discrete-time Oseledets multiplicative ergodic theorem to the continuous-flow setting (Ambrose–Kakutani; Bessa–Varandas).

Following the quotient model, the suspension space is

Xᵗ := Quotient (AddAction.orbitRel ℤ (X × ℝ)),

where the ℤ-action is generated by the measurable automorphism

G (x, s) = (T x, s − τ x)

identifying (x, s) with (T x, s − τ x). The half-open box under the roof

suspensionDomain τ = {p : X × ℝ | 0 ≤ p.2 ∧ p.2 < τ p.1}

is a fundamental domain for this action with respect to μ.prod volume, and that is the keystone result of this file: Oseledets.isAddFundamentalDomain_suspensionDomain. It is the Ambrose–Kakutani cross-section structure from which the suspension's invariant probability measure (μ × Leb)|_box / ∫ τ and the per-time measure-preservation of the flow are subsequently obtained.

Main definitions

• Oseledets.suspensionGen: the generating measurable automorphism G (x, s) = (T x, s − τ x).
• Oseledets.suspensionVAdd: the AddAction ℤ (X × ℝ) generated by suspensionGen, defined as the zpow of the underlying permutation.
• Oseledets.roofSum: the signed (integer-indexed) Birkhoff sum τ⁽ⁿ⁾ of the roof function along T, defined as the drop in the ℝ-coordinate under the n-th power of the generator.
• Oseledets.suspensionDomain: the half-open box {p | 0 ≤ p.2 ∧ p.2 < τ p.1}.

Main results

• Oseledets.roofSum_add: the integer roof-cocycle identity, read off from G ^ (m + n) = G ^ m * G ^ n.
• Oseledets.exists_unique_lt_of_strictMono: a pure real-analysis fact — a strictly monotone ℤ-indexed sequence tending to ±∞ partitions ℝ into half-open intervals.
• Oseledets.suspension_exists_unique_vadd_mem: every orbit meets the box exactly once.
• Oseledets.isAddFundamentalDomain_suspensionDomain: the box is a fundamental domain for the ℤ-action with respect to μ.prod volume.

What is not in this file

The downstream construction — the invariant probability measure μ̂ on Xᵗ, the per-time measure-preservation of the suspension flow ζ_t, the packaging as a MeasurePreservingFlow, and the exponent-transfer identity λ_flow = λ_base / ∫ τ — is left to follow-up modules. Establishing those requires the ℤ-invariance of μ.prod volume (the "shear preserves the product measure" lemma) and the descent of the ℝ-translation through the quotient, neither of which is included here. This file deliberately stops at the fundamental-domain keystone, which is self-contained and sorry-free.

def Oseledets.suspensionGen {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) : X × ℝ ≃ᵐ X × ℝ

The generating measurable automorphism of the suspension ℤ-action: G (x, s) = (T x, s − τ x). Its inverse is (x, s) ↦ (T⁻¹ x, s + τ (T⁻¹ x)).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Oseledets.suspensionGen_apply {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (p : X × ℝ) : (suspensionGen T hτ) p = (T p.1, p.2 - τ p.1)

@[simp]

theorem Oseledets.suspensionGen_symm_apply {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (p : X × ℝ) : (suspensionGen T hτ).symm p = (T.symm p.1, p.2 + τ (T.symm p.1))

@[reducible]

def Oseledets.suspensionAddAction {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) : AddAction ℤ (X × ℝ)

The ℤ-action on X × ℝ generated by the suspension automorphism suspensionGen, defined as n +ᵥ p = ((suspensionGen) ^ n) p via the zpow of the underlying permutation. This is the suspension orbit relation: (x, s) is identified with (T x, s − τ x). The action laws zero_vadd and add_vadd are read off from zpow_zero and zpow_add in the permutation group.

This is bundled as a def rather than a global instance because it depends on the data T and hτ; it is activated locally (via letI) in the statements and proofs that use it. The bundled VAdd is available as (suspensionAddAction T hτ).toVAdd.

Equations

• Oseledets.suspensionAddAction T hτ = { vadd := fun (n : ℤ) (p : X × ℝ) => ((Oseledets.suspensionGen T hτ).toEquiv ^ n) p, add_vadd := ⋯, zero_vadd := ⋯ }

def Oseledets.suspensionAct {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℤ) (p : X × ℝ) : X × ℝ

The underlying function of the suspension ℤ-action, written without typeclass notation: suspensionAct T hτ n p = ((suspensionGen) ^ n) p. This agrees with the +ᵥ of suspensionAddAction (see suspension_vadd_eq_act). Using a plain function lets the structural lemmas be stated without activating the data-dependent AddAction instance.

Equations

• Oseledets.suspensionAct T hτ n p = ((Oseledets.suspensionGen T hτ).toEquiv ^ n) p

theorem Oseledets.suspension_vadd_eq_act {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℤ) (p : X × ℝ) : VAdd.vadd n p = suspensionAct T hτ n p

@[simp]

theorem Oseledets.suspensionAct_zero {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (p : X × ℝ) : suspensionAct T hτ 0 p = p

theorem Oseledets.suspensionAct_add {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (m n : ℤ) (p : X × ℝ) : suspensionAct T hτ (m + n) p = suspensionAct T hτ m (suspensionAct T hτ n p)

@[simp]

theorem Oseledets.suspensionAct_one {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (p : X × ℝ) : suspensionAct T hτ 1 p = (suspensionGen T hτ) p

@[simp]

theorem Oseledets.suspensionAct_neg_one {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (p : X × ℝ) : suspensionAct T hτ (-1) p = (suspensionGen T hτ).symm p

def Oseledets.roofSum {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℤ) (x : X) : ℝ

The signed (integer-indexed) Birkhoff sum τ⁽ⁿ⁾ of the roof function τ along T, defined as the drop in the ℝ-coordinate produced by suspensionAct n. For n ≥ 0 this is the ordinary Birkhoff sum τ x + τ (T x) + … + τ (Tⁿ⁻¹ x); for n < 0 it is its backward counterpart with a sign.

Equations

• Oseledets.roofSum T hτ n x = -(Oseledets.suspensionAct T hτ n (x, 0)).2

def Oseledets.baseIter {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℤ) (x : X) : X

The first coordinate of suspensionAct n (x, s), i.e. the n-th ℤ-iterate of T applied to x. It is independent of the ℝ-coordinate s.

Equations

• Oseledets.baseIter T hτ n x = (Oseledets.suspensionAct T hτ n (x, 0)).1

theorem Oseledets.suspensionAct_eq {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℤ) (x : X) (s : ℝ) : suspensionAct T hτ n (x, s) = (baseIter T hτ n x, s - roofSum T hτ n x)

Structural form of the action: suspensionAct n (x, s) = (baseIter n x, s − roofSum n x). The action translates the ℝ-coordinate by −roofSum n x, a quantity independent of s, and moves the X-coordinate by the ℤ-iterate of T.

theorem Oseledets.suspensionAct_snd {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℤ) (x : X) (s : ℝ) : (suspensionAct T hτ n (x, s)).2 = s - roofSum T hτ n x

theorem Oseledets.suspensionAct_fst {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℤ) (x : X) (s : ℝ) : (suspensionAct T hτ n (x, s)).1 = baseIter T hτ n x

@[simp]

theorem Oseledets.roofSum_zero {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (x : X) : roofSum T hτ 0 x = 0

theorem Oseledets.roofSum_add_one {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℤ) (x : X) : roofSum T hτ (n + 1) x = roofSum T hτ n x + τ (baseIter T hτ n x)

The roof-cocycle step: τ⁽ⁿ⁺¹⁾ x = τ⁽ⁿ⁾ x + τ (Tⁿ x), where Tⁿ x = baseIter n x.

theorem Oseledets.strictMono_roofSum {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (x : X) : StrictMono fun (n : ℤ) => roofSum T hτ n x

With inf τ ≥ c > 0, the roof sum strictly increases in the integer index.

theorem Oseledets.roofSum_ge {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c : ℝ} (hc : ∀ (x : X), c ≤ τ x) (x : X) (n : ℕ) : c * ↑n ≤ roofSum T hτ (↑n) x

Telescoping lower bound: for 0 ≤ n, the roof sum is at least c * n.

theorem Oseledets.roofSum_le_of_nonpos {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c : ℝ} (hc : ∀ (x : X), c ≤ τ x) (x : X) (n : ℕ) : roofSum T hτ (-↑n) x ≤ c * -↑↑n

Telescoping upper bound: for n ≤ 0, the roof sum is at most c * n (a negative quantity).

theorem Oseledets.tendsto_roofSum_atTop {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (x : X) : Filter.Tendsto (fun (n : ℤ) => roofSum T hτ n x) Filter.atTop Filter.atTop

theorem Oseledets.tendsto_roofSum_atBot {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (x : X) : Filter.Tendsto (fun (n : ℤ) => roofSum T hτ n x) Filter.atBot Filter.atBot

theorem Oseledets.exists_unique_lt_of_strictMono {a : ℤ → ℝ} (hmono : StrictMono a) (htop : Filter.Tendsto a Filter.atTop Filter.atTop) (hbot : Filter.Tendsto a Filter.atBot Filter.atBot) (s : ℝ) : ∃! n : ℤ, a n ≤ s ∧ s < a (n + 1)

A strictly monotone ℤ-indexed real sequence tending to +∞ along atTop and to −∞ along atBot partitions ℝ into the half-open intervals [a n, a (n+1)): every real s lies in exactly one of them. This is the pure real-analysis core of the suspension fundamental-domain result.

def Oseledets.suspensionDomain {X : Type u_1} (τ : X → ℝ) : Set (X × ℝ)

The half-open box under the roof, {p : X × ℝ | 0 ≤ p.2 ∧ p.2 < τ p.1}. It is the Ambrose–Kakutani cross-section of the suspension and a fundamental domain for the suspension ℤ-action with respect to μ × volume.

Equations

• Oseledets.suspensionDomain τ = {p : X × ℝ | 0 ≤ p.2 ∧ p.2 < τ p.1}

theorem Oseledets.measurableSet_suspensionDomain {X : Type u_1} [MeasurableSpace X] {τ : X → ℝ} (hτ : Measurable τ) : MeasurableSet (suspensionDomain τ)

theorem Oseledets.suspensionAct_mem_domain_iff {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℤ) (x : X) (s : ℝ) : suspensionAct T hτ n (x, s) ∈ suspensionDomain τ ↔ roofSum T hτ n x ≤ s ∧ s < roofSum T hτ (n + 1) x

Membership of suspensionAct n (x, s) in the box is equivalent to the half-open interval condition roofSum n x ≤ s < roofSum (n+1) x.

theorem Oseledets.suspension_exists_unique_act_mem {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (x : X) (s : ℝ) : ∃! n : ℤ, suspensionAct T hτ n (x, s) ∈ suspensionDomain τ

Every orbit meets the box exactly once. For each (x, s) there is a unique integer n with suspensionAct n (x, s) in the half-open box. This is the heart of the fundamental-domain property; it follows from the half-open-interval partition exists_unique_lt_of_strictMono applied to the strictly increasing, two-sided-unbounded sequence n ↦ roofSum n x.

theorem Oseledets.isAddFundamentalDomain_suspensionDomain {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {μ : MeasureTheory.Measure X} {c : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) : MeasureTheory.IsAddFundamentalDomain ℤ (suspensionDomain τ) (μ.prod MeasureTheory.volume)

The box is a fundamental domain. With inf τ ≥ c > 0 and T measure-preserving, the half-open box suspensionDomain τ is a fundamental domain for the suspension ℤ-action on X × ℝ with respect to μ × volume. This is the Ambrose–Kakutani cross-section structure of the suspension.

The action is the locally-activated suspensionAddAction T hτ; the statement uses letI to bring its VAdd instance into scope. The proof is IsAddFundamentalDomain.mk', whose sole content is the exactly-once meeting suspension_exists_unique_act_mem.