Continuity of restriction and stopping #
Restriction is continuous at paths continuous at the new terminal endpoint.
theorem
BGW.Skorokhod.continuousAt_restrict
{T : ℝ}
{E : Type u_1}
[MetricSpace E]
{a : ℝ}
(ha : 0 ≤ a)
(haT : a ≤ T)
{f : D T E}
(hf : ContinuousAt ⇑f ⟨a, ⋯⟩)
:
ContinuousAt (restrict haT) f
Restriction is continuous at every path continuous at a (C6.2).
theorem
BGW.Skorokhod.continuousAt_stop
{T : ℝ}
{E : Type u_1}
[MetricSpace E]
{a : ℝ}
(ha : 0 ≤ a)
(haT : a ≤ T)
{f : D T E}
(hf : ContinuousAt ⇑f ⟨a, ⋯⟩)
:
ContinuousAt (stop a) f
Stopping at a is continuous at every path continuous at a (C6.2).
theorem
BGW.Skorokhod.continuousAt_oscillationFrom
{T : ℝ}
{c : ↑(Set.Icc 0 T)}
{f : D T ℝ}
(hf : ContinuousAt (⇑f) c)
:
The oscillation sup_{s ≥ c} |g s - g c| after time c is continuous at every path
continuous at c (C6.3).