Strict positivity of unbounded-variation scale-function self-convolution

Proved

AvramDividend.Classical.unbounded_scale_self_convolution_positive

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

avram-classicalconvolutionpositivityscale-functionunbounded-variation

For any scale function of a spectrally negative Lévy process with unbounded variation, its causal self-convolution is strictly positive at each strictly positive reserve. This does not require a second discount parameter and supplies the positivity input for studying higher discount sensitivity.

Preamble

import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
import Mathlib.Tactic.Linarith
import Theorems.Thm_AvramDividend_Classical_scaleFunction_strict_pos_of_unbounded_variation
open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

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

Source

Direct application of the interval-integral positivity theorem, continuity and strict positivity of q-scale functions on the positive half-line.

View graph