Finite-jump zero-barrier scale normalisation equals discounted first-jump dividends

Proved

AvramDividend.Classical.barrierValue_zero_of_finite_jump_normalisation

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

avram-classicalfinite-activityfinite-jumpfirst-jumpscale-functionzero-barrier

In the bounded-variation finite-jump case with drift d and negative-jump intensity λ, the standard scale boundary data W(0)=1/d and W'(0+)=(q+λ)/d² yield the discounted first-jump value d/(q+λ). This deterministic equality is one half of the zero-reflected-supremum proof. Proving the actual reflected dividend expectation and the scale boundary formulas from Standing remain separate stochastic/analytic obligations.

Preamble

import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring
import Theorems.Thm_AvramDividend_Classical_barrierValue_zero_eq_ratio_of_finite_derivZeroPlus

open AvramDividend.Classical

Formal statement

namespace AvramDividend.Classical

/-- The finite-activity zero-barrier analytic normaliser, conditional on the
    scale function origin and right-derivative identities. -/
theorem barrierValue_zero_of_finite_jump_normalisation
    (W : ℝ → ℝ) (q lam d : ℝ)
    (hd : d ≠ 0) (hql : q + lam ≠ 0)
    (hW0 : W 0 = 1 / d)
    (hWder : derivZeroPlus W = (((q + lam) / d ^ 2 : ℝ) : EReal)) :
    barrierValue W 0 0 = d / (q + lam) := by sorry

end AvramDividend.Classical

Source

Avram, Palmowski and Pistorius (2007), Proposition 1, zero-barrier calculation (3.14); https://arxiv.org/pdf/math/0702893

View graph