Basic API for the local càdlàg path space

The space DLoc consists of real càdlàg paths on nonnegative time. It carries the σ-algebra generated by evaluations, together with restriction, shifting, natural filtrations, and strict passage times. This module is independent of path-law constructions and Kolmogorov extension.

References

• P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999, Section 16.
• D. Revuz and M. Yor, Continuous Martingales and Brownian Motion, 3rd ed., Springer, 1999, Chapter I, Section 4.

theorem BGW.Skorokhod.strictMono_succHorizon : StrictMono fun (n : ℕ) => ↑n + 1

The integer horizons n + 1 are positive and strictly increasing.

def BGW.Skorokhod.DLoc : Type

The local càdlàg carrier: càdlàg real paths on ℝ≥0 (Mathlib's IsCadlag; at 0 the left limit is vacuous).

Equations

• BGW.Skorokhod.DLoc = { f : NNReal → ℝ // IsCadlag f }

def BGW.Skorokhod.DLoc.eval (t : NNReal) (f : DLoc) : ℝ

Evaluation at time t.

Equations

• BGW.Skorokhod.DLoc.eval t f = ↑f t

@[instance_reducible]

noncomputable instance BGW.Skorokhod.DLoc.instMeasurableSpace : MeasurableSpace DLoc

The evaluation σ-algebra: the supremum of the pullbacks of the Borel σ-algebra of ℝ under all evaluations.

Equations

• BGW.Skorokhod.DLoc.instMeasurableSpace = ⨆ (t : NNReal), MeasurableSpace.comap (BGW.Skorokhod.DLoc.eval t) inferInstance

def BGW.Skorokhod.DLoc.restrict (T : NNReal) (f : DLoc) : D ↑T ℝ

Restriction to [0, T], as an element of the compact path space.

Equations

• BGW.Skorokhod.DLoc.restrict T f = { toFun := fun (t : ↑(Set.Icc 0 ↑T)) => ↑f ⟨↑t, ⋯⟩, isCadlag' := ⋯ }

def BGW.Skorokhod.DLoc.shift (s : NNReal) (f : DLoc) : DLoc

Centered shift: u ↦ f (s + u) - f s.

Equations

• BGW.Skorokhod.DLoc.shift s f = ⟨fun (u : NNReal) => ↑f (s + u) - ↑f s, ⋯⟩

theorem BGW.Skorokhod.DLoc.measurable_eval (t : NNReal) : Measurable (eval t)

Evaluation is measurable.

theorem BGW.Skorokhod.DLoc.measurable_restrict (T : NNReal) : Measurable (restrict T)

Restriction to every compact horizon is measurable.

theorem BGW.Skorokhod.DLoc.measurableSpace_eq_iSup_comap_restrict : inferInstance = ⨆ (n : ℕ), MeasurableSpace.comap (restrict ↑n) inferInstance

The evaluation σ-algebra is generated by restrictions to integer horizons.

theorem BGW.Skorokhod.DLoc.measurable_eval₂ : Measurable fun (p : DLoc × NNReal) => ↑p.1 p.2

Joint measurability of (f, t) ↦ f t.

theorem BGW.Skorokhod.DLoc.measurable_shift : Measurable fun (p : NNReal × DLoc) => shift p.1 p.2

Joint measurability of the centered shift (s, f) ↦ shift s f.

theorem BGW.Skorokhod.DLoc.shift_shift (s t : NNReal) (f : DLoc) : shift s (shift t f) = shift (t + s) f

The shift is a semigroup action: shift s (shift t f) = shift (t + s) f.

theorem BGW.Skorokhod.DLoc.restrict_restrict {a T : NNReal} (h : a ≤ T) (f : DLoc) : Skorokhod.restrict ⋯ (restrict T f) = restrict a f

Restrictions are compatible with each other.

theorem BGW.Skorokhod.DLoc.ext_of_restrict {f g : DLoc} (h : ∀ (n : ℕ), restrict (↑n) f = restrict (↑n) g) : f = g

Extensionality by restrictions to the integer horizons.

Filtrations

noncomputable def BGW.Skorokhod.DLoc.rawFiltration : MeasureTheory.Filtration NNReal inferInstance

The natural (raw) filtration F_t = σ(f s : s ≤ t). It does not depend on any law.

Equations

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

noncomputable def BGW.Skorokhod.DLoc.filtration : MeasureTheory.Filtration NNReal inferInstance

The right-continuous filtration F⁺_t = ⋂_{u > t} F_u (Mathlib's rightCont).

Equations

• BGW.Skorokhod.DLoc.filtration = BGW.Skorokhod.DLoc.rawFiltration.rightCont

instance BGW.Skorokhod.DLoc.instIsRightContinuousNNRealFiltration : filtration.IsRightContinuous

The filtration filtration is right-continuous.

theorem BGW.Skorokhod.DLoc.iSup_rawFiltration : ⨆ (t : NNReal), ↑rawFiltration t = inferInstance

The σ-algebra of DLoc is the supremum of the raw filtration.

theorem BGW.Skorokhod.DLoc.adapted_eval : MeasureTheory.Adapted filtration fun (t : NNReal) (f : DLoc) => ↑f t

The coordinate process is adapted to the raw filtration, hence to filtration.

theorem BGW.Skorokhod.DLoc.isStronglyProgressive_eval : MeasureTheory.IsStronglyProgressive filtration fun (t : NNReal) (f : DLoc) => ↑f t

Càdlàg coordinate process is progressively measurable.

Strict passage times

noncomputable def BGW.Skorokhod.DLoc.strictPassageAbove (x : ℝ) (f : DLoc) : WithTop NNReal

T_x = inf {t | f t > x} (strict passage upward); ⊤ if the set is empty.

Equations

• BGW.Skorokhod.DLoc.strictPassageAbove x f = ⨅ (t : NNReal), ⨅ (_ : x < ↑f t), ↑t

noncomputable def BGW.Skorokhod.DLoc.strictPassageBelow (x : ℝ) (f : DLoc) : WithTop NNReal

inf {t | f t < x} (strict passage downward).

Equations

• BGW.Skorokhod.DLoc.strictPassageBelow x f = ⨅ (t : NNReal), ⨅ (_ : ↑f t < x), ↑t

theorem BGW.Skorokhod.DLoc.strictPassageAbove_lt_iff (x : ℝ) (f : DLoc) (t : NNReal) : strictPassageAbove x f < ↑t ↔ ∃ (q : ℚ), 0 ≤ q ∧ ↑q < ↑t ∧ x < ↑f (↑q).toNNReal

Deterministic description by rationals (right-continuity): T_x < t iff some rational time before t has value above x.

theorem BGW.Skorokhod.DLoc.isStoppingTime_strictPassageAbove (x : ℝ) : MeasureTheory.IsStoppingTime filtration (strictPassageAbove x)

T_x is a stopping time of the right-continuous filtration.

theorem BGW.Skorokhod.DLoc.strictPassageBelow_neg (x : ℝ) (f : DLoc) : strictPassageBelow (-x) f = strictPassageAbove x ⟨fun (t : NNReal) => -↑f t, ⋯⟩

Deterministic reflection identity (audit, F3): inf{t | f t < -x} is the strict passage of -f above x.

theorem BGW.Skorokhod.DLoc.isStoppingTime_strictPassageBelow (x : ℝ) : MeasureTheory.IsStoppingTime filtration (strictPassageBelow x)

inf {t | f t < x} is a stopping time of the right-continuous filtration.