The suspension flow

This module builds the natural one-parameter flow on the suspension (mapping-torus) space of Oseledets.Continuous.SuspensionSpace. On the product X × ℝ the flow is the ℝ-translation in the second (time) coordinate,

S t (x, s) = (x, s + t),

and the suspension flow ζ_t is its descent through the orbit quotient: ζ_t [x, s] = [x, s + t].

The descent is well-defined because S t commutes with the suspension ℤ-action: the generator G (x, s) = (T x, s − τ x) moves the first coordinate by T and subtracts a roof value from the second, while S t only adds t to the second coordinate, so the two operations on the second coordinate (subtracting roofSum n x, adding t) commute. Concretely suspensionAct n (S t p) = S t (suspensionAct n p) (suspensionAct_translate), which sends one orbit onto another and makes ζ_t well-defined on the quotient.

Main definitions

• Oseledets.suspensionTranslate: the ℝ-translation S t (x, s) = (x, s + t) on X × ℝ.
• Oseledets.suspensionFlowMap: the descended time-t map ζ_t on the suspension space.

Main results

• Oseledets.measurePreserving_translate: S t preserves μ × volume (fibrewise translation invariance of Lebesgue measure).
• Oseledets.suspensionAct_translate: the commutation suspensionAct n (S t p) = S t (suspensionAct n p) of the action with the translation — the well-definedness core.
• Oseledets.suspensionFlowMap_mk: the descent identity ζ_t [p] = [S t p].
• Oseledets.suspensionFlowMap_zero: ζ_0 = id.
• Oseledets.suspensionFlowMap_add: ζ_(s+t) = ζ_s ∘ ζ_t.
• Oseledets.measurable_suspensionFlowMap: each ζ_t is measurable.

What is not in this file

The per-time measure-preservation of the suspension flow, MeasurePreserving (suspensionFlowMap t) suspensionMeasure suspensionMeasure, and its packaging as a MeasurePreservingFlow, are deliberately left to a follow-up module. Establishing them requires transporting the fundamental-domain measure-preservation of the ℝ-translation through the quotient map (an IsAddFundamentalDomain/Measure.map argument), which is a separate piece of infrastructure. This file stops at the well-defined, additive, measurable flow maps, which are self-contained and sorry-free.

def Oseledets.suspensionTranslate {X : Type u_1} (t : ℝ) (p : X × ℝ) : X × ℝ

The ℝ-translation in the time coordinate, S t (x, s) = (x, s + t). This is the lift to X × ℝ of the suspension flow; its descent through the orbit quotient is suspensionFlowMap.

Equations

• Oseledets.suspensionTranslate t p = (p.1, p.2 + t)

@[simp]

theorem Oseledets.suspensionTranslate_apply {X : Type u_1} (t : ℝ) (p : X × ℝ) : suspensionTranslate t p = (p.1, p.2 + t)

@[simp]

theorem Oseledets.suspensionTranslate_zero {X : Type u_1} (p : X × ℝ) : suspensionTranslate 0 p = p

theorem Oseledets.suspensionTranslate_add {X : Type u_1} (s t : ℝ) (p : X × ℝ) : suspensionTranslate (s + t) p = suspensionTranslate s (suspensionTranslate t p)

theorem Oseledets.measurable_suspensionTranslate {X : Type u_1} [MeasurableSpace X] (t : ℝ) : Measurable (suspensionTranslate t)

theorem Oseledets.measurePreserving_translate {X : Type u_1} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.SFinite μ] (t : ℝ) : MeasureTheory.MeasurePreserving (suspensionTranslate t) (μ.prod MeasureTheory.volume) (μ.prod MeasureTheory.volume)

The translation S t (x, s) = (x, s + t) preserves the product measure μ × volume.

It is a fibered translation: on each fibre {x} × ℝ it is the Lebesgue-measure-preserving translation s ↦ s + t (right-invariance of volume on ℝ). The skew-product Fubini lemma MeasureTheory.MeasurePreserving.skew_product over the identity base map assembles these into the product-measure statement.

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

The suspension ℤ-action commutes with the ℝ-translation: suspensionAct n (S t p) = S t (suspensionAct n p). The action subtracts roofSum n x (a quantity independent of the time coordinate) from the time coordinate and moves the base coordinate by the iterate of T; the translation adds t to the time coordinate; these two operations on the time coordinate commute. This is the key fact making the descended flow well-defined on the quotient.

theorem Oseledets.suspensionTranslate_orbitRel {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (t : ℝ) (p q : X × ℝ) (hpq : (AddAction.orbitRel ℤ (X × ℝ)) p q) : suspensionMk T hτ (suspensionTranslate t p) = suspensionMk T hτ (suspensionTranslate t q)

The ℝ-translation S t respects the suspension orbit relation: if p and q are in the same ℤ-orbit then so are S t p and S t q, with the same integer witness, by the commutation suspensionAct_translate. This is the well-definedness obligation for the descended map suspensionMk ∘ S t, phrased so that ≈ is the suspension orbit relation in scope.

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

The suspension flow map ζ_t : Xᵗ → Xᵗ, the descent of the ℝ-translation S t through the orbit quotient: ζ_t [p] = [S t p]. It is well-defined by suspensionTranslate_orbitRel.

Equations

• Oseledets.suspensionFlowMap T hτ t = Quotient.lift (fun (p : X × ℝ) => Oseledets.suspensionMk T hτ (Oseledets.suspensionTranslate t p)) ⋯

@[simp]

theorem Oseledets.suspensionFlowMap_mk {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (t : ℝ) (p : X × ℝ) : suspensionFlowMap T hτ t (suspensionMk T hτ p) = suspensionMk T hτ (suspensionTranslate t p)

The descent identity: ζ_t [p] = [S t p].

@[simp]

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

The time-zero flow map is the identity: ζ_0 = id.

theorem Oseledets.suspensionFlowMap_add {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (s t : ℝ) : suspensionFlowMap T hτ (s + t) = suspensionFlowMap T hτ s ∘ suspensionFlowMap T hτ t

The flow maps are additive in time: ζ_(s+t) = ζ_s ∘ ζ_t.

theorem Oseledets.measurable_suspensionFlowMap {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (t : ℝ) : Measurable (suspensionFlowMap T hτ t)

Each suspension flow map ζ_t is measurable: it is the descent of the measurable translation S t, and measurability out of a quotient is measurability of the composite with the quotient map (measurable_from_quotient), which here equals suspensionMk ∘ S t.