Local Esscher-tilted q-scale logarithmic derivative order from corrected exits

Proved

AvramDividend.Classical.unbounded_tilted_scale_cross_derivative_of_corrected_exit

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

avram-classicalesscherfirst-passagelog-concavityscale-functions

For an unbounded-variation spectrally negative Lévy process, its corrected killed two-sided exit-scale identity implies the cross-derivative inequality for the Esscher-tilted q-scale function V(z)=exp(-φz)W(z), for any real tilt φ and any ordered positive points x≤y where W is differentiable. In particular V'(y)V(x)≤V'(x)V(y) with no global C1 assumption. The proof imports the verified corrected-exit cross derivative theorem and a verified generic exponential tilt preservation theorem, supplying a local analytic consequence for the open full Esscher-tilted log-concavity milestone.

Preamble

import Definitions.Def_AvramDividend_Classical_SpectrallyNegativeLevy
import Definitions.Def_AvramDividend_Classical_ScaleFunction
import Definitions.Def_AvramDividend_Classical_TwoSidedExitCorrected
import Theorems.Thm_AvramDividend_Classical_unbounded_scale_cross_derivative_of_corrected_exit
import Theorems.Thm_AvramDividend_Classical_exponential_tilt_preserves_cross_derivative_order
import Mathlib.Analysis.Calculus.Deriv.Basic
open AvramDividend.Classical MeasureTheory
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.unbounded_tilted_scale_cross_derivative_of_corrected_exit
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    {P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (q : ℝ) (hq : 0 < q)
    (W : ℝ → ℝ) (hW : IsScaleFunction X q W)
    (hnbv : ¬ X.BoundedVariation)
    (hExit : ∀ a x : ℝ, 0 < a → 0 < x → x ≤ a →
      twoSidedExitExpectationCorrected X q a x =
        ENNReal.ofReal (W x / W a))
    (φ x y : ℝ) (hx : 0 < x) (hxy : x ≤ y)
    (hdx : DifferentiableAt ℝ W x)
    (hdy : DifferentiableAt ℝ W y) :
    deriv (fun z : ℝ => Real.exp (-φ * z) * W z) y *
        (Real.exp (-φ * x) * W x) ≤
      deriv (fun z : ℝ => Real.exp (-φ * z) * W z) x *
        (Real.exp (-φ * y) * W y) := by sorry

Source

Avram Palmowski Pistorius (2007) corrected two-sided exit scale formula and deterministic exponential Esscher tilting of logarithmic derivatives.

View graph