Strict upper exit time is monotone in the crossing threshold

Proved

AvramDividend.Classical.twoSidedExitUpTime_mono_threshold

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

avram-dividendpassage-timestrict-upcrossingthreshold-monotonicitytwo-sided-exit

For each Lévy path, if a ≤ b, the first strict crossing above a occurs no later than the first strict crossing above b. This supports monotone approximation of exit boundaries and bounded-horizon passage arguments.

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.twoSidedExitUpTime_mono_threshold
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    {P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (a b : ℝ) (hab : a ≤ b) (ω : Ω) :
    twoSidedExitUpTime X a ω ≤ twoSidedExitUpTime X b ω := by sorry

Source

Nested indexed-infimum definition of twoSidedExitUpTime and order bounds for strict inequalities.

View graph