Measurability of the càdlàg Vervaat map

The first minimizing time is measurable because its sublevel sets are equality sets between prefix infima and the global infimum. Joint evaluation then gives measurability of the rotated path.

theorem BGW.Skorokhod.vervaatTime_le_iff_prefix_inf (f : D 1 ℝ) (a : ↑(Set.Icc 0 1)) : vervaatTime f ≤ a ↔ ⨅ (t : ↑(Set.Iic a)), f ↑t = ⨅ (t : ↑(Set.Icc 0 1)), f t

A prefix contains the first minimizing time exactly when its infimum is global.

theorem BGW.Skorokhod.measurable_vervaatTime : Measurable vervaatTime

The canonical first minimum time is measurable, including at paths with tied minima.

theorem BGW.Skorokhod.measurable_vervaatD : Measurable vervaatD

The càdlàg Vervaat map is Borel (C33.4).