Global-in-discount continuity of the q-scale family at every real reserve

Proved

AvramDividend.Classical.unbounded_scale_discount_family_continuousOn_nonnegative_all_reserves

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

all-reservesavram-classicalcontinuitydiscountnonnegative-halflinescale-function

The q-scale function of an unbounded-variation spectrally negative Lévy process depends continuously on any nonnegative discount parameter at every real reserve, including the zero origin and negative reserves. The result is obtained by localising to [0,q+1] and invoking the proved compact-discount all-reserve continuity theorem.

Preamble

import Mathlib.Tactic.Linarith
import Mathlib.Topology.ContinuousOn
import Mathlib.Topology.Order.Basic
import Theorems.Thm_AvramDividend_Classical_unbounded_scale_discount_family_continuousOn_all_reserves
open AvramDividend.Classical MeasureTheory Set Filter Topology
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.unbounded_scale_discount_family_continuousOn_nonnegative_all_reserves
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    {P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (hnbv : ¬ X.BoundedVariation)
    (W : ℝ → ℝ → ℝ)
    (hW : ∀ q : ℝ, 0 ≤ q → IsScaleFunction X q (W q)) :
    ∀ x : ℝ,
      ContinuousOn (fun q : ℝ => W q x) (Ici (0 : ℝ)) := by sorry

Source

Local-to-global topological argument from the canonical Proved continuousOn_all_reserves theorem.

View graph