Canonical strict lower ruin clock is bounded by any observed strict downcrossing time

Open

AvramDividend.Classical.twoSidedExitDownTime_le_observation_of_strict_downcrossing

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

avram-dividendclockfirst-passageruintwo-sided-exit

For any spectrally negative Lévy process and initial reserve x, the canonical strict lower exit (ruin) clock, defined as an ENNReal infimum over observations satisfying X_s < -x, is at most every observation time s where that strict downward crossing occurs. This deterministic first-passage bound is the counterpart to the strict upper-clock lemma and is useful when proving two-sided stopped-scale and ruin boundary identities.

Preamble

import Definitions.Def_AvramDividend_Classical_TwoSidedExit
import Mathlib.Data.ENNReal.Basic

open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.twoSidedExitDownTime_le_observation_of_strict_downcrossing
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    {P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (x : ℝ) (ω : Ω) (s : ℝ≥0)
    (hs : X.X s ω < -x) :
    twoSidedExitDownTime X x ω ≤ (s : ℝ≥0∞) := by sorry

Source

Definition of twoSidedExitDownTime as nested iInf and the order-theoretic iInf_le rule.

View graph