Successful strict two-sided upper exit implies survival above the lower level throughout the prefix

Proved

AvramDividend.Classical.strict_up_before_down_preserves_lower_prefix

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

For any strict upward and downward first-passage clocks of a Lévy path, if the upper clock is strictly before the lower clock then at every earlier deterministic time t the path value is at least the lower threshold. Otherwise the witnessing lower crossing at t forces the lower passage clock to be at most t, contradicting the strict order. This elementary but exact named-clock event inclusion converts the standard q-scale two-sided upper-first exit payoff into the lower ordinary prefix-survival payoff used in the stopped-dividend record sandwich.

Preamble

import Mathlib.Order.ConditionallyCompleteLattice.Basic
import Definitions.Def_AvramDividend_Classical_TwoSidedExit

open MeasureTheory
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.strict_up_before_down_preserves_lower_prefix
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (u d : ℝ) (ω : Ω)
    (hUp : twoSidedExitUpTime X u ω <
      twoSidedExitDownTime X d ω) :
    ∀ t : ℝ≥0, (t : ℝ≥0∞) < twoSidedExitUpTime X u ω →
      d ≤ X.X t ω := by sorry

Source

Order of first-passage stopping times; interface between Avram Palmowski Pistorius (2007) equation (3.6) and the first-record reflected survival sandwich.

View graph