Reflected drawdown resets to the shifted future supremum at an attained first record

Proved

AvramDividend.Classical.firstRecord_drawdown_post_shift_reset

by WillR · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

At any finite first strict upward passage u of a nonnegative level b, reflected drawdown is zero at u. Consequently the drawdown at u+t equals precisely the future shifted path's running supremum over [0,t] minus its terminal value. This composes two independently Proved pathwise theorems and removes the pre-record history from the future ruin criterion, a core prerequisite of the strong-Markov killed-record renewal step.

Preamble

import Mathlib.Order.ConditionallyCompleteLattice.Basic
import Definitions.Def_AvramDividend_Classical_Reflection
import Theorems.Thm_AvramDividend_Classical_firstUpcrossing_runningSup_sub_path_eq_zero
import Theorems.Thm_AvramDividend_Classical_drawdown_after_firstUpcrossing_shift

open MeasureTheory Set
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.firstRecord_drawdown_post_shift_reset
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (b : ℝ) (hb : 0 ≤ b) (ω : Ω) (u : ℝ≥0)
    (hu : (u : ℝ≥0∞) =
      (⨅ (s : ℝ≥0) (_ : b < X.X s ω), (s : ℝ≥0∞)))
    (hBdd : BddAbove ((fun r : ℝ≥0 => X.X r ω) '' Set.Icc 0 u)) :
    ∀ t : ℝ≥0,
      runningSup X (u + t) ω - X.X (u + t) ω =
        sSup ((fun r : ℝ≥0 => X.X (u + r) ω) '' Set.Icc 0 t) -
          X.X (u + t) ω := by sorry

Source

Avram, Palmowski and Pistorius (2007), Proposition 1; drawdown restart at attained reflected barrier records.

View graph