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.

Originally extracted from MartingaleHelpers.lean for broader reusability.

Main definitions

• tailCylinder r C: Cylinder on the first r tail coordinates (shifted by one)
• cylinder r C: Standard cylinder on the first r coordinates starting at index 0
• finCylinder r C: Cylinder for functions with domain Fin r
• 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 all cylinder types
• Extensionality properties (universal sets, intersections)
• Bridge lemmas connecting different cylinder formulations

Implementation notes

This file is designed to be general-purpose infrastructure, not specific to any particular proof approach (martingale, Koopman, L²). It only imports mathlib and has no project dependencies.

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

Cylinder on the first r tail coordinates (shifted by one).

Equations

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

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

Basic measurability for tail cylinders.

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}

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

Cylinder for functions with domain Fin r.

Equations

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

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

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_eq_preimage_finCylinder {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (r : ℕ) (C : Fin r → Set α) : firstRCylinder X r C = firstRMap X r ⁻¹' finCylinder r C

As expected, the block cylinder is the preimage of a finite cylinder under the firstRMap.

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.measurable_firstRMap {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) (r : ℕ) (hX : ∀ (i : ℕ), Measurable (X i)) : Measurable (firstRMap X r)

The firstRMap is measurable when all coordinates are measurable.

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.

theorem Exchangeability.PathSpace.firstRSigma_mono {Ω : Type u_1} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) {r s : ℕ} (hrs : r ≤ s) : firstRSigma X r ≤ firstRSigma X s

Stronger version: firstRSigma increases with r.

@[simp]

theorem Exchangeability.PathSpace.firstRCylinder_zero {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (C : Fin 0 → Set α) : firstRCylinder X 0 C = Set.univ

The empty cylinder (r = 0) is the whole space.

theorem Exchangeability.PathSpace.mem_firstRCylinder_iff {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (r : ℕ) (C : Fin r → Set α) (ω : Ω) : ω ∈ firstRCylinder X r C ↔ ∀ (i : Fin r), X (↑i) ω ∈ C i

Cylinder membership characterization.

theorem Exchangeability.PathSpace.firstRCylinder_univ {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) (r : ℕ) : (firstRCylinder X r fun (x : Fin r) => Set.univ) = Set.univ

firstRCylinder on universal sets is the whole space.

theorem Exchangeability.PathSpace.firstRCylinder_inter {Ω : Type u_1} {α : Type u_2} (X : ℕ → Ω → α) {r : ℕ} {C D : Fin r → Set α} : firstRCylinder X r C ∩ firstRCylinder X r D = firstRCylinder X r fun (i : Fin r) => C i ∩ D i

Intersection of firstRCylinders equals coordinate-wise intersection.

theorem Exchangeability.PathSpace.tailCylinder_eq_preimage_cylinder {α : Type u_1} {r : ℕ} {C : Fin r → Set α} : tailCylinder r C = shift ⁻¹' cylinder r C

tailCylinder is the preimage of a standard cylinder under shift.

@[simp]

theorem Exchangeability.PathSpace.mem_cylinder_iff {α : Type u_1} {r : ℕ} {C : Fin r → Set α} {f : ℕ → α} : f ∈ cylinder r C ↔ ∀ (i : Fin r), f ↑i ∈ C i

@[simp]

theorem Exchangeability.PathSpace.mem_tailCylinder_iff {α : Type u_1} {r : ℕ} {C : Fin r → Set α} {f : ℕ → α} : f ∈ tailCylinder r C ↔ ∀ (i : Fin r), f (↑i + 1) ∈ C i

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

The cylinder set is measurable when each component set is measurable.

@[simp]

theorem Exchangeability.PathSpace.cylinder_zero {α : Type u_1} : (cylinder 0 fun (x : Fin 0) => Set.univ) = Set.univ

Empty cylinder is the whole space.

@[simp]

theorem Exchangeability.PathSpace.tailCylinder_zero' {α : Type u_1} : (tailCylinder 0 fun (x : Fin 0) => Set.univ) = Set.univ

Empty tail cylinder is the whole space.

theorem Exchangeability.PathSpace.cylinder_univ {α : Type u_1} {r : ℕ} : (cylinder r fun (x : Fin r) => Set.univ) = Set.univ

Cylinder on universal sets is the whole space.

theorem Exchangeability.PathSpace.tailCylinder_univ {α : Type u_1} {r : ℕ} : (tailCylinder r fun (x : Fin r) => Set.univ) = Set.univ

Tail cylinder on universal sets is the whole space.

theorem Exchangeability.PathSpace.cylinder_inter {α : Type u_1} {r : ℕ} {C D : Fin r → Set α} : cylinder r C ∩ cylinder r D = cylinder r fun (i : Fin r) => C i ∩ D i

Cylinders form intersections coordinate-wise.