The suspension quotient space and its invariant probability measure

This module assembles the suspension (mapping-torus) measure space from the fundamental-domain keystone of Oseledets.Continuous.Suspension and the measure facts of Oseledets.Continuous.SuspensionMeasure. The suspension space is the quotient of X × ℝ by the suspension ℤ-action G (x, s) = (T x, s − τ x), i.e. the mapping torus of the base map T under the roof function τ.

Construction

The suspension space is the orbit quotient

SuspensionSpace T hτ := Quotient (AddAction.orbitRel ℤ (X × ℝ)),

for the action suspensionAddAction T hτ of Oseledets.Continuous.Suspension. As a Quotient it carries the canonical pushforward MeasurableSpace instance for free.

Its measure is built by restricting μ × volume to the fundamental box suspensionDomain τ and pushing forward along the quotient map π = Quotient.mk:

suspensionMeasure₀ := ((μ × volume).restrict (suspensionDomain τ)).map π.

The total mass of this raw measure equals ENNReal.ofReal (∫ x, τ x ∂μ) (the box mass, since π is surjective so π ⁻¹' univ = univ). Normalising by (∫ τ)⁻¹ produces the invariant probability measure suspensionMeasure.

Main definitions

• Oseledets.SuspensionSpace: the suspension quotient Quotient (AddAction.orbitRel ℤ (X × ℝ)).
• Oseledets.suspensionMeasure₀: the raw pushforward measure (restrict box).map π.
• Oseledets.suspensionMeasure: the normalised invariant probability measure (∫ τ)⁻¹ • suspensionMeasure₀.

Main results

• Oseledets.suspensionMeasure₀_univ: suspensionMeasure₀ univ = ENNReal.ofReal (∫ x, τ x ∂μ).
• Oseledets.isProbabilityMeasure_suspensionMeasure: with 0 < ∫ τ and Integrable τ, the normalised measure suspensionMeasure is a probability measure.

What is not in this file

The per-time measure-preservation of the suspension flow ζ_t [x, s] = [x, s + t] through the quotient — the descent of the ℝ-translation via the fundamental domain (the IsAddFundamentalDomain.measurePreserving_quotient-style argument) and its packaging as a MeasurePreservingFlow — is left to a follow-up module. Establishing it requires transporting the fundamental-domain measure-preservation of the ℝ-translation through the quotient map, which is a separate piece of infrastructure. This file stops at the invariant probability measure, which is self-contained and sorry-free.

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

The suspension (mapping-torus) space of the base map T under the roof function τ: the orbit quotient of X × ℝ by the suspension ℤ-action G (x, s) = (T x, s − τ x).

The action is the locally-activated suspensionAddAction T hτ of Oseledets.Continuous.Suspension; it is brought into scope by letI so that AddAction.orbitRel ℤ (X × ℝ) is the suspension orbit relation. As a Quotient the space carries the canonical pushforward MeasurableSpace instance.

Equations

• Oseledets.SuspensionSpace T hτ = Quotient (AddAction.orbitRel ℤ (X × ℝ))

@[implicit_reducible]

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

The canonical MeasurableSpace on the suspension space, pushed forward from X × ℝ along the quotient map. This is Quotient.instMeasurableSpace for the suspension orbit relation.

Equations

• Oseledets.instMeasurableSpaceSuspensionSpace T hτ = inferInstance

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

The quotient projection π : X × ℝ → SuspensionSpace T hτ, π p = [p].

Equations

• Oseledets.suspensionMk T hτ p = ⟦p⟧

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

The quotient projection suspensionMk is measurable (it is Quotient.mk, which is measurable for the pushforward MeasurableSpace on the quotient).

noncomputable def Oseledets.suspensionMeasure₀ {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (μ : MeasureTheory.Measure X) : MeasureTheory.Measure (SuspensionSpace T hτ)

The raw suspension measure: restrict the product measure μ × volume to the fundamental box suspensionDomain τ and push it forward along the quotient projection suspensionMk. Its normalisation (see suspensionMeasure) is the suspension's invariant probability measure.

Equations

• Oseledets.suspensionMeasure₀ T hτ μ = MeasureTheory.Measure.map (Oseledets.suspensionMk T hτ) ((μ.prod MeasureTheory.volume).restrict (Oseledets.suspensionDomain τ))

theorem Oseledets.suspensionMeasure₀_univ_eq_measure_box {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (μ : MeasureTheory.Measure X) : (suspensionMeasure₀ T hτ μ) Set.univ = (μ.prod MeasureTheory.volume) (suspensionDomain τ)

The total mass of the raw suspension measure equals the box mass (μ × volume) (box).

The quotient map π is total, so π ⁻¹' univ = univ; hence ((restrict box).map π) univ = (restrict box) univ = (μ × volume) box by Measure.map_apply and Measure.restrict_apply_univ.

theorem Oseledets.suspensionMeasure₀_univ {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (μ : MeasureTheory.Measure X) [MeasureTheory.SFinite μ] (hτ_nonneg : ∀ (x : X), 0 ≤ τ x) (hτ_int : MeasureTheory.Integrable τ μ) : (suspensionMeasure₀ T hτ μ) Set.univ = ENNReal.ofReal (∫ (x : X), τ x ∂μ)

The total mass of the raw suspension measure equals ENNReal.ofReal (∫ x, τ x ∂μ), for a nonnegative integrable roof function τ. This is the box mass measure_suspensionDomain pushed through the quotient.

noncomputable def Oseledets.suspensionMeasure {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (μ : MeasureTheory.Measure X) : MeasureTheory.Measure (SuspensionSpace T hτ)

The suspension invariant probability measure: the raw measure suspensionMeasure₀ normalised by the reciprocal of its total mass (∫ τ)⁻¹. When 0 < ∫ τ (so the mass is positive) and τ is integrable (so the mass is finite), this is a probability measure (isProbabilityMeasure_suspensionMeasure).

Equations

• Oseledets.suspensionMeasure T hτ μ = (ENNReal.ofReal (∫ (x : X), τ x ∂μ))⁻¹ • Oseledets.suspensionMeasure₀ T hτ μ

theorem Oseledets.suspensionMeasure_univ {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (μ : MeasureTheory.Measure X) [MeasureTheory.SFinite μ] (hτ_nonneg : ∀ (x : X), 0 ≤ τ x) (hτ_int : MeasureTheory.Integrable τ μ) (hτ_pos : 0 < ∫ (x : X), τ x ∂μ) : (suspensionMeasure T hτ μ) Set.univ = 1

The suspension invariant probability measure has total mass 1: with 0 < ∫ τ (positive mass) and τ integrable (finite mass), (∫ τ)⁻¹ • suspensionMeasure₀ evaluates to 1 on univ via ENNReal.inv_mul_cancel.

theorem Oseledets.isProbabilityMeasure_suspensionMeasure {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (μ : MeasureTheory.Measure X) [MeasureTheory.SFinite μ] (hτ_nonneg : ∀ (x : X), 0 ≤ τ x) (hτ_int : MeasureTheory.Integrable τ μ) (hτ_pos : 0 < ∫ (x : X), τ x ∂μ) : MeasureTheory.IsProbabilityMeasure (suspensionMeasure T hτ μ)

With 0 < ∫ τ and τ integrable, the normalised suspensionMeasure is a probability measure.