Infima of càdlàg paths on suffixes and windows

Suffix and bounded-window infima are J1-continuous at paths continuous at the relevant left endpoint. The window statement is obtained by restriction to an initial segment.

noncomputable def BGW.Skorokhod.suffixInf {T : ℝ} (f : D T ℝ) (c : ↑(Set.Icc 0 T)) : ℝ

The infimum of a compact càdlàg path over a suffix beginning at c.

Equations

• BGW.Skorokhod.suffixInf f c = ⨅ (s : { s : ↑(Set.Icc 0 T) // c ≤ s }), f ↑s

theorem BGW.Skorokhod.continuousAt_suffixInf {T : ℝ} {c : ↑(Set.Icc 0 T)} {f : D T ℝ} (hf : ContinuousAt (⇑f) c) : ContinuousAt (fun (g : D T ℝ) => suffixInf g c) f

Suffix infima are J1-continuous at paths continuous at the initial endpoint.

noncomputable def BGW.Skorokhod.windowInf {T : ℝ} (f : D T ℝ) {a b : ℝ} (ha : 0 ≤ a) (_hab : a ≤ b) (hbT : b ≤ T) : ℝ

The infimum of a finite path over a closed subinterval.

Equations

• BGW.Skorokhod.windowInf f ha _hab hbT = ⨅ (u : ↑(Set.Icc a b)), f ⟨↑u, ⋯⟩

theorem BGW.Skorokhod.continuousAt_windowInf {T a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hbT : b ≤ T) {f : D T ℝ} (hfa : ContinuousAt ⇑f ⟨a, ⋯⟩) (hfb : b = T ∨ ContinuousAt ⇑f ⟨b, ⋯⟩) : ContinuousAt (fun (g : D T ℝ) => windowInf g ha hab hbT) f

Window infima are J1-continuous if both endpoints are continuity points; the original terminal endpoint needs no continuity premise.