Documentation

BGW.Skorokhod.Measurable

Borel structure on the Skorokhod space #

The measurable structure on D is the Borel structure of the J1 metric.

source
theorem BGW.Skorokhod.dist_eval_top_le {T : ℝ} {E : Type u_1} [MetricSpace E] (hT : 0 ≤ T) (f g : D T E) :
dist (f ⟨T, ⋯⟩) (g ⟨T, ⋯⟩) ≤ dist f g

Evaluation at the terminal time is nonexpansive for the J1 metric.

source
@[instance_reducible]
noncomputable instance BGW.Skorokhod.instMeasurableSpace {T : ℝ} {E : Type u_1} [MetricSpace E] :
MeasurableSpace (D T E)

The measurable structure on the Skorokhod space is the Borel structure of J1.

Equations
source
instance BGW.Skorokhod.instBorelSpace {T : ℝ} {E : Type u_1} [MetricSpace E] :
BorelSpace (D T E)

The measurable structure on the Skorokhod space is its Borel structure.

source
theorem BGW.Skorokhod.measurable_eval_top {T : ℝ} {E : Type u_1} [MetricSpace E] [MeasurableSpace E] [BorelSpace E] (hT : 0 ≤ T) :
Measurable fun (f : D T E) => f ⟨T, ⋯⟩

The terminal evaluation map is Lipschitz, hence Borel measurable.

source
theorem BGW.Skorokhod.dist_eval_zero_le {T : ℝ} {E : Type u_1} [MetricSpace E] (hT : 0 ≤ T) (f g : D T E) :
dist (f ⟨0, ⋯⟩) (g ⟨0, ⋯⟩) ≤ dist f g

Evaluation at the initial time is nonexpansive for the J1 metric.

source
theorem BGW.Skorokhod.measurable_eval_zero {T : ℝ} {E : Type u_1} [MetricSpace E] [MeasurableSpace E] [BorelSpace E] (hT : 0 ≤ T) :
Measurable fun (f : D T E) => f ⟨0, ⋯⟩

The initial evaluation map is Lipschitz, hence Borel measurable.

source
theorem BGW.Skorokhod.measurable_leftLim_eval_of_measurable_eval {T : ℝ} {E : Type u_1} [MetricSpace E] [MeasurableSpace E] [BorelSpace E] (hEval : ∀ (s : ↑(Set.Icc 0 T)), Measurable fun (f : D T E) => f s) (t : ↑(Set.Icc 0 T)) :
Measurable fun (f : D T E) => Function.leftLim (⇑f) t

Measurability of all fixed evaluations implies measurability of fixed left limits.

source
theorem BGW.Skorokhod.measurable_eval_on_countable_range {T : ℝ} {E : Type u_1} [MetricSpace E] [MeasurableSpace E] {R : Type u_2} [MeasurableSpace R] [Countable R] [MeasurableSingletonClass R] (τ : R → ↑(Set.Icc 0 T)) (hEval : ∀ (t : ↑(Set.Icc 0 T)), Measurable fun (f : D T E) => f t) :
Measurable fun (p : D T E × R) => p.1 (τ p.2)

Evaluation is measurable when the time argument has countable range.

source
theorem BGW.Skorokhod.measurable_eval₂_of_measurable_eval {T : ℝ} {E : Type u_1} [MetricSpace E] [MeasurableSpace E] [BorelSpace E] (hEval : ∀ (t : ↑(Set.Icc 0 T)), Measurable fun (f : D T E) => f t) :
Measurable fun (p : D T E × ↑(Set.Icc 0 T)) => p.1 p.2

Joint evaluation is a pointwise limit of evaluations at dyadic right times.

source
theorem BGW.Skorokhod.isOpen_setOf_exists_eval_mem {T : ℝ} {E : Type u_1} [MetricSpace E] {U : Set E} (hU : IsOpen U) (a b : ℝ) :
IsOpen {f : D T E | ∃ (s : ↑(Set.Icc 0 T)), a < ↑s ∧ ↑s < b ∧ f s ∈ U}

Hitting an open spatial set during an open time interval is J1-open.

source
theorem BGW.Skorokhod.measurable_eval {T : ℝ} {E : Type u_1} [MetricSpace E] [MeasurableSpace E] [BorelSpace E] (t : ↑(Set.Icc 0 T)) :
Measurable fun (f : D T E) => f t

Each evaluation map is Borel for J1 (C4.1).

source
theorem BGW.Skorokhod.measurable_eval₂ {T : ℝ} {E : Type u_1} [MetricSpace E] [MeasurableSpace E] [BorelSpace E] :
Measurable fun (p : D T E × ↑(Set.Icc 0 T)) => p.1 p.2

Joint evaluation (f, t) ↦ f t is measurable (C4.3).

source
theorem BGW.Skorokhod.measurable_leftLim_eval {T : ℝ} {E : Type u_1} [MetricSpace E] [MeasurableSpace E] [BorelSpace E] (t : ↑(Set.Icc 0 T)) :
Measurable fun (f : D T E) => Function.leftLim (⇑f) t

The left limit at a fixed time is a measurable functional (C4.4).