Joint extrema under fixed-horizon reversal

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters IV and VI.

theorem BGW.StableTrees.iSup_reverseIncrements {T : ℝ} (hT : 0 ≤ T) (f : Skorokhod.D T ℝ) (hf : ∀ (t : ↑(Set.Icc 0 T)), Function.leftLim (⇑f) t ≤ f t) : ⨆ (u : ↑(Set.Icc 0 T)), (Skorokhod.reverseIncrements hT f) u = f ⟨T, ⋯⟩ - ⨅ (u : ↑(Set.Icc 0 T)), f u

Reversal turns the supremum into the terminal value minus the running infimum, for a path whose jumps are nonnegative.

theorem BGW.StableTrees.reverseIncrements_terminal {T : ℝ} (hT : 0 ≤ T) (f : Skorokhod.D T ℝ) : (Skorokhod.reverseIncrements hT f) ⟨T, ⋯⟩ = f ⟨T, ⋯⟩ - f ⟨0, ⋯⟩

The reversed terminal value is the original increment over the whole interval.

theorem BGW.StableTrees.lintegral_sup_drawdown_reverse {θ T : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (hT : 0 < T) {F G : ℝ → ENNReal} (hF : Measurable F) (hG : Measurable G) : ∫⁻ (f : Skorokhod.D T ℝ), F (⨆ (u : ↑(Set.Icc 0 T)), f u) * G ((⨆ (u : ↑(Set.Icc 0 T)), f u) - f ⟨T, ⋯⟩) ∂↑(stableProcessLaw θ T) = ∫⁻ (f : Skorokhod.D T ℝ), G (-⨅ (u : ↑(Set.Icc 0 T)), f u) * F (f ⟨T, ⋯⟩ - ⨅ (u : ↑(Set.Icc 0 T)), f u) ∂↑(stableProcessLaw θ T)

Fixed-horizon joint reversal of the supremum and drawdown, in nonnegative test form.

theorem BGW.StableTrees.lintegral_sup_drawdown_reverse_local {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) {t : NNReal} (ht : 0 < t) {F G : ℝ → ENNReal} (hF : Measurable F) (hG : Measurable G) : ∫⁻ (f : Skorokhod.DLoc), F (supRunning f t) * G (supReflected f t) ∂↑(stableLocalLaw θ) = ∫⁻ (f : Skorokhod.DLoc), G (localTime f t) * F (↑(reflectedFrom 0 f) t) ∂↑(stableLocalLaw θ)

Fixed-time joint reversal on the local stable path law.