Drift-volume payout on prescribed payment times equals strict positive-time survival integral

Proved

AvramDividend.Classical.paymentTimes_volume_lintegral_eq_strict_survival

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

avram-classicallebesguemeasure-theorystrict-survivalzero-barrier

For any extended nonnegative ruin horizon, integration against Lebesgue time on the actual original paymentTimes set coincides with integration over strictly positive real times of the same weight restricted to survival. The only difference between these sets is the possible singleton time zero, which has Lebesgue measure zero. This deterministic lemma handles zero and infinite horizons without assumptions on the dividend process.

Preamble

import Theorems.Thm_AvramDividend_Classical_paymentTimes_measurable
import Mathlib.MeasureTheory.Integral.Lebesgue.Basic
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic

open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.paymentTimes_volume_lintegral_eq_strict_survival
    (σ : ℝ≥0∞) (w : ℝ → ℝ≥0∞) :
    (∫⁻ t in paymentTimes σ, w t ∂volume) =
    (∫⁻ t in Ioi (0 : ℝ),
      (if ENNReal.ofReal t < σ then w t else 0) ∂volume) := by sorry

Source

Mathlib Lebesgue indicator integration and Prove2Me paymentTimes measurable; canonical Avram Dividend dividend-payment convention.

View graph