Stability of the first minimum time #
The completed lower envelope has a strictly positive gap away from a unique minimizer. Uniform approximation after a time change preserves this gap.
theorem
BGW.Skorokhod.dist_completedValue_timeChange_le
(u f : D 1 ℝ)
(σ : TimeChange 1)
{e : ℝ}
(he : ∀ (t : ↑(Set.Icc 0 1)), dist (u (σ t)) (f t) ≤ e)
(t : ↑(Set.Icc 0 1))
:
Uniform path control after a time change also controls the completed lower envelope.
theorem
BGW.Skorokhod.continuousAt_vervaatTime
{f : D 1 ℝ}
(huniq : ∀ (t : ↑(Set.Icc 0 1)), min (Function.leftLim (⇑f) t) (f t) = ⨅ (s : ↑(Set.Icc 0 1)), f s → t = vervaatTime f)
:
A unique completed minimum makes the first minimizing time J1-continuous.