The drift deficit of the actual infinite-activity bounded-variation Lévy process is strictly increasing on all positive-length intervals almost surely

Proved

AvramDividend.Classical.bv_infinite_activity_deficit_strictMono_ae

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

avram-classicaldrift-deficitinfinite-activitystrict-monotonezero-barrier

For a BV spectrally negative Lévy process with infinite negative Lévy measure, the physical-drift deficit dt-Xt is almost surely strictly increasing as a function of all nonnegative real times. Instantiate the already proved dense-grid strict monotonicity theorem using Mathlib's canonical countable dense sequence of NNReal values.

Preamble

import Theorems.Thm_AvramDividend_Classical_bv_infinite_activity_deficit_strictMono_of_dense_grid
import Mathlib.Topology.Bases
import Mathlib.Topology.Instances.NNReal.Lemmas

open AvramDividend.Classical MeasureTheory Set Topology
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.bv_infinite_activity_deficit_strictMono_ae
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (hBV : X.BoundedVariation)
    (hνinf : X.ν (Iio (0 : ℝ)) = ⊤) :
    ∀ᵐ ω ∂P, StrictMono
      (fun t : ℝ≥0 => X.drift * (t : ℝ) - X.X t ω) := by sorry

Source

Accepted conditional dense-grid strict monotonicity theorem; TopologicalSpace.denseRange_denseSeq in pinned Mathlib.Topology.Bases.

View graph