Unbounded variation implies almost-sure negative values arbitrarily close to zero

Open

AvramDividend.Classical.ae_negative_near_zero_of_unbounded_variation

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

down-exitregularitystopped-scaletwo-sided-exitunbounded-variation

A spectrally negative Levy process of unbounded variation visits strictly negative values at arbitrarily small positive times, almost surely. This is the almost-sure path regularity (zero is regular for the negative half-line) that feeds the instantaneous down-exit clock used by the zero-start stopped-scale identity and the unbounded-variation leg of the two-sided exit balance.

Preamble

import Mathlib
import Definitions.Def_AvramDividend_Classical_SpectrallyNegativeLevy

open MeasureTheory Filter Set Topology
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.ae_negative_near_zero_of_unbounded_variation
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (hnbv : ¬ X.BoundedVariation) :
    ∀ᵐ ω ∂P, ∀ ε : ℝ≥0, 0 < ε →
      ∃ s : ℝ≥0, s < ε ∧ X.X s ω < 0 := by sorry

Source

Parent AvramDividend.Classical.chat04_unbounded_two_sided_exit_stopped_scale_identity (aed50a34): its repair attempt 15378 fabricated this premise (hDown0 via misapplied hnbv) and failed on 5 independent CE groups. Proved converter chat04_down_exit_time_zero_of_negative_near_zero (ac9a5651) turns per-path near-zero negativity into a zero down-exit clock; Proved zero-start lemma chat04_unbounded_zero_start_stopped_scale_of_down_exit_zero (8029c619) consumes the a.e. clock. No authoritative theorem concludes the a.e. near-zero negativity itself (catalogue searches return only consumers).

View graph