Documentation

Oseledets.Continuous.SuspensionQuotientImage

Measurability of quotient images: discharging the suspension exponent hmeas #

This module discharges the quotient-image measurability hypothesis hmeas carried as an explicit input by Oseledets.ae_suspensionMeasure_hasFlowExponent (Oseledets.Continuous.SuspensionSpaceExponentValue). That hypothesis asks that the image under the quotient projection suspensionMk of a measurable base set is a MeasurableSet in the suspension space SuspensionSpace T hτ. We prove this unconditionally from the measurable structure of the orbit quotient, following the special-flow / mapping-torus model of Cornfeld–Fomin–Sinai, Ergodic Theory (Springer 1982), Ch. 11 (special/suspension flows; Ambrose–Kakutani).

Construction #

The suspension space carries the canonical coinduced measurable structure of an orbit quotient: a set U in SuspensionSpace T hτ is measurable iff its preimage suspensionMk ⁻¹' U is measurable (measurableSet_quotient). For an image U = suspensionMk '' S, the preimage is the orbit-saturation

suspensionMk ⁻¹' (suspensionMk '' S) = ⋃ n : ℤ, suspensionAct T hτ n '' S

(AddAction.quotient_preimage_image_eq_union_add for the suspension orbit relation), a countable union over ℤ. Each translate suspensionAct T hτ n '' S is measurable because suspensionAct n is a measurable equivalence (suspensionActEquiv, with measurable inverse suspensionAct (-n)), so the saturation is measurable and the image is measurable.

Main results #

gap #

This is the unconditional measurability fact closing the explicit hmeas hypothesis of ae_suspensionMeasure_hasFlowExponent; it does not itself re-derive that exponent theorem (the statement still takes hmeas as an input — measurableSet_suspensionMk_exponent_image is the term one supplies for it). No invariance or a.e.-statement is asserted here beyond the pure measurability of the quotient image.

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

The suspension action suspensionAct T hτ n packaged as a measurable equivalence of X × ℝ. Its inverse is suspensionAct T hτ (-n): the two compose to suspensionAct 0 = id via the cocycle identity suspensionAct_add and suspensionAct_zero. Both directions are measurable by measurable_suspensionAct.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Oseledets.suspensionActEquiv_apply {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℤ) (p : X × ℝ) :
    (suspensionActEquiv T hτ n) p = suspensionAct T hτ n p
    source
    theorem Oseledets.measurableSet_suspensionAct_image {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (n : ℤ) {S : Set (X × ℝ)} (hS : MeasurableSet S) :
    MeasurableSet (suspensionAct T hτ n '' S)

    The image of a measurable set under the suspension action suspensionAct T hτ n is measurable: suspensionAct n is a measurable equivalence (suspensionActEquiv), hence a measurable embedding, so it preserves measurability of images.

    source
    theorem Oseledets.preimage_image_suspensionMk {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (S : Set (X × ℝ)) :
    suspensionMk T hτ ⁻¹' suspensionMk T hτ '' S = ⋃ (n : ℤ), suspensionAct T hτ n '' S

    The orbit-saturation identity. The preimage under the quotient projection suspensionMk of the image suspensionMk '' S is the orbit-saturation of S: the countable union of the translates suspensionAct T hτ n '' S over n : ℤ. This is AddAction.quotient_preimage_image_eq_union_add for the suspension orbit relation, rewritten with suspensionAct = (n +ᵥ ·).

    source
    theorem Oseledets.measurableSet_suspensionMk_image {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {S : Set (X × ℝ)} (hS : MeasurableSet S) :
    MeasurableSet (suspensionMk T hτ '' S)

    General quotient-image measurability. The image under the quotient projection suspensionMk of a measurable set S in X × ℝ is a MeasurableSet in the suspension space.

    A set in the orbit quotient is measurable iff its suspensionMk-preimage is measurable (measurableSet_quotient, the coinduced structure). For suspensionMk '' S that preimage is the orbit-saturation ⋃ n : ℤ, suspensionAct n '' S (preimage_image_suspensionMk), a countable union of measurable translates (measurableSet_suspensionAct_image), hence measurable.

    source
    theorem Oseledets.measurableSet_suspensionMk_exponent_image {X : Type u_1} [MeasurableSpace X] {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c : ℝ} (μ : MeasureTheory.Measure X) {lam : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (hPmeas : MeasurableSet {x : X | Filter.Tendsto (fun (t : ℝ) => Real.log ‖coverCocycle A T hτ hc hcpos (x, 0) t‖ / t) Filter.atTop (nhds (lam / ∫ (y : X), τ y ∂μ))}) :
    MeasurableSet {q : SuspensionSpace T hτ | ∃ (p : X × ℝ), suspensionMk T hτ p = q ∧ Filter.Tendsto (fun (t : ℝ) => Real.log ‖coverCocycle A T hτ hc hcpos (p.1, 0) t‖ / t) Filter.atTop (nhds (lam / ∫ (y : X), τ y ∂μ))}

    Discharging hmeas. The lifted exponent set of ae_suspensionMeasure_hasFlowExponent,

    {q | ∃ p, suspensionMk p = q ∧ <section exponent at p.1>},

    is exactly the image under suspensionMk of the base exponent set {p : X × ℝ | <section exponent at p.1>}; that base set is the measurable cylinder over the base exponent set hPmeas (it ignores the ℝ-coordinate), so its quotient image is measurable by measurableSet_suspensionMk_image. This is the MeasurableSet term one supplies for the hmeas hypothesis of ae_suspensionMeasure_hasFlowExponent.