Continuity of the càdlàg Vervaat map

A positive minimizing time and continuity there give continuity at the terminal endpoint. Positivity of the minimizing time is essential for this conclusion. Local correction of J1 time changes near a unique continuous minimum proves continuity of the transformation without disturbing the other jumps.

References: W. Vervaat, A relation between Brownian bridge and Brownian excursion, Ann. Probab. 7 (1979); T. Duquesne, A limit theorem for the contour process of conditioned Galton–Watson trees, Ann. Probab. 31 (2003), §4; items C33–C34 of CLASSICAL_THEORY_INPUTS.md.

theorem BGW.Skorokhod.vervaatD_zero_of_continuousAt {f : D 1 ℝ} (hg : ContinuousAt (⇑f) (vervaatTime f)) : (vervaatD f) ⟨0, ⋯⟩ = 0

Continuity at the minimizing time makes the transformed initial value zero.

theorem BGW.Skorokhod.continuousAt_vervaatD_wrap {f : D 1 ℝ} (h1 : ContinuousAt ⇑f ⟨1, ⋯⟩) : ContinuousAt (⇑(vervaatD f)) (Set.projIcc 0 1 ⋯ (1 - ↑(vervaatTime f)))

Continuity at the original terminal endpoint makes the transformed wrap point continuous.

theorem BGW.Skorokhod.vervaatD_one_of_continuousAt {f : D 1 ℝ} (hg0 : 0 < ↑(vervaatTime f)) (hg : ContinuousAt (⇑f) (vervaatTime f)) : (vervaatD f) ⟨1, ⋯⟩ = f ⟨1, ⋯⟩ - f ⟨0, ⋯⟩ ∧ ContinuousAt ⇑(vervaatD f) ⟨1, ⋯⟩

If the first infimum time is positive and f is continuous there, then V f is continuous at 1 with value f 1 - f 0 (C33.3, with the corrected premise 0 < g of roadmap §8.3: for f t = t on [0,1) and f 1 = 2 one has g = 0 and V f = f, discontinuous at 1).

theorem BGW.Skorokhod.continuousAt_vervaatD {f : D 1 ℝ} (h0 : f ⟨0, ⋯⟩ = 0) (h1 : ContinuousAt ⇑f ⟨1, ⋯⟩) (huniq : ∀ (t : ↑(Set.Icc 0 1)), min (Function.leftLim (⇑f) t) (f t) = ⨅ (s : ↑(Set.Icc 0 1)), f s → t = vervaatTime f) (hint : 0 < ↑(vervaatTime f) ∧ ↑(vervaatTime f) < 1) (hg : ContinuousAt (⇑f) (vervaatTime f)) : ContinuousAt vervaatD f ∧ (vervaatD f) ⟨0, ⋯⟩ = 0 ∧ ContinuousAt (⇑(vervaatD f)) (Set.projIcc 0 1 ⋯ (1 - ↑(vervaatTime f)))

Continuity of the càdlàg Vervaat map (C34): at a path vanishing at 0, continuous at 1, whose infimum is attained (as a value or left limit) only at an interior time g where the path is continuous. Moreover V f vanishes at 0 and is continuous at 1 - g.