The strict two-sided exit expectation is bounded by the killed reflected first-record reward

Proved

AvramDividend.Classical.killed_firstRecord_weight_lower_of_strict_exit

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

For any nonnegative reward depending on a path, the expected reward paid on a strict two-sided upper-first exit is bounded by the reward paid on the actual reflected-record survival event. Composes the published strict exit prefix inclusion and the independently Proved killed first-upcrossing survival comparison.

Preamble

import Mathlib.MeasureTheory.Integral.Lebesgue.Basic
import Definitions.Def_AvramDividend_Classical_TwoSidedExit
import Theorems.Thm_AvramDividend_Classical_strict_up_before_down_preserves_lower_prefix
import Theorems.Thm_AvramDividend_Classical_named_killed_upcrossing_lower_of_raw_exit

open MeasureTheory
open scoped NNReal ENNReal Classical
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.killed_firstRecord_weight_lower_of_strict_exit
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (a b : ℝ) (ha : 0 < a) (hb : 0 ≤ b)
    (w : Ω → ℝ≥0∞) (k : ℝ≥0∞)
    (hExit : (∫⁻ ω,
      if twoSidedExitUpTime X b ω <
          twoSidedExitDownTime X (b - a) ω
      then w ω else 0 ∂P) = k) :
    k ≤ (∫⁻ ω,
      if twoSidedExitUpTime X b ω < barrierRuinTime X a ω
      then w ω else 0 ∂P) := by sorry

Source

Avram, Palmowski and Pistorius (2007), two-sided exit and Proposition 1. Pure pathwise expectation bridge.

View graph