Payment times up to ruin are exhausted by deterministic integer horizons

Proved

AvramDividend.Classical.paymentTimes_eq_iUnion_nat_horizons

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

avram-classicaldividendslocalisationmonotone-convergencepayment-times

For every extended nonnegative ruin time σ, the dividend-payment set [0,σ) together with the time-zero lump sum is the increasing union of the same payment set stopped at deterministic integer horizons n. This is the set-exhaustion step used when applying monotone convergence to pass from finite-horizon verification inequalities to the full dividend value.

Preamble

import Mathlib
import Definitions.Def_AvramDividend_Classical_DividendStrategy

open MeasureTheory Set
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.paymentTimes_eq_iUnion_nat_horizons
    (σ : ℝ≥0∞) :
    paymentTimes σ =
      ⋃ n : ℕ, paymentTimes (min σ (n : ℝ≥0∞)) := by sorry

Source

Deterministic set-theoretic component of the monotone-convergence passage following equation (5.13) in Avram, Palmowski and Pistorius (2007), Proposition 4(i), Section 5.4.

View graph