The ordinary q-scale exit identity implies the actual first-record payment lower estimate

Proved

AvramDividend.Classical.killed_firstRecord_initial_lower_of_raw_exit

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

Assume the standard ordinary two-sided q-scale exit formula, weighted by exp(−qTε), for paths crossing ε before falling below ε−a, with the official first-passage clock. The established named-clock survival sandwich implies that this unscaled discounted expectation is a lower bound for the actual first upward record surviving reflected ruin. The independently Proved nonnegative payment-scaling theorem then multiplies the lower bound by ε, yielding the exact initial killed-record expectation used in the stopped renewal inequality. It leaves only the genuine q-scale exit theorem as an assumption.

Preamble

import Mathlib.MeasureTheory.Integral.Lebesgue.Basic
import Mathlib.Data.ENNReal.Real
import Mathlib.Analysis.Complex.Exponential
import Theorems.Thm_AvramDividend_Classical_named_killed_upcrossing_lower_of_raw_exit
import Theorems.Thm_AvramDividend_Classical_killed_lintegral_ofReal_scaled_lower

open MeasureTheory
open scoped NNReal ENNReal Classical
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.killed_firstRecord_initial_lower_of_raw_exit
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (q a ε : ℝ) (ha : 0 < a) (hε : 0 < ε) (W : ℝ → ℝ)
    (hRaw : (∫⁻ ω,
      if twoSidedExitUpTime X ε ω ≠ ∞ ∧
          (∀ t : ℝ≥0, t < (twoSidedExitUpTime X ε ω).toNNReal →
            ε - a ≤ X.X t ω) then
        ENNReal.ofReal (Real.exp
          (-(q * (twoSidedExitUpTime X ε ω).toReal)))
      else 0 ∂P) =
      ENNReal.ofReal (W (a - ε) / W a)) :
    ENNReal.ofReal (ε * (W (a - ε) / W a)) ≤
      (∫⁻ ω,
        if twoSidedExitUpTime X ((1 : ℝ) * ε) ω <
            barrierRuinTime X a ω then
          ENNReal.ofReal (ε * Real.exp
            (-(q * (twoSidedExitUpTime X ((1 : ℝ) * ε) ω).toReal)))
        else 0 ∂P) := by sorry

Source

Avram, Palmowski and Pistorius (2007), equation (3.6) and Proposition 1; combination of named first-upcrossing survival comparison and killed integral scalar homogeneity.

View graph