The constant-roof suspension space is standard Borel

This module proves that the suspension (mapping-torus) space of a standard Borel base map under the constant roof τ ≡ 1 is again a standard Borel space, and specialises this to the constant-roof Bernoulli suspension SuspensionSpace biShiftEquiv measurable_oneRoof over a standard Borel alphabet.

A quotient by a group action carries the pushforward (coinduced) MeasurableSpace, which is not automatically standard Borel. We obtain the property honestly, through the Ambrose–Kakutani fundamental domain: for τ ≡ 1 the box under the roof is X × [0, 1), and the quotient projection restricted to it is a measurable bijection. Concretely we build the measurable equivalence

SuspensionSpace T hτ ≃ᵐ X × ↥(Set.Ico (0 : ℝ) 1),

whose forward map is the orbit-invariant fundamental-domain coordinate [x, s] ↦ (baseIter ⌊s⌋ x, Int.fract s) and whose inverse is (x, t) ↦ [x, t]. Standard Borelness is then transported across this equivalence (standardBorelSpace_of_measurableEquiv, pulling back the Polish topology along the equivalence), using that ↥(Set.Ico (0 : ℝ) 1) is standard Borel (a measurable subset of ℝ) and that products of standard Borel spaces are standard Borel.

Main definitions

• Oseledets.suspensionUnitCoord: the raw fundamental-domain coordinate (x, s) ↦ (baseIter ⌊s⌋ x, Int.fract s) on X × ℝ.
• Oseledets.suspensionUnitFwd / Oseledets.suspensionUnitInv: the two directions of the fundamental-domain coordinate bijection.
• Oseledets.suspensionUnitMeasurableEquiv: the measurable equivalence SuspensionSpace T hτ ≃ᵐ X × ↥(Set.Ico (0 : ℝ) 1) for the constant roof.

Main results

• Oseledets.standardBorelSpace_of_measurableEquiv: a measurable equivalence transports StandardBorelSpace.
• Oseledets.standardBorelSpace_suspensionSpace_const_roof: for τ ≡ 1 and a standard Borel base, the suspension space is standard Borel.
• Oseledets.Multifractal.instStandardBorelSpace_suspensionSpace_bern: the constant-roof Bernoulli suspension space SuspensionSpace biShiftEquiv measurable_oneRoof is standard Borel (for a standard Borel alphabet α₀).

theorem Oseledets.standardBorelSpace_of_measurableEquiv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [hβ : StandardBorelSpace β] (e : α ≃ᵐ β) : StandardBorelSpace α

A measurable equivalence transports StandardBorelSpace. If e : α ≃ᵐ β and β is a standard Borel space, then so is α: pull back a compatible Polish topology along e (the induced topology), under which e is a topological embedding, so α is Polish and its measurable space is the Borel σ-algebra.

noncomputable def Oseledets.suspensionUnitCoord {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (p : X × ℝ) : X × ↑(Set.Ico 0 1)

The raw fundamental-domain coordinate on X × ℝ: the first coordinate of the fundamental-domain representative, baseIter ⌊s⌋ x, paired with the fractional height Int.fract s ∈ [0, 1). For the constant roof τ ≡ 1 this descends through the suspension orbit quotient (suspensionUnitFwd).

Equations

• Oseledets.suspensionUnitCoord T hτ p = (Oseledets.Multifractal.suspensionBaseProjRaw T hτ p, ⟨Int.fract p.2, ⋯⟩)

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

The raw fundamental-domain coordinate is measurable: its first component is the measurable raw base projection and its second is the measurable fractional part landing in the interval subtype.

theorem Oseledets.roofSum_oneRoof {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (hτ1 : τ = fun (x : X) => 1) (n : ℤ) (x : X) : roofSum T hτ n x = ↑n

For the constant roof τ ≡ 1, the signed roof Birkhoff sum is the index: τ⁽ⁿ⁾ x = n.

theorem Oseledets.suspensionUnitCoord_gen {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (hτ1 : τ = fun (x : X) => 1) (p : X × ℝ) : suspensionUnitCoord T hτ ((suspensionGen T hτ) p) = suspensionUnitCoord T hτ p

For the constant roof τ ≡ 1, the raw fundamental-domain coordinate is invariant under the suspension orbit generator G (x, s) = (T x, s − 1). The first coordinate is invariant by suspensionBaseProjRaw_gen; the second because Int.fract (s − 1) = Int.fract s.

theorem Oseledets.suspensionUnitCoord_gen_symm {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (hτ1 : τ = fun (x : X) => 1) (p : X × ℝ) : suspensionUnitCoord T hτ ((suspensionGen T hτ).symm p) = suspensionUnitCoord T hτ p

The same invariance under the inverse generator, obtained from suspensionUnitCoord_gen.

theorem Oseledets.suspensionUnitCoord_act {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (hτ1 : τ = fun (x : X) => 1) (n : ℤ) (p : X × ℝ) : suspensionUnitCoord T hτ (suspensionAct T hτ n p) = suspensionUnitCoord T hτ p

For the constant roof τ ≡ 1, the raw fundamental-domain coordinate is invariant under every power of the suspension orbit generator, i.e. along the whole ℤ-action.

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

The quotient projection identifies a point with each of its translates along the action: [suspensionAct n p] = [p].

theorem Oseledets.suspensionMk_unitCoord {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (hτ1 : τ = fun (x : X) => 1) (x : X) (s : ℝ) : suspensionMk T hτ (baseIter T hτ ⌊s⌋ x, Int.fract s) = suspensionMk T hτ (x, s)

The fundamental-domain representative (baseIter ⌊s⌋ x, Int.fract s) lies in the same orbit as (x, s) (for the constant roof), so they have the same quotient class.

noncomputable def Oseledets.suspensionUnitFwd {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (hτ1 : τ = fun (x : X) => 1) : SuspensionSpace T hτ → X × ↑(Set.Ico 0 1)

The forward fundamental-domain map [x, s] ↦ (baseIter ⌊s⌋ x, Int.fract s), the descent of the orbit-invariant raw coordinate suspensionUnitCoord through the suspension orbit quotient (for the constant roof τ ≡ 1).

Equations

• Oseledets.suspensionUnitFwd T hτ hτ1 = Quotient.lift (Oseledets.suspensionUnitCoord T hτ) ⋯

@[simp]

theorem Oseledets.suspensionUnitFwd_mk {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (hτ1 : τ = fun (x : X) => 1) (p : X × ℝ) : suspensionUnitFwd T hτ hτ1 (suspensionMk T hτ p) = suspensionUnitCoord T hτ p

The descent identity: suspensionUnitFwd [p] = suspensionUnitCoord p.

theorem Oseledets.measurable_suspensionUnitFwd {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (hτ1 : τ = fun (x : X) => 1) : Measurable (suspensionUnitFwd T hτ hτ1)

The forward fundamental-domain map is measurable (measurability out of the quotient is measurability of the composite with the projection, which is suspensionUnitCoord).

def Oseledets.suspensionUnitInv {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (y : X × ↑(Set.Ico 0 1)) : SuspensionSpace T hτ

The inverse fundamental-domain map (x, t) ↦ [x, t], embedding the fundamental domain X × [0, 1) into the suspension quotient.

Equations

• Oseledets.suspensionUnitInv T hτ y = Oseledets.suspensionMk T hτ (y.1, ↑y.2)

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

The inverse fundamental-domain map is measurable.

theorem Oseledets.suspensionUnitInv_fwd {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (hτ1 : τ = fun (x : X) => 1) (q : SuspensionSpace T hτ) : suspensionUnitInv T hτ (suspensionUnitFwd T hτ hτ1 q) = q

suspensionUnitInv is a left inverse of suspensionUnitFwd: the fundamental-domain representative of a class lies in the same class.

theorem Oseledets.suspensionUnitFwd_inv {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (hτ1 : τ = fun (x : X) => 1) (y : X × ↑(Set.Ico 0 1)) : suspensionUnitFwd T hτ hτ1 (suspensionUnitInv T hτ y) = y

suspensionUnitInv is a right inverse of suspensionUnitFwd: on the fundamental domain X × [0, 1) the floor is 0 and the fractional part is the identity.

noncomputable def Oseledets.suspensionUnitMeasurableEquiv {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) (hτ1 : τ = fun (x : X) => 1) : SuspensionSpace T hτ ≃ᵐ X × ↑(Set.Ico 0 1)

The fundamental-domain measurable equivalence for the constant roof τ ≡ 1: SuspensionSpace T hτ ≃ᵐ X × ↥(Set.Ico (0 : ℝ) 1), with forward map the orbit-invariant fundamental-domain coordinate and inverse the quotient embedding of the box.

Equations

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

theorem Oseledets.standardBorelSpace_suspensionSpace_const_roof {X : Type u_1} [MeasurableSpace X] (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) [StandardBorelSpace X] (hτ1 : τ = fun (x : X) => 1) : StandardBorelSpace (SuspensionSpace T hτ)

The constant-roof suspension of a standard Borel base is standard Borel. For τ ≡ 1 the suspension space is measurably equivalent to X × ↥(Set.Ico (0 : ℝ) 1) (the fundamental domain), which is standard Borel (a product of a standard Borel space with a measurable subset of ℝ); standard Borelness transports across the equivalence.

instance Oseledets.Multifractal.instStandardBorelSpace_suspensionSpace_bern {α₀ : Type u_1} [MeasurableSpace α₀] [StandardBorelSpace α₀] : StandardBorelSpace (SuspensionSpace biShiftEquiv ⋯)

The constant-roof Bernoulli suspension space is standard Borel. For a standard Borel alphabet α₀, the two-sided shift base BiShift α₀ = (ℤ → α₀) is standard Borel (a countable product), so the constant-roof (τ ≡ 1) suspension space SuspensionSpace biShiftEquiv measurable_oneRoof is standard Borel by standardBorelSpace_suspensionSpace_const_roof.