Finite dividend barrier value from strict exit factor below one

Proved

AvramDividend.Classical.chat12_barrierSupValue_finite_of_trueExit_factor

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

Let X be a standing spectrally negative Lévy process and q,a,epsilon>0. If the true discounted strict upward-before-(-a)-downward exit expectation equals ENNReal.ofReal p for 0≤p<1, then the barrier strategy value barrierSupValue X a q is finite in ENNReal. This uses the Proved pathwise dividend Stieltjes upper bound by killed record rewards, Proved expected value upper sum, and Proved finiteness of the total expected killed-record payments. It does not require the Open q-scale-function exit identity.

Preamble

import Mathlib.MeasureTheory.Integral.Lebesgue.Basic
import Mathlib.Analysis.Complex.Exponential
import Theorems.Thm_AvramDividend_Classical_barrierSup_stopped_indicator_reward_le_killed_record_tsum
import Theorems.Thm_AvramDividend_Classical_barrierSupValue_le_sum_expected_firstRecord_budgets
import Theorems.Thm_AvramDividend_Classical_killed_firstRecord_discount_reward_measurable
import Theorems.Thm_AvramDividend_Classical_chat12_total_expected_upper_finite_of_trueExit_factor

open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.chat12_barrierSupValue_finite_of_trueExit_factor
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (hX : X.Standing)
    (q : ℝ) (hq : 0 < q) (a ε : ℝ)
    (ha : 0 < a) (hε : 0 < ε) (p : ℝ)
    (hp : 0 ≤ p) (hp1 : p < 1)
    (hExit : (∫⁻ ω, if
          (⨅ (t : ℝ≥0) (_ : ε < X.X t ω), (t : ℝ≥0∞)) <
          (⨅ (t : ℝ≥0) (_ : X.X t ω < -a), (t : ℝ≥0∞)) then
          ENNReal.ofReal (Real.exp
            (-(q * ENNReal.toReal
              (⨅ (t : ℝ≥0) (_ : ε < X.X t ω), (t : ℝ≥0∞)))))
      else 0 ∂P) = ENNReal.ofReal p) :
    barrierSupValue X a q < ∞ := by sorry

View graph