Positive Lévy exponent gives positive upward-increment probability at every positive time

Proved

AvramDividend.Classical.positive_psi_implies_upward_increment_positive_measure_all_times

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

avram-dividendfirst-passagelevy-processprobabilityupward-increments

At every strictly positive time, the distribution of a spectrally negative Lévy process assigns positive probability to a strictly positive increment whenever the Laplace exponent is positive at some nonnegative argument. If the positive event were null, the exponential moment would be at most one, contradicting the strict inequality exp(tψ(θ))>1. This is a robust all-time version relevant to first-passage arguments and to correction of nonstopped martingale assumptions.

Preamble

import Mathlib.MeasureTheory.Integral.Bochner.Basic
import Mathlib.Analysis.Complex.Exponential
import Mathlib.MeasureTheory.OuterMeasure.AE
import Definitions.Def_AvramDividend_Classical_SpectrallyNegativeLevy

open AvramDividend.Classical MeasureTheory
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.positive_psi_implies_upward_increment_positive_measure_all_times
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    {P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (θ : ℝ) (hθ : 0 ≤ θ) (hψ : 0 < X.ψ θ) :
    ∀ t : ℝ≥0, 0 < t → 0 < P {ω : Ω | 0 < X.X t ω} := by sorry

Source

SpectrallyNegativeLevy.laplace and the pinned Mathlib ae_iff, integral_mono_ae and Real.one_lt_exp_iff.

View graph