Controlled reserve equals raw Lévy capital before first barrier upcrossing

Proved

AvramDividend.Classical.riskProcess_barrier_before_firstUpcrossing_eq_raw

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

avram-classicalbarrier-strategyfirst-passageruinstrong-markov

Pathwise, prior to the first upward barrier passage the barrier strategy has paid no dividends, so the controlled reserve x+X-D agrees with the uncontrolled reserve x+X. Identifies the pre-upcrossing ruin event needed to apply the killed strong-Markov barrier-value splitting.

Preamble

import Theorems.Thm_AvramDividend_Classical_firstUpcrossing_prethreshold_le
import Theorems.Thm_AvramDividend_Classical_barrierStrategy_zero_before_upcrossing
import Definitions.Def_AvramDividend_Classical_DividendStrategy

open MeasureTheory Set
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.riskProcess_barrier_before_firstUpcrossing_eq_raw
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (x a : ℝ)
    (ω : Ω) (u t : ℝ≥0)
    (hu : (u : ℝ≥0∞) =
      (⨅ (s : ℝ≥0) (_ : a - x < X.X s ω), (s : ℝ≥0∞)))
    (ht : t < u) :
    riskProcess X x (barrierStrategy X x a) t ω = x + X.X t ω := by
  sorry

Source

Root-connected pathwise killing-event bridge for dividendValue_barrierStrategy_upExit_split_of_standing 79978d61-9d1f-4b20-b8a5-114797a8e380 and barrierStrategy_value_eq_killed_exit_mul_supValue 8fc83520-78bb-4a8c-a394-12b04a096b66. Uses published prethreshold and no-dividend lemmas, no scale-function parameters.

View graph