Stopped-history Markov future-reward lower bound transfers to the killed record expectation

Proved

AvramDividend.Classical.levy_killed_record_expectation_ge_markov_reward

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

For a finite Lévy stopping time, a past-observable survival event, and a measurable nonnegative future reward, suppose the actual killed first-record reward is pointwise at least the past discount times the shifted future reward on that event. Then the expected actual killed weight is at least the past discounted survival expectation times the independent fresh-path reward expectation. This is the expectation-level lower-comparison bridge for the q-scale regenerative step.

Preamble

import Mathlib.MeasureTheory.Integral.Lebesgue.Basic
import Theorems.Thm_AvramDividend_Classical_levy_finiteStopping_killedDiscount_futureReward_factor

open MeasureTheory ProbabilityTheory Set Classical
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.levy_killed_record_expectation_ge_markov_reward
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (τ : Ω → ℝ≥0)
    (hτ : ∀ s : ℝ≥0, MeasurableSet[𝓕 s] {ω : Ω | τ ω ≤ s})
    (A : Set Ω)
    (hA : MeasurableSet[
      (isStoppingTime_withTop_of_le_events τ hτ).measurableSpace] A)
    (hAfine : MeasurableSet A)
    (hτfine : Measurable τ)
    (discount : ℝ≥0 → ℝ≥0∞) (hd : Measurable discount)
    (reward : (ℝ≥0 → ℝ) → ℝ≥0∞) (hr : Measurable reward)
    (killedWeight : Ω → ℝ≥0∞)
    (hLower : ∀ ω : Ω,
      (if ω ∈ A then discount (τ ω) *
        reward (fun t : ℝ≥0 =>
          X.X (τ ω + t) ω - X.X (τ ω) ω)
        else 0) ≤ killedWeight ω) :
    (∫⁻ ω, if ω ∈ A then discount (τ ω) else 0 ∂P) *
      (∫⁻ ω, reward (fun t : ℝ≥0 => X.X t ω) ∂P) ≤
        (∫⁻ ω, killedWeight ω ∂P) := by sorry

Source

Avram, Palmowski and Pistorius (2007), Proposition 1; stopped Lévy strong-Markov reward factorisation.

View graph