Unbounded scale zero-mean forces nonpositive Lévy increments

Proved

AvramDividend.Classical.unbounded_discounted_scale_zero_mean_forces_nonpositive_increment_ae

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

avram-dividendscale-functionstopped-martingaleverification-prerequisitezero-origin

For an unbounded-variation spectrally negative Levy process whose q-scale function vanishes at the origin, an integrable un-killed discounted scale reward with expectation zero at any fixed time forces X_t to be nonpositive almost surely. It combines the positive-axis strict positivity of scale functions with the zero-mean nonnegative-reward theorem. This identifies a precise obstacle to using an un-stopped scale-function martingale in the strict-exit proof.

Preamble

import Theorems.Thm_AvramDividend_Classical_discounted_scale_zero_mean_forces_zero_ae
import Theorems.Thm_AvramDividend_Classical_scaleFunction_strict_pos_of_unbounded_variation
import Definitions.Def_AvramDividend_Classical_ScaleFunction

open AvramDividend.Classical MeasureTheory
open scoped NNReal

Formal statement

theorem AvramDividend.Classical.unbounded_discounted_scale_zero_mean_forces_nonpositive_increment_ae
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    {P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (q : ℝ) (W : ℝ → ℝ) (hW : IsScaleFunction X q W)
    (hnbv : ¬ X.BoundedVariation) (hW0 : W 0 = 0) (t : ℝ≥0)
    (hInt : Integrable
      (fun ω : Ω => Real.exp (-(q * (t : ℝ))) * W (X.X t ω)) P)
    (hMean : (∫ ω : Ω, Real.exp (-(q * (t : ℝ))) *
      W (X.X t ω) ∂P) = W 0) :
    ∀ᵐ ω ∂P, X.X t ω ≤ 0 := by sorry

Source

Proved strict positivity of q-scale functions under unbounded variation, and the nonnegative zero-integral criterion.

View graph