Zero-barrier optimal dividend candidate is monotone

Proved

AvramDividend.Classical.vcstar_monotone_of_unbounded_zero_cstar

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

avram-dividendmonotoneoptimal-barriervcstar

Under unbounded variation and zero optimal barrier, the exact vcstar candidate is monotone. Monotonicity of the actual optimal-barrier verification candidate gives the ordering property of the value function at the zero-barrier edge case.

Preamble

import Theorems.Thm_AvramDividend_Classical_unbounded_variation_zero_barrier_candidate_monotone
import Definitions.Def_AvramDividend_Classical_ScaleFunction
import Mathlib.Order.Monotone.Basic

open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.vcstar_monotone_of_unbounded_zero_cstar
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    {P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (q : ℝ) (hq : 0 < q)
    (W : ℝ → ℝ) (hW : IsScaleFunction X q W)
    (hnbv : ¬ X.BoundedVariation)
    (hc0 : cstar W = 0) :
    Monotone (vcstar W) := by sorry

Source

Previously Proved unbounded_variation_zero_barrier_candidate_monotone and the definitional equality vcstar W = barrierValue W (cstar W).toReal.

View graph