Positive-probability passage above some strictly positive level before any horizon

Proved

AvramDividend.Classical.unbounded_positive_level_upcrossing_before_horizon

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

avram-dividendfirst-passagepositive-levelunbounded-variationupcrossing

For any positive time horizon and unbounded-variation spectrally negative Lévy process, there exists a deterministic strictly positive level a whose upcrossing event by that horizon has strictly positive probability. The Lévy exponential-moment growth supplies positive mass of X_t>0; countable positive-tail separation gives some a>0 with positive mass of X_t>a; every such terminal path crosses above a by time t. This is a direct supporting first-passage existence statement without the un-killed martingale fallacy.

Preamble

import Theorems.Thm_AvramDividend_Classical_unbounded_levy_positive_upward_increment_measure_all_times
import Theorems.Thm_AvramDividend_Classical_positive_measure_positive_real_tail_contains_positive_level
import Mathlib.MeasureTheory.OuterMeasure.Basic

open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.unbounded_positive_level_upcrossing_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 {ω : Ω | ∃ s : ℝ≥0, s ≤ t ∧ a < X.X s ω} := by sorry

Source

Proved positive exponent/upward increment, positive mass positive level, and Mathlib measure_mono.

View graph