Every q-scale function is Borel measurable, even when discontinuous at the origin

Proved

AvramDividend.Classical.chat04_scaleFunction_measurable_of_punctured_continuity

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

bounded-variationkilled-semigroupmeasurablescale-functiontwo-sided-exit

The scale function of any spectrally negative Lévy process is Borel measurable on the real line, including the bounded-variation case where W(0) may be positive and W has a discontinuity at zero. Continuity at every point other than zero and removal of a singleton establish global measurability. This removes the measurable-W side assumption of the Proved chat04_countable_killed_scale_markov_tonelli identity, which feeds the stopped q-scale renewal and two-sided exit obligations.

Preamble

import Mathlib.MeasureTheory.MeasurableSpace.Constructions
import Mathlib.MeasureTheory.Constructions.BorelSpace.Real
import Mathlib.Topology.Instances.ENNReal.Lemmas
import Theorems.Thm_AvramDividend_Classical_scaleFunction_continuousAt_away_zero

open MeasureTheory
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.chat04_scaleFunction_measurable_of_punctured_continuity
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (q : ℝ) (W : ℝ → ℝ) (hW : IsScaleFunction X q W) :
    Measurable W := by sorry

Source

Proved scaleFunction_continuousAt_away_zero and Mathlib measurable_of_measurable_on_compl_singleton.

View graph