Post-upcrossing controlled reserve is the reflected shifted Lévy increment path

Proved

AvramDividend.Classical.barrierStrategy_controlledReserve_shifted_reflectedPath

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

barrier-strategypost-upcrossingruinshifted-processstrong-markov

At the first finite upward crossing u of a-x, after any elapsed time t the controlled surplus under the barrier strategy equals the reserve a plus the increment after u minus the running maximum of the shifted Lévy increments. The formula identifies the exact future ruin event and is essential for translating killed dividend-payment windows.

Preamble

import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith
import Definitions.Def_AvramDividend_Classical_DividendStrategy
import Theorems.Thm_AvramDividend_Classical_firstUpcrossing_value_eq_threshold
import Theorems.Thm_AvramDividend_Classical_barrierStrategy_at_firstUpcrossing_zero
import Theorems.Thm_AvramDividend_Classical_barrierStrategy_after_firstUpcrossing_increment_eq_shiftedSup
import Theorems.Thm_AvramDividend_Classical_levyPath_bddAbove_Icc

open MeasureTheory Set
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.barrierStrategy_controlledReserve_shifted_reflectedPath
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (x a : ℝ) (hx0 : 0 ≤ x) (hxa : x ≤ a)
    (ω : Ω) (u t : ℝ≥0)
    (hu : (u : ℝ≥0∞) =
      (⨅ (s : ℝ≥0) (_ : a - x < X.X s ω), (s : ℝ≥0∞))) :
    riskProcess X x (barrierStrategy X x a) (u + t) ω =
      a + (X.X (u + t) ω - X.X u ω) -
        sSup ((fun r : ℝ≥0 => X.X (u + r) ω - X.X u ω) ''
          Set.Icc 0 t) := by
  sorry

Source

Direct child 79978d61-9d1f-4b20-b8a5-114797a8e380. Uses proved finite first crossing attainment, zero dividend at crossing, shifted running-supremum dividend increment and boundedness. The conclusion specifies post-crossing ruin in terms of shifted path, without W/scale parameters.

View graph