Any shifted future record witness bounds the next original first-passage clock

Proved

AvramDividend.Classical.nextRecord_upclock_le_shifted_witness

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

Suppose the Lévy path is exactly at its attained record level b at time u. If the shifted future path rises strictly above ε during the next time interval t, then the official strict first upward crossing time of the next level b+ε is at most u+t. This is the fundamental witness inclusion for transferring shifted Markov future-path upper exits back to the original first-record clock.

Preamble

import Mathlib.Order.ConditionallyCompleteLattice.Basic
import Mathlib.Tactic.Linarith
import Definitions.Def_AvramDividend_Classical_TwoSidedExit

open MeasureTheory
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.nextRecord_upclock_le_shifted_witness
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (b ε : ℝ) (u t : ℝ≥0) (ω : Ω)
    (hAt : X.X u ω = b)
    (hNext : ε < X.X (u + t) ω - X.X u ω) :
    twoSidedExitUpTime X (b + ε) ω ≤ ((u + t : ℝ≥0) : ℝ≥0∞) := by sorry

Source

Avram, Palmowski and Pistorius (2007), Proposition 1, strong-Markov renewal across attained running-supremum records.

View graph