Negative jumps and the offspring step-path bound

Negation preserves J1 distance. An offspring walk has steps at least -1, so its normalized step paths have negative jumps bounded by the reciprocal normalizer, including at the horizon. The jump functional is that of Billingsley, Convergence of Probability Measures, 2nd ed., 1999, Section 13.

def BGW.Skorokhod.negPath {T : ℝ} (f : D T ℝ) : D T ℝ

Negation of a real càdlàg path.

Equations

• BGW.Skorokhod.negPath f = { toFun := fun (t : ↑(Set.Icc 0 T)) => -f t, isCadlag' := ⋯ }

theorem BGW.Skorokhod.isometry_negPath {T : ℝ} : Isometry negPath

Negation preserves the J1 metric.

noncomputable def BGW.Skorokhod.maxNegativeJump {T : ℝ} (f : D T ℝ) : ℝ

The largest negative jump of a real càdlàg path.

Equations

• BGW.Skorokhod.maxNegativeJump f = BGW.Skorokhod.maxJump (BGW.Skorokhod.negPath f)

theorem BGW.Skorokhod.continuous_maxNegativeJump {T : ℝ} : Continuous maxNegativeJump

The largest negative jump is continuous in J1.

theorem BGW.Skorokhod.maxNegativeJump_le_iff {T c : ℝ} (hT : 0 ≤ T) (hc : 0 ≤ c) (f : D T ℝ) : maxNegativeJump f ≤ c ↔ ∀ (t : ↑(Set.Icc 0 T)), Function.leftLim (⇑f) t - f t ≤ c

A uniform bound on all negative jumps is equivalent to a bound on their maximum.

theorem BGW.Skorokhod.leftLim_sub_realStepPath_le {T b : ℝ} (n : ℕ) (hb : 0 < b) (ω : ℕ → ℝ) (hω : ∀ (i : ℕ), -1 ≤ ω i) (t : ↑(Set.Icc 0 T)) : Function.leftLim (⇑(realStepPath T n b ω)) t - (realStepPath T n b ω) t ≤ 1 / b

For steps at least -1 and a positive normalizer, every negative jump of the step path is at most the reciprocal normalizer.