Measure-preservation of the suspension flow

This module supplies the measure-theoretic content that Oseledets.Continuous.SuspensionFlow deliberately deferred: the per-time measure-preservation of the suspension flow ζ_t on the suspension probability space, and its packaging as a MeasurePreservingFlow.

The descent argument runs through the fundamental domain. The suspension measure is the pushforward of μ × volume restricted to the half-open box 𝓕 = suspensionDomain τ along the quotient projection π = suspensionMk. The flow ζ_t descends from the vertical translation S t (x, s) = (x, s + t), which

• preserves ν = μ × volume (measurePreserving_translate), and
• commutes with the suspension ℤ-action (suspensionAct_translate),

so the image box S t '' 𝓕 is again a fundamental domain (image_of_equiv for fundamental domains). Pushing forward, (ζ_t)_* (ν|_𝓕 ↦ π) = (ν|_(S t '' 𝓕) ↦ π), and the fundamental-domain independence of the quotient measure (measure_set_eq applied to the saturated set π ⁻¹' U) identifies this with the original (ν|_𝓕 ↦ π). The normalising scalar passes through Measure.map_smul.

Main results

• Oseledets.suspensionTranslateEquiv: the vertical translation S t packaged as a measurable equivalence on X × ℝ (used to take measurable images of the fundamental domain).
• Oseledets.isAddFundamentalDomain_image_translate: the translated box S t '' 𝓕 is again a fundamental domain for the suspension ℤ-action.
• Oseledets.suspensionFlowMap_comp_mk: the descent commutation ζ_t ∘ π = π ∘ S t.
• Oseledets.map_suspensionFlowMap_suspensionMeasure₀: (ζ_t)_* μ̂₀ = μ̂₀ for the raw (unnormalised) suspension measure.
• Oseledets.measurePreserving_suspensionFlowMap: each ζ_t preserves the suspension probability measure suspensionMeasure.
• Oseledets.suspensionFlow: the suspension flow packaged as a MeasurePreservingFlow.

def Oseledets.suspensionTranslateEquiv {X : Type u_1} [MeasurableSpace X] (t : ℝ) : X × ℝ ≃ᵐ X × ℝ

The vertical translation S t (x, s) = (x, s + t) as a measurable equivalence on X × ℝ, with inverse S (-t). Bundling it as an equivalence lets us take measurable images of the fundamental domain and invoke the fundamental-domain transport lemma image_of_equiv.

Equations

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

@[simp]

theorem Oseledets.suspensionTranslateEquiv_apply {X : Type u_1} [MeasurableSpace X] (t : ℝ) (p : X × ℝ) : (suspensionTranslateEquiv t) p = suspensionTranslate t p

@[simp]

theorem Oseledets.suspensionTranslateEquiv_symm_apply {X : Type u_1} [MeasurableSpace X] (t : ℝ) (p : X × ℝ) : (suspensionTranslateEquiv t).symm p = suspensionTranslate (-t) p

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

The translated box S t '' 𝓕 is again a fundamental domain for the suspension ℤ-action with respect to μ × volume. It is the image of the fundamental box 𝓕 = suspensionDomain τ under the ν-preserving translation S t, which commutes with the action (suspensionAct_translate); IsAddFundamentalDomain.image_of_equiv transports the fundamental-domain property along such an equivalence.

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

Each integer iterate of the suspension action is measurable: it is a power of the measurable generator suspensionGen. Proved by induction on n from the measurability of the generator and its inverse.

theorem Oseledets.measurePreserving_suspensionAct {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {μ : MeasureTheory.Measure X} [MeasureTheory.SFinite μ] (hT : MeasureTheory.MeasurePreserving (⇑T) μ μ) (n : ℤ) : MeasureTheory.MeasurePreserving (suspensionAct T hτ n) (μ.prod MeasureTheory.volume) (μ.prod MeasureTheory.volume)

Each integer iterate of the suspension action preserves μ × volume: it is a power of the measure-preserving generator suspensionGen, so suspensionAct n preserves the product measure for every n : ℤ. Proved by induction on n from measurePreserving_suspensionGen and the measure-preservation of its inverse.

theorem Oseledets.measurableConstVAdd_suspension {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) : MeasurableConstVAdd ℤ (X × ℝ)

The suspension action has measurable constant translations: n +ᵥ · is measurable for each n : ℤ (it is the measurable power of the generator). Packaged as the MeasurableConstVAdd instance needed by the fundamental-domain quotient lemmas.

theorem Oseledets.vaddInvariantMeasure_suspension {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {μ : MeasureTheory.Measure X} [MeasureTheory.SFinite μ] (hT : MeasureTheory.MeasurePreserving (⇑T) μ μ) : MeasureTheory.VAddInvariantMeasure ℤ (X × ℝ) (μ.prod MeasureTheory.volume)

The product measure μ × volume is invariant under the suspension action: each suspensionAct n preserves it (measurePreserving_suspensionAct), so the preimage of any measurable set has the same measure. Packaged as the VAddInvariantMeasure instance needed by the fundamental-domain quotient lemmas.

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

The descent commutation ζ_t ∘ π = π ∘ S t: the suspension flow map composed with the quotient projection equals the projection of the vertical translation.

theorem Oseledets.map_restrict_image_translate_eq {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {μ : MeasureTheory.Measure X} [MeasureTheory.SFinite μ] (hT : MeasureTheory.MeasurePreserving (⇑T) μ μ) {c : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (t : ℝ) : MeasureTheory.Measure.map (suspensionMk T hτ) ((μ.prod MeasureTheory.volume).restrict (suspensionTranslate t '' suspensionDomain τ)) = MeasureTheory.Measure.map (suspensionMk T hτ) ((μ.prod MeasureTheory.volume).restrict (suspensionDomain τ))

Fundamental-domain independence of the raw quotient measure: pushing ν = μ × volume restricted to the translated box S t '' 𝓕 along the quotient projection gives the same measure as pushing it from the original box 𝓕. This is the additive quotientMeasure_eq, proved here inline from addMeasure_map_restrict_apply and the fundamental-domain set-measure equality measure_set_eq applied to the saturated set π ⁻¹' U.

theorem Oseledets.map_suspensionFlowMap_suspensionMeasure₀ {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {μ : MeasureTheory.Measure X} [MeasureTheory.SFinite μ] (hT : MeasureTheory.MeasurePreserving (⇑T) μ μ) {c : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (t : ℝ) : MeasureTheory.Measure.map (suspensionFlowMap T hτ t) (suspensionMeasure₀ T hτ μ) = suspensionMeasure₀ T hτ μ

The raw (unnormalised) suspension measure μ̂₀ is invariant under the suspension flow: (ζ_t)_* μ̂₀ = μ̂₀. Combining the descent commutation ζ_t ∘ π = π ∘ S t, the measure-preservation of S t, and the fundamental-domain independence map_restrict_image_translate_eq.

theorem Oseledets.measurePreserving_suspensionFlowMap {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {μ : MeasureTheory.Measure X} [MeasureTheory.SFinite μ] (hT : MeasureTheory.MeasurePreserving (⇑T) μ μ) {c : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (t : ℝ) : MeasureTheory.MeasurePreserving (suspensionFlowMap T hτ t) (suspensionMeasure T hτ μ) (suspensionMeasure T hτ μ)

Each suspension flow map preserves the suspension probability measure. With a measure-preserving base map T, a strictly positive integrable roof function τ (bounded below by c > 0), the descended flow ζ_t preserves suspensionMeasure.

The raw measure μ̂₀ is ζ_t-invariant (map_suspensionFlowMap_suspensionMeasure₀); the normalising scalar passes through Measure.map_smul.

def Oseledets.suspensionFlow {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {μ : MeasureTheory.Measure X} [MeasureTheory.SFinite μ] (hT : MeasureTheory.MeasurePreserving (⇑T) μ μ) {c : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) : MeasurePreservingFlow (suspensionMeasure T hτ μ)

The suspension flow as a measure-preserving flow. Packages the additive, measurable, measure-preserving family ζ_t into a MeasurePreservingFlow on the suspension probability space. The map_add' field uses φ (s + t) = φ s ∘ φ t (suspensionFlowMap_add).

Equations

• Oseledets.suspensionFlow T hτ hT hc hcpos = { toFun := Oseledets.suspensionFlowMap T hτ, map_zero' := ⋯, map_add' := ⋯, measurePreserving' := ⋯ }