Cylinder Sets on Path Space

This file contains infrastructure for working with cylinder sets on path space (ℕ → α). Cylinder sets are fundamental objects in probability theory on sequence spaces, consisting of events determined by finitely many coordinates.

Main definitions

• cylinder r C: Standard cylinder on the first r coordinates starting at index 0
• firstRMap X r: Map collecting the first r coordinates of a process
• firstRCylinder X r C: Finite block cylinder event on the first r coordinates

Main results

• Measurability lemmas for cylinder types
• Extensionality properties (universal sets, intersections)
• Bridge lemmas connecting different cylinder formulations

def Exchangeability.PathSpace.cylinder {α : Type u_1} (r : ℕ) (C : Fin r → Set α) : Set (ℕ → α)

Standard cylinder on the first r coordinates starting at index 0.

Equations

• Exchangeability.PathSpace.cylinder r C = {f : ℕ → α | ∀ (i : Fin r), f ↑i ∈ C i}

theorem Exchangeability.PathSpace.cylinder_measurable {α : Type u_1} [MeasurableSpace α] {r : ℕ} {C : Fin r → Set α} (hC : ∀ (i : Fin r), MeasurableSet (C i)) : MeasurableSet (cylinder r C)

def Exchangeability.PathSpace.firstRMap {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (r : ℕ) : Ω → Fin r → α

The map collecting the first r coordinates.

Equations

• Exchangeability.PathSpace.firstRMap X r ω i = X (↑i) ω

@[reducible, inline]

abbrev Exchangeability.PathSpace.firstRSigma {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) (r : ℕ) : MeasurableSpace Ω

The σ‑algebra generated by the first r coordinates.

Equations

• Exchangeability.PathSpace.firstRSigma X r = MeasurableSpace.comap (Exchangeability.PathSpace.firstRMap X r) inferInstance

def Exchangeability.PathSpace.firstRCylinder {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (r : ℕ) (C : Fin r → Set α) : Set Ω

The finite block cylinder event on the first r coordinates.

Equations

• Exchangeability.PathSpace.firstRCylinder X r C = {ω : Ω | ∀ (i : Fin r), X (↑i) ω ∈ C i}

theorem Exchangeability.PathSpace.firstRCylinder_measurable_in_firstRSigma {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) (r : ℕ) (C : Fin r → Set α) (hC : ∀ (i : Fin r), MeasurableSet (C i)) : MeasurableSet (firstRCylinder X r C)

Measurable in the first-r σ‑algebra. If each C i is measurable in α, then the block cylinder is measurable in firstRSigma X r (no measurability assumptions on the X i are needed for this comap‑level statement).

theorem Exchangeability.PathSpace.firstRCylinder_measurable_ambient {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) (r : ℕ) (C : Fin r → Set α) (hX : ∀ (i : ℕ), Measurable (X i)) (hC : ∀ (i : Fin r), MeasurableSet (C i)) : MeasurableSet (firstRCylinder X r C)

Measurable in the ambient σ‑algebra. If each coordinate X i is measurable, then the block cylinder is measurable in the ambient σ‑algebra (useful for Integrable.indicator).

theorem Exchangeability.PathSpace.firstRSigma_le_ambient {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) (r : ℕ) (hX : ∀ (i : ℕ), Measurable (X i)) : firstRSigma X r ≤ inferInstance

The first-r σ-algebra is a sub-σ-algebra of the ambient σ-algebra when coordinates are measurable.