Measurable extrema of càdlàg paths

Right continuity reduces extrema over intervals to a countable family of evaluations.

theorem BGW.Skorokhod.exists_countable_detecting_times {T : ℝ} {J : Set ↑(Set.Icc 0 T)} (hJ : J.OrdConnected) : ∃ (K : Set ↑J), K.Countable ∧ ∀ (E : Type u_2) [inst : MetricSpace E] (f : D T E) (U : Set E), IsOpen U → ∀ (s : ↑J), f ↑s ∈ U → ∃ q ∈ K, f ↑q ∈ U

Countably many interval times detect every open-set visit of every càdlàg path.

theorem BGW.Skorokhod.measurable_iSup_eval {T : ℝ} {J : Set ↑(Set.Icc 0 T)} (hJ : J.OrdConnected) : Measurable fun (f : D T ℝ) => ⨆ (s : ↑J), f ↑s

The supremum of a real path over an interval of times is measurable (C4.4).

theorem BGW.Skorokhod.measurable_iInf_eval {T : ℝ} {J : Set ↑(Set.Icc 0 T)} (hJ : J.OrdConnected) : Measurable fun (f : D T ℝ) => ⨅ (s : ↑J), f ↑s

The infimum of a real path over an interval of times is measurable (C4.4).