Global pointwise q-scale generator harmonicity at every positive reserve for bounded-variation Lévy processes

Proved

AvramDividend.Classical.bv_scale_generator_q_harmonic_positive_global_ws01b

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

avram-classicalbounded-variationgenerator-harmonicitytwo-sided-exitws01b

For any standing bounded-variation spectrally negative Lévy process and q>0 with q-scale function W, prove the generator is integrable and ΓW=qW at every positive reserve, with no fixed barrier or optimal-barrier assumptions. Follows by applying the canonically proved arbitrary-barrier generator result at a=y+1.

Preamble

import Definitions.Def_AvramDividend_Classical_SpectrallyNegativeLevy
import Definitions.Def_AvramDividend_Classical_ScaleFunction
import Theorems.Thm_AvramDividend_Classical_bv_scale_generator_q_harmonic_all_barriers_ws01b
import Mathlib.Tactic.Linarith
open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.bv_scale_generator_q_harmonic_positive_global_ws01b
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (hX : X.Standing)
    (q : ℝ) (hq : 0 < q)
    (W : ℝ → ℝ) (hW : IsScaleFunction X q W)
    (hBV : X.BoundedVariation) :
    ∀ y : ℝ, 0 < y →
      X.GeneratorIntegrable W y ∧ X.generator W y = q * W y := by sorry

Source

Avram, Palmowski and Pistorius (2007), q-scale harmonicity; corollary of the canonically Proved ws01b all-barrier generator theorem UUID 554ee8ff-e1e6-463b-bb9f-9ea5f24cb169.

View graph