Random-time shifts of local càdlàg paths

This file defines the centered shift of a local càdlàg path at an extended nonnegative random time and records its basic measurability properties, including measurability of the stopped coordinates (O. Kallenberg, Foundations of Modern Probability, 2nd ed., Springer, 2002, Chapter 7).

noncomputable def BGW.Skorokhod.DLoc.shiftAt (τ : DLoc → ENNReal) (f : DLoc) : DLoc

Post-τ centered shift. shiftAt τ f = (u ↦ f (τ f + u) - f (τ f)) when τ f < ⊤; junk value shift 0 f when τ f = ⊤.

Equations

• BGW.Skorokhod.DLoc.shiftAt τ f = BGW.Skorokhod.DLoc.shift (τ f).toNNReal f

theorem BGW.Skorokhod.DLoc.eval_shiftAt (τ : DLoc → ENNReal) (u : NNReal) {f : DLoc} (hf : τ f < ⊤) : eval u (shiftAt τ f) = eval ((τ f).toNNReal + u) f - eval (τ f).toNNReal f

Evaluation of the post-τ shift on {τ < ⊤}.

theorem BGW.Skorokhod.DLoc.shiftAt_const (s : NNReal) : (shiftAt fun (x : DLoc) => ↑s) = shift s

shiftAt at a constant time is the deterministic shift.

theorem BGW.Skorokhod.DLoc.measurable_shiftAt {τ : DLoc → ENNReal} (hτ : MeasureTheory.IsStoppingTime filtration τ) : Measurable (shiftAt τ)

A stopping time of the right-continuous filtration is Borel measurable, hence so is shiftAt τ on all of DLoc (the junk branch on {τ = ⊤} is measurable too); in particular its restriction to {τ < ⊤} is measurable.

theorem BGW.Skorokhod.DLoc.measurableSet_lt_top_stopped {τ : DLoc → ENNReal} (hτ : MeasureTheory.IsStoppingTime filtration τ) : MeasurableSet {f : DLoc | τ f < ⊤}

{τ < ⊤} is an event of the stopped σ-algebra.

theorem BGW.Skorokhod.DLoc.measurable_stoppedValue_eval {τ : DLoc → ENNReal} (hτ : MeasureTheory.IsStoppingTime filtration τ) : Measurable (MeasureTheory.stoppedValue (fun (t : NNReal) (f : DLoc) => eval t f) τ)

Stopped coordinate, everywhere form. Mathlib's stoppedValue (junk value on {τ = ⊤}) of the coordinate process is measurable for the stopped σ-algebra.

theorem BGW.Skorokhod.DLoc.measurable_eval_toNNReal_stopped {τ : DLoc → ENNReal} (hτ : MeasureTheory.IsStoppingTime filtration τ) (hfin : ∀ (f : DLoc), τ f < ⊤) : Measurable fun (f : DLoc) => eval (τ f).toNNReal f

Stopped coordinate, for τ < ⊤ everywhere: f ↦ f (τ f) is hτ.measurableSpace- measurable.

theorem BGW.Skorokhod.integral_freeze_shiftAt (P : MeasureTheory.Measure DLoc) [MeasureTheory.IsFiniteMeasure P] (Q : MeasureTheory.Measure DLoc) [MeasureTheory.IsFiniteMeasure Q] {Y : DLoc → NNReal} {Z : DLoc → DLoc} (hZ : Measurable Z) {A : Set DLoc} {H : NNReal × DLoc → ℝ} (hH : Measurable H) (hHb : ∃ (C : ℝ), ∀ (p : NNReal × DLoc), |H p| ≤ C) {m : MeasurableSpace DLoc} (hm : m ≤ DLoc.instMeasurableSpace) (hY : Measurable Y) (hA : MeasurableSet A) (hfact : ∀ (B : Set DLoc), MeasurableSet B → B ⊆ A → ∀ (C : Set DLoc), MeasurableSet C → P (B ∩ Z ⁻¹' C) = P B * Q C) : ∫ (f : DLoc) in A, H (Y f, Z f) ∂P = ∫ (f : DLoc) in A, ∫ (g : DLoc), H (Y f, g) ∂Q ∂P

Freezing a stopped-state coordinate turns integration of a bounded measurable functional of an independent future into an iterated integral.