Positive probability of a strict upper exit clock before any positive horizon

Proved

AvramDividend.Classical.unbounded_first_up_clock_positive_probability_before_horizon

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

avram-dividendfirst-passagelevy-processstrict-horizontwo-sided-exit

For unbounded-variation spectrally negative Lévy processes, before every positive horizon t there exists a positive upper level a whose canonical two-sided upper first-passage clock from reserve zero is less than t with positive probability. This converts the Proved strict pathwise upcrossing event into an event stated using the actual twoSidedExitUpTime definition, giving a root-connected helper for strict two-sided exit identities.

Preamble

import Definitions.Def_AvramDividend_Classical_TwoSidedExit
import Theorems.Thm_AvramDividend_Classical_unbounded_positive_level_upcrossing_strictly_before_horizon
import Mathlib.Data.ENNReal.Basic
import Mathlib.MeasureTheory.OuterMeasure.Basic

open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.unbounded_first_up_clock_positive_probability_before_horizon
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    {P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (q : ℝ) (hq : 0 < q) (hnbv : ¬ X.BoundedVariation)
    (t : ℝ≥0) (ht : 0 < t) :
    ∃ a : ℝ, 0 < a ∧
      0 < P {ω : Ω | twoSidedExitUpTime X a ω < (t : ℝ≥0∞)} := by sorry

Source

Proved unbounded_positive_level_upcrossing_strictly_before_horizon and the iInf representation of twoSidedExitUpTime.

View graph