The negative endpoint exponential is integrable under each genuine finite-time Esscher law

Proved

AvramDividend.Classical.chat04_esscher_finite_negative_exp_integrable

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

esscherintegrabilitylevy-processesmarkov-inequality

For a spectrally negative Lévy process and finite Esscher tilt θ≥0, the random variable exp(−εX_t) is integrable under the actual finite-horizon density-weighted probability law for every ε∈[0,θ]. This upgrades the existing real integral identity to a genuine finite exponential moment suitable for nonnegative Markov and path-tail estimates.

Preamble

import Mathlib.MeasureTheory.Function.L1Space.Integrable
import Mathlib.Probability.Process.Adapted
import Mathlib.Analysis.Complex.Exponential
import Mathlib.Tactic.Ring
import Definitions.Def_AvramDividend_Classical_SpectrallyNegativeLevy
open MeasureTheory
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.chat04_esscher_finite_negative_exp_integrable
    {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω}
    {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (t : ℝ≥0) (θ ε : ℝ) (hθ : 0 ≤ θ)
    (hε : 0 ≤ ε) (hεθ : ε ≤ θ) :
    Integrable (fun ω => Real.exp (-ε * X.X t ω))
      (P.withDensity (fun ω : Ω =>
        ENNReal.ofReal
          (Real.exp (θ * X.X t ω - (t : ℝ) * X.ψ θ)))) := by sorry

Source

Apply pinned `MeasureTheory.integrable_withDensity_iff` for a measurable everywhere finite Esscher density; transform exp(−εX_t)×density into exp(−tψθ)×exp((θ−ε)X_t); the latter is integrable by the defining Lévy exponential moment at θ−ε≥0. This is independent of Wiener–Hopf.

View graph