Discounted terminal partial record cell bounded by its left first-record weight

Proved

AvramDividend.Classical.runningSup_terminal_partial_record_clock_discount_upper

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

avram-dividendfirst-passagepathwise-upperstopped-renewalterminal-record-cell

If u is a finite first upcrossing of level b and t is strictly before the finite first upcrossing of b+h, the stopped running-supremum increase on (u,t] is at most h. Nonnegative discount makes the discounted Stieltjes reward on that terminal partial record cell at most h exp(-q u). This is the missing terminal-cell estimate needed alongside the accepted complete-record-cell upper bounds.

Preamble

import Mathlib.Analysis.Complex.Exponential
import Mathlib.MeasureTheory.Integral.Lebesgue.Basic
import Theorems.Thm_AvramDividend_Classical_firstUpcrossing_attains_peak
import Theorems.Thm_AvramDividend_Classical_firstUpcrossing_runningSup_sub_path_eq_zero
import Theorems.Thm_AvramDividend_Classical_runningSup_pre_firstUpcrossing_between
import Theorems.Thm_AvramDividend_Classical_runningSup_discounted_partial_record_cell_upper

open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal Classical

Formal statement

theorem AvramDividend.Classical.runningSup_terminal_partial_record_clock_discount_upper
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (ω : Ω)
    (q b h : ℝ) (hq : 0 ≤ q) (hb : 0 ≤ b) (hh : 0 ≤ h)
    (u v t : ℝ≥0)
    (hu : (u : ℝ≥0∞) =
      (⨅ (r : ℝ≥0) (_ : b < X.X r ω), (r : ℝ≥0∞)))
    (hv : (v : ℝ≥0∞) =
      (⨅ (r : ℝ≥0) (_ : b + h < X.X r ω), (r : ℝ≥0∞)))
    (ht : t < v) :
    (∫⁻ r,
      if r ∈ Set.Ioc (u : ℝ) (t : ℝ)
      then ENNReal.ofReal (Real.exp (-(q * r))) else 0
      ∂(dividendMeasure (runningSup X) ω)) ≤
      ENNReal.ofReal (Real.exp (-(q * (u : ℝ)))) * ENNReal.ofReal h := by sorry

Source

First-upcrossing peak attainment, equality of running supremum and process at first record, pre-upcrossing running-sup bound, and the accepted discounted partial-record-cell lemma. Supports root c6c3b1d0-2c2f-41ce-a5a0-2771efcc3a69.

View graph