Strict separation of finite upward-record times at different positive levels

Proved

AvramDividend.Classical.firstUpcrossing_finite_attained_times_strict

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

avramdividendbarrier-valuationstopped-recordstrict-passage

On a spectrally negative Lévy path, the finite first strict-passage times of two record levels b<c with b>=0 are strictly ordered. The accepted weak monotonicity of finite passage clocks gives u<=v; if they coincided, the accepted no-positive-overshoot theorem would force the path to equal both b and c at the same time. This rules out zero-duration renewal cells for positive record increments, independently of the strong-Markov and q-scale exit-transform identities.

Preamble

import Mathlib.Tactic.Linarith
import Theorems.Thm_AvramDividend_Classical_firstUpcrossing_finite_attained_times_mono
import Theorems.Thm_AvramDividend_Classical_firstUpcrossing_value_eq_threshold

open MeasureTheory Set
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.firstUpcrossing_finite_attained_times_strict
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (ω : Ω)
    (b c : ℝ) (hb : 0 ≤ b) (hbc : b < c)
    (u v : ℝ≥0)
    (hu : (u : ℝ≥0∞) =
      (⨅ (r : ℝ≥0) (_ : b < X.X r ω), (r : ℝ≥0∞)))
    (hv : (v : ℝ≥0∞) =
      (⨅ (r : ℝ≥0) (_ : c < X.X r ω), (r : ℝ≥0∞))) : (u : ℝ) < (v : ℝ) := by sorry

Source

Avram, Palmowski and Pistorius (2007), Proposition 1, reflected running-supremum renewal cells. Follows from proved firstUpcrossing_finite_attained_times_mono and firstUpcrossing_value_eq_threshold at the pinned revision.

View graph