Measurability of the full-history killed q-scale payoff for any measurable initial reserve

Proved

AvramDividend.Classical.chat04_full_history_killed_scale_payoff_measurable

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

full-historykilled-scalemeasurablerenewaltwo-sided-exit

For any q-scale function W, finite horizon T, and measurable possibly random reserve H, the terminal ENNReal-valued discounted scale payoff killed by continuous-time ruin throughout [0,T] is measurable. Establishes the precise integrand measurability needed by chat04_unbounded_killed_survival_discounted_scale_expectation and two_sided_exit_stopped_scale_identity, without zero-origin assumptions or positive-reserve restrictions.

Preamble

import Mathlib.MeasureTheory.MeasurableSpace.Constructions
import Mathlib.MeasureTheory.Constructions.BorelSpace.Real
import Mathlib.Topology.Instances.ENNReal.Lemmas
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Theorems.Thm_AvramDividend_Classical_chat04_random_reserve_closed_survival_measurable
import Theorems.Thm_AvramDividend_Classical_chat04_scaleFunction_measurable_of_punctured_continuity

open MeasureTheory
open scoped NNReal ENNReal
attribute [local instance] Classical.propDecidable
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.chat04_full_history_killed_scale_payoff_measurable
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (H : Ω → ℝ) (hH : Measurable H) (T : ℝ≥0)
    (q : ℝ) (W : ℝ → ℝ) (hW : IsScaleFunction X q W) :
    Measurable (fun ω =>
      if ∀ s : ℝ≥0, s ≤ T → 0 ≤ H ω + X.X s ω
      then ENNReal.ofReal
        (Real.exp (-(q * (T : ℝ))) * W (H ω + X.X T ω))
      else (0 : ℝ≥0∞)) := by sorry

Source

Proved random-reserve closed-horizon survival measurability and Proved Borel measurability of the q-scale function.

View graph