Scale-function discount secant slope equals a causal convolution

Proved

AvramDividend.Classical.unbounded_scale_discount_secant_convolution

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

avram-classicalconvolutiondiscountresolventscale-functionsensitivity

For any two distinct nonnegative discount rates of an unbounded-variation spectrally negative Lévy process, the finite difference quotient of their scale functions in discount equals their positive causal convolution. This gives an exact starting point for differentiability and sensitivity analysis in the discount parameter.

Preamble

import Mathlib.Tactic.Linarith
import Theorems.Thm_AvramDividend_Classical_unbounded_scale_resolvent_convolution
open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.unbounded_scale_discount_secant_convolution
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    {P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕) (hnbv : ¬ X.BoundedVariation)
    (q₁ q₂ : ℝ) (hq₁ : 0 ≤ q₁) (hq₂ : 0 ≤ q₂) (hq : q₁ < q₂)
    (W₁ W₂ : ℝ → ℝ)
    (hW₁ : IsScaleFunction X q₁ W₁) (hW₂ : IsScaleFunction X q₂ W₂) :
    ∀ x : ℝ, 0 < x →
      (W₂ x - W₁ x) / (q₂ - q₁) =
        ∫ s in Ioc (0 : ℝ) x, W₁ s * W₂ (x - s) := by sorry

Source

Algebraic consequence of the Proved unbounded_scale_resolvent_convolution and strict positivity of the difference in discounts.

View graph