Bridge: Path Space Measure and Shift Preservation

This file provides the path space measure μ_path and proves that contractability implies the shift map is measure-preserving on path space.

Main definitions

• pathify X: Factor map ω ↦ (n ↦ X n ω) from sample space to path space
• μ_path μ X: Law of process X as a measure on path space

Main results

• contractable_shift_invariant_law: Contractability implies shift-invariant law
• measurePreserving_shift_path: Packages above as MeasurePreserving for MET

Path Space and Factor Map

@[reducible, inline]

abbrev Exchangeability.Bridge.PathSpace (α : Type u_1) : Type u_1

Path space for a type α

Equations

• Exchangeability.Bridge.PathSpace α = (ℕ → α)

def Exchangeability.Bridge.pathify {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (X : ℕ → Ω → α) : Ω → PathSpace α

Factor map that sends ω : Ω to the path (n ↦ X n ω)

Equations

• Exchangeability.Bridge.pathify X ω n = X n ω

theorem Exchangeability.Bridge.measurable_pathify {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {X : ℕ → Ω → α} (hX_meas : ∀ (n : ℕ), Measurable (X n)) : Measurable (pathify X)

def Exchangeability.Bridge.μ_path {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → α) : MeasureTheory.Measure (PathSpace α)

Law of the process as a probability measure on path space.

Equations

• Exchangeability.Bridge.μ_path μ X = MeasureTheory.Measure.map (Exchangeability.Bridge.pathify X) μ

def Exchangeability.Bridge.μ_path' {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {α : Type u_2} [MeasurableSpace α] (X : ℕ → Ω → α) : MeasureTheory.Measure (PathSpace α)

Alternate definition of process law without explicit μ for compatibility. Equivalent to μ_path but with μ as an implicit argument.

Equations

• Exchangeability.Bridge.μ_path' X = MeasureTheory.Measure.map (Exchangeability.Bridge.pathify X) μ

theorem Exchangeability.Bridge.isProbabilityMeasure_μ_path {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → α) (hX : ∀ (n : ℕ), Measurable (X n)) : MeasureTheory.IsProbabilityMeasure (μ_path μ X)

B. Bridge 1: Contractable → Shift Invariance

theorem Exchangeability.Bridge.contractable_shift_invariant_law {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → ℝ} (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) : MeasureTheory.Measure.map PathSpace.shift (μ_path μ X) = μ_path μ X

Bridge 1. Contractable ⇒ shift-invariant law on path space.

theorem Exchangeability.Bridge.measurable_shift_real : Measurable PathSpace.shift

Measurability of shift on path space.

theorem Exchangeability.Bridge.measurePreserving_shift_path {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX : Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) : MeasureTheory.MeasurePreserving PathSpace.shift (μ_path μ X) (μ_path μ X)

Bridge 1'. Package the previous lemma as MeasurePreserving for MET.