The exact zero-barrier dividend identity yields global zero-cap verification

Proved

AvramDividend.Classical.zero_cap_value_upper_bound_all_of_boundary_identity

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

avram-dividendboundary-identityglobal-verificationzero-cap

For any standing spectrally negative Levy process and valid positive-discount scale function, the exact dividend value identity at the zero barrier and zero reserve already implies the upper verification inequality for the zero-capped dividend problem from every nonnegative initial reserve. No Gaussian, bounded-variation, tilt, or path-regularity premises are needed beyond the displayed exact boundary identity. This result can be applied as soon as the open zero-barrier identity is proved.

Preamble

import Theorems.Thm_AvramDividend_Classical_barrierValue_zero_zero_nonneg
import Theorems.Thm_AvramDividend_Classical_zero_cap_value_at_zero_upper_bound_of_boundary
import Theorems.Thm_AvramDividend_Classical_zero_cap_value_upper_bound_of_zero_bound

open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.zero_cap_value_upper_bound_all_of_boundary_identity
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (hX : X.Standing)
    (q : ℝ) (hq : 0 < q) (W : ℝ → ℝ)
    (hW : IsScaleFunction X q W)
    (hboundary : dividendValue X q 0 (barrierStrategy X 0 0) =
      ENNReal.ofReal (barrierValue W 0 0)) :
    ∀ x : ℝ, 0 ≤ x →
      valueFunctionLe X q 0 x ≤ ENNReal.ofReal (barrierValue W 0 x) := by sorry

Source

Canonically Proved barrier value nonnegativity eb66042a-0dc2-4d0c-9514-5dd05be55c16, boundary-zero comparison d58a54f2-7f8b-4467-b485-93506d163ab8 and reserve-transfer lemma a77b926c-06ed-4fc1-a8f4-945437968469.

View graph