Zero-barrier optimal dividend candidate is globally continuous

Proved

AvramDividend.Classical.vcstar_continuous_of_unbounded_zero_cstar

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

avram-dividendcontinuousoptimal-barriervcstar

Under unbounded variation and zero optimal barrier, the exact vcstar candidate is globally continuous. Continuity of the actual verification candidate provides the boundary regularity needed when applying local comparison arguments.

Preamble

import Theorems.Thm_AvramDividend_Classical_unbounded_variation_zero_barrier_candidate_continuous
import Definitions.Def_AvramDividend_Classical_ScaleFunction
import Mathlib.Topology.Order.OrderClosed

open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.vcstar_continuous_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) :
    Continuous (vcstar W) := by sorry

Source

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

View graph