Complete stopped running-supremum dividend reward is bounded by the killed first-record series

Proved

AvramDividend.Classical.runningSup_full_stopped_reward_le_killed_record_tsum

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

avram-dividendkilled-record-gridpathwise-upperstopped-renewal

The genuine discounted Stieltjes dividend reward paid strictly before an arbitrary ruin horizon, including a zero or infinite horizon, is pathwise no greater than the complete series of killed discounted strict upward grid crossings. At zero horizon both payment and initial Stieltjes atom vanish. For positive horizons, the proved rational-prefix exhaustion and zero-atom comparison transfer the proved finite-horizon record budget to the complete stopped integral.

Preamble

import Mathlib.MeasureTheory.Integral.Lebesgue.Basic
import Mathlib.Analysis.Complex.Exponential
import Mathlib.Data.ENNReal.Real
import Theorems.Thm_AvramDividend_Classical_paymentTimes_min_zero_eq_singleton_zero
import Theorems.Thm_AvramDividend_Classical_runningSup_dividendMeasure_zero_atom
import Theorems.Thm_AvramDividend_Classical_paymentTimes_lintegral_le_of_rational_prefix_bounds
import Theorems.Thm_AvramDividend_Classical_lintegral_Ico_le_Ioc_of_zero_initial_atom
import Theorems.Thm_AvramDividend_Classical_paymentTimes_Ioc_subset_of_terminal_survival
import Theorems.Thm_AvramDividend_Classical_stopped_finite_horizon_reward_le_killed_record_tsum

open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal BigOperators

Formal statement

theorem AvramDividend.Classical.runningSup_full_stopped_reward_le_killed_record_tsum
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (ω : Ω)
    (τ : ℝ≥0∞) (q h : ℝ) (hq : 0 ≤ q) (hh : 0 < h) :
    (∫⁻ r in paymentTimes τ,
      ENNReal.ofReal (Real.exp (-(q * r)))
      ∂(dividendMeasure (runningSup X) ω)) ≤
    (∑' k : ℕ,
      if twoSidedExitUpTime X ((k : ℝ) * h) ω < τ then
        ENNReal.ofReal
          (h * Real.exp (-(q *
            (twoSidedExitUpTime X ((k : ℝ) * h) ω).toReal)))
      else 0) := by sorry

Source

Combine Proved finite pre-ruin horizon record budget, countable rational prefix exhaustion, null time-zero Stieltjes atom, Ico-to-Ioc comparison, and the surviving payment-time inclusion.

View graph