Measure-preservation for the suspension construction

This module supplies the measure-theoretic infrastructure that the suspension (mapping-torus) construction of Oseledets.Continuous.Suspension deliberately deferred: the fact that the generating automorphism of the suspension ℤ-action preserves the product measure μ × volume.

The key new ingredient is the shear map (x, s) ↦ (x, s − τ x). It is a fibered translation: on each fibre {x} × ℝ it is the translation s ↦ s − τ x, which preserves Lebesgue measure because volume on ℝ is right-invariant. Assembling the fibrewise translations via the skew-product Fubini lemma MeasureTheory.MeasurePreserving.skew_product shows the shear preserves μ × volume. The generating automorphism suspensionGen T hτ : (x, s) ↦ (T x, s − τ x) is then the same skew product over the base map T, so it preserves μ × volume whenever T does.

Main results

• Oseledets.measurePreserving_shear: the shear (x, s) ↦ (x, s − τ x) preserves μ × volume.
• Oseledets.measurePreserving_suspensionGen: the generator suspensionGen T hτ preserves μ × volume, given MeasurePreserving T μ μ.
• Oseledets.suspensionDomain_fiber: the x-fibre of the box is the half-open interval Ico 0 (τ x).
• Oseledets.measure_suspensionDomain: the box mass equals ENNReal.ofReal (∫ x, τ x ∂μ) for a nonnegative integrable roof function τ.

These are the measure facts from which the suspension's invariant probability measure (μ × volume)|_box / ∫ τ and the per-time measure-preservation of the suspension flow are subsequently built.

theorem Oseledets.measurePreserving_shear {X : Type u_1} [MeasurableSpace X] {τ : X → ℝ} (hτ : Measurable τ) (μ : MeasureTheory.Measure X) [MeasureTheory.SFinite μ] : MeasureTheory.MeasurePreserving (fun (p : X × ℝ) => (p.1, p.2 - τ p.1)) (μ.prod MeasureTheory.volume) (μ.prod MeasureTheory.volume)

The shear map (x, s) ↦ (x, s − τ x) preserves the product measure μ × volume.

It is a fibered translation: on each fibre {x} × ℝ it is the Lebesgue-measure-preserving translation s ↦ s − τ x (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.measurePreserving_suspensionGen {X : Type u_1} [MeasurableSpace X] {τ : X → ℝ} (hτ : Measurable τ) {μ : MeasureTheory.Measure X} [MeasureTheory.SFinite μ] {T : X ≃ᵐ X} (hT : MeasureTheory.MeasurePreserving (⇑T) μ μ) : MeasureTheory.MeasurePreserving (⇑(suspensionGen T hτ)) (μ.prod MeasureTheory.volume) (μ.prod MeasureTheory.volume)

The suspension generator suspensionGen T hτ : (x, s) ↦ (T x, s − τ x) preserves the product measure μ × volume, given that the base map T preserves μ.

It is the skew product over T whose fibre translation is s ↦ s − τ x; equivalently, the shear measurePreserving_shear followed by the base move (x, s) ↦ (T x, s).

theorem Oseledets.suspensionDomain_fiber {X : Type u_1} {τ : X → ℝ} (x : X) : Prod.mk x ⁻¹' suspensionDomain τ = Set.Ico 0 (τ x)

The x-fibre of the box under the roof is the half-open interval Ico 0 (τ x): {s : ℝ | (x, s) ∈ suspensionDomain τ} = Ico 0 (τ x).

theorem Oseledets.measure_suspensionDomain {X : Type u_1} [MeasurableSpace X] {τ : X → ℝ} {μ : MeasureTheory.Measure X} [MeasureTheory.SFinite μ] (hτ : Measurable τ) (hτ_nonneg : ∀ (x : X), 0 ≤ τ x) (hτ_int : MeasureTheory.Integrable τ μ) : (μ.prod MeasureTheory.volume) (suspensionDomain τ) = ENNReal.ofReal (∫ (x : X), τ x ∂μ)

The mass of the box under the roof equals ENNReal.ofReal (∫ x, τ x ∂μ), for a nonnegative integrable roof function τ. This is the normalising constant for the suspension's invariant probability measure.

The proof is Fubini: the x-fibre of the box is Ico 0 (τ x), whose Lebesgue measure is ENNReal.ofReal (τ x) (as 0 ≤ τ x), and ∫⁻ x, ofReal (τ x) ∂μ = ofReal (∫ x, τ x ∂μ) for a nonnegative integrable function.