Compatible families for the local càdlàg path space

This module extends the basic DLoc API with the measurable equivalence between local càdlàg paths and compatible families of restrictions to integer horizons. It also proves that finite laws on DLoc are determined by these restrictions.

The construction uses PathLawFamily; the law-independent carrier, filtrations, and passage times are provided by DLocBasic.

def BGW.Skorokhod.DLoc.toCompatible (f : DLoc) : CompatiblePaths (fun (n : ℕ) => ↑n + 1) strictMono_succHorizon

The compatible integer-horizon family of a local path (horizons n + 1).

Equations

• f.toCompatible = ⟨fun (n : ℕ) => BGW.Skorokhod.DLoc.restrict ⟨↑n + 1, ⋯⟩ f, ⋯⟩

noncomputable def BGW.Skorokhod.DLoc.glue (p : CompatiblePaths (fun (n : ℕ) => ↑n + 1) strictMono_succHorizon) : DLoc

Gluing: a compatible integer-horizon family determines a local càdlàg path.

Equations

• BGW.Skorokhod.DLoc.glue p = ⟨fun (t : NNReal) => (↑p ⌈↑t⌉₊) ⟨↑t, ⋯⟩, ⋯⟩

theorem BGW.Skorokhod.DLoc.restrict_glue (p : CompatiblePaths (fun (n : ℕ) => ↑n + 1) strictMono_succHorizon) (n : ℕ) (t : ↑(Set.Icc 0 (↑n + 1))) : ↑(glue p) ⟨↑t, ⋯⟩ = (↑p n) t

Gluing restricts back to the family.

theorem BGW.Skorokhod.DLoc.glue_toCompatible (f : DLoc) : glue f.toCompatible = f

The gluing is inverted by the family of restrictions.

theorem BGW.Skorokhod.DLoc.toCompatible_glue (p : CompatiblePaths (fun (n : ℕ) => ↑n + 1) strictMono_succHorizon) : (glue p).toCompatible = p

Restricting a glued family recovers the compatible family.

noncomputable def BGW.Skorokhod.DLoc.measurableEquivCompatible : DLoc ≃ᵐ CompatiblePaths (fun (n : ℕ) => ↑n + 1) strictMono_succHorizon

DLoc is measurably equivalent to the compatible families of restrictions to [0, n + 1], so laws constructed in PathLawFamily transfer to DLoc.

Equations

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

theorem BGW.Skorokhod.DLoc.measure_ext_of_restrict {P Q : MeasureTheory.Measure DLoc} [MeasureTheory.IsFiniteMeasure P] (h : ∀ (n : ℕ), MeasureTheory.Measure.map (restrict ↑n) P = MeasureTheory.Measure.map (restrict ↑n) Q) : P = Q

Two finite measures with equal restrictions to every integer horizon are equal.