Measurable approximations of càdlàg paths

This module collects path measurability tools for the later Borel and cylinder results.

theorem BGW.Skorokhod.Measurable.comp_of_countable_range {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSingletonClass β] [MeasurableSpace γ] {g : α → β} (hg : Measurable g) (hgc : (Set.range g).Countable) (f : β → γ) : Measurable (f ∘ g)

A measurable map with countable range remains measurable after any function on its range.

theorem BGW.Skorokhod.exists_right_oscillation {T : ℝ} {E : Type u_4} [MetricSpace E] (f : D T E) (t : ↑(Set.Icc 0 T)) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ (s : ↑(Set.Icc 0 T)), ↑t ≤ ↑s → ↑s < ↑t + δ → dist (f s) (f t) < ε

Right continuity gives a right neighborhood on which a path stays close to its value.

theorem BGW.Skorokhod.exists_left_oscillation {T : ℝ} {E : Type u_4} [MetricSpace E] (f : D T E) (t : ↑(Set.Icc 0 T)) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ (s : ↑(Set.Icc 0 T)), ↑t - δ < ↑s → ↑s < ↑t → dist (f s) (Function.leftLim (⇑f) t) < ε

A left limit controls path values in a sufficiently small left neighborhood.

theorem BGW.Skorokhod.exists_local_path_ball {T : ℝ} {E : Type u_4} [MetricSpace E] (f : D T E) (t : ↑(Set.Icc 0 T)) {ε : ℝ} (hε : 0 < ε) : ∃ r > 0, ∀ (s : ↑(Set.Icc 0 T)), dist s t < r → (↑s < ↑t → dist (f s) (Function.leftLim (⇑f) t) < ε / 2) ∧ (t ≤ s → dist (f s) (f t) < ε / 2)

A neighborhood of a time has small oscillation on each side of that time.

theorem BGW.Skorokhod.exists_small_oscillation_partition {T : ℝ} {E : Type u_4} [MetricSpace E] (f : D T E) (hT : 0 ≤ T) {ε : ℝ} (hε : 0 < ε) : ∃ (u : ℕ → ↑(Set.Icc 0 T)), u 0 = ⟨0, ⋯⟩ ∧ Monotone u ∧ (∃ (m : ℕ), ∀ n ≥ m, ↑(u n) = T) ∧ ∀ (n : ℕ) (s v : ↑(Set.Icc 0 T)), ↑(u n) ≤ ↑s → s < u (n + 1) → ↑(u n) ≤ ↑v → v < u (n + 1) → dist (f s) (f v) < ε

A half-open partition on which a càdlàg path has arbitrarily small oscillation.

theorem BGW.Skorokhod.exists_uniform_step_approximation {T : ℝ} {E : Type u_4} [MetricSpace E] (f : D T E) (hT : 0 ≤ T) {ε : ℝ} (hε : 0 < ε) : ∃ (u : ℕ → ↑(Set.Icc 0 T)) (g : ↑(Set.Icc 0 T) → E), u 0 = ⟨0, ⋯⟩ ∧ Monotone u ∧ (∃ (m : ℕ), ∀ n ≥ m, ↑(u n) = T) ∧ (∀ (n : ℕ) (s : ↑(Set.Icc 0 T)), ↑(u n) ≤ ↑s → s < u (n + 1) → g s = f (u n)) ∧ ∀ (s : ↑(Set.Icc 0 T)), dist (g s) (f s) < ε

A càdlàg path is uniformly approximated by functions constant on half-open partition blocks.

theorem BGW.Skorokhod.finite_setOf_jump_gt {T : ℝ} {E : Type u_4} [MetricSpace E] (f : D T E) {ε : ℝ} (hε : 0 < ε) : {t : ↑(Set.Icc 0 T) | ε < dist (Function.leftLim (⇑f) t) (f t)}.Finite

A càdlàg path has only finitely many jumps larger than any fixed positive threshold.

theorem BGW.Skorokhod.countable_setOf_jump_ne {T : ℝ} {E : Type u_4} [MetricSpace E] (f : D T E) : {t : ↑(Set.Icc 0 T) | Function.leftLim (⇑f) t ≠ f t}.Countable

The set of discontinuity times of a càdlàg path is countable.

noncomputable def BGW.Skorokhod.dyadicRightTime {T : ℝ} (hT : 0 ≤ T) (n : ℕ) (t : ↑(Set.Icc 0 T)) : ↑(Set.Icc 0 T)

The next dyadic grid point, capped at the terminal time.

Equations

• BGW.Skorokhod.dyadicRightTime hT n t = ⟨min (↑(⌈2 ^ n * ↑t⌉₊ + 1) / 2 ^ n) T, ⋯⟩

theorem BGW.Skorokhod.measurable_dyadicRightTime {T : ℝ} (hT : 0 ≤ T) (n : ℕ) : Measurable (dyadicRightTime hT n)

The dyadic right approximation is measurable as a function of time.

theorem BGW.Skorokhod.countable_range_dyadicRightTime {T : ℝ} (hT : 0 ≤ T) (n : ℕ) : (Set.range (dyadicRightTime hT n)).Countable

For each fixed grid level, the dyadic right approximation has countable range.

theorem BGW.Skorokhod.le_dyadicRightTime {T : ℝ} (hT : 0 ≤ T) (n : ℕ) (t : ↑(Set.Icc 0 T)) : t ≤ dyadicRightTime hT n t

The dyadic right approximation never precedes the given time.

theorem BGW.Skorokhod.lt_dyadicRightTime {T : ℝ} (hT : 0 ≤ T) (n : ℕ) {t : ↑(Set.Icc 0 T)} (ht : ↑t < T) : t < dyadicRightTime hT n t

The next dyadic grid point is strictly to the right before the terminal time.

theorem BGW.Skorokhod.tendsto_dyadicRightTime {T : ℝ} (hT : 0 ≤ T) (t : ↑(Set.Icc 0 T)) : Filter.Tendsto (fun (n : ℕ) => dyadicRightTime hT n t) Filter.atTop (nhds t)

Dyadic right times converge to the time being approximated.

theorem BGW.Skorokhod.measurable_path {T : ℝ} {E : Type u_4} [MetricSpace E] [MeasurableSpace E] [BorelSpace E] (f : D T E) (hT : 0 < T) : Measurable ⇑f

Every càdlàg path on a positive compact interval is Borel measurable in time.