Unbounded q-scale Esscher root and exponential ratio bound from corrected exits

Proved

AvramDividend.Classical.unbounded_esscher_ratio_bound_of_corrected_exit

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

avram-classicalesscherfirst-passageratio-boundscale-functions

For q>0 and unbounded variation, assume the canonical killed two-sided exit identity on nonnegative reserves. Then a positive Esscher root φ exists and satisfies W(x)/W(y) ≤ exp(-φ(y−x)) whenever 0<x≤y. This proves the exact conclusion of the Open root-connected unbounded_esscher_ratio_bound milestone under the single source-faithful corrected exit prerequisite. The proof imports previously Proved root existence and fixed-root exit decay, and divides by the canonically positive W(y).

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_positive_tilt_of_corrected_exit
import Theorems.Thm_AvramDividend_Classical_unbounded_fixedroot_decay_of_corrected_exit_identity
import Mathlib.Algebra.Order.Field.Basic
open AvramDividend.Classical MeasureTheory Set
open scoped NNReal ENNReal

Formal statement

theorem AvramDividend.Classical.unbounded_esscher_ratio_bound_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)) :
    ∃ (φ : ℝ) (hφ : 0 < φ) (hroot : X.ψ φ = q),
      ∀ x y : ℝ, 0 < x → x ≤ y →
        W x / W y ≤ Real.exp (-(φ * (y - x))) := by sorry

Source

Avram Palmowski Pistorius (2007) corrected killed two-sided exit identity and positive Esscher root comparison.

View graph