Unbounded-variation stopped scale harmonicity for nonpositive upper barrier

Proved

AvramDividend.Classical.chat04_unbounded_stopped_scale_nonpositive_upper

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

fluctuation-theorylevy-processessource-faithful-childtwo-sided-exitunbounded-variation

For a spectrally negative Levy process of unbounded variation, q>0, a q-scale function W, and starting reserve x≤a≤0, the entire strict two-sided stopped discounted W payoff equals W(x). The weak-endpoint branch follows from the accepted payoff factorisation and the fact that W vanishes on (-infinity,0] in unbounded variation. This reduces the canonical general-reserve harmonicity parent to the positive-upper-barrier case.

Preamble

import Mathlib.MeasureTheory.Integral.Lebesgue.Add
import Definitions.Def_AvramDividend_Classical_TwoSidedExit
import Definitions.Def_AvramDividend_Classical_ScaleFunction
import Theorems.Thm_AvramDividend_Classical_chat04_strict_two_sided_exit_terminal_payoff_factorisation_unbounded
import Theorems.Thm_AvramDividend_Classical_chat04_scale_zero_origin_of_unbounded_variation

open MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

namespace AvramDividend.Classical
theorem chat04_unbounded_stopped_scale_nonpositive_upper
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (hnbv : ¬ X.BoundedVariation)
    (q : ℝ) (hq : 0 < q)
    (W : ℝ → ℝ) (hW : IsScaleFunction X q W)
    (a x : ℝ) (hxa : x ≤ a) (ha : a ≤ 0) :
    (∫⁻ ω, (if twoSidedExitUpTime X (a - x) ω <
          twoSidedExitDownTime X (-x) ω then
        ENNReal.ofReal
          (Real.exp (-(q * ENNReal.toReal (twoSidedExitUpTime X (a - x) ω)))) *
          ENNReal.ofReal
            (W (x + X.X (twoSidedExitUpTime X (a - x) ω).toNNReal ω))
      else 0) + (if twoSidedExitDownTime X (-x) ω <
          twoSidedExitUpTime X (a - x) ω then
        ENNReal.ofReal
          (Real.exp (-(q * ENNReal.toReal (twoSidedExitDownTime X (-x) ω)))) *
          ENNReal.ofReal
            (W (x + X.X (twoSidedExitDownTime X (-x) ω).toNNReal ω))
      else 0) ∂P) = ENNReal.ofReal (W x) := by sorry
end AvramDividend.Classical

Source

Avram, Palmowski and Pistorius (2007), arXiv:math/0702893, scale-function support and unbounded-variation zero boundary. Prove2Me accepted strict terminal payoff factorisation and accepted scale zero origin.

View graph