Every finite Esscher law has exactly the same null events as the original Lévy law

Proved

AvramDividend.Classical.chat04_esscher_finite_horizon_null_events_iff

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

esscherlevy-processesmeasure-equivalencewiener-hopf

For every deterministic horizon, every real exponential tilt parameter, and every measurable-space event A, the genuine Esscher density-weighted measure assigns zero mass to A if and only if the original Lévy measure does. Strict positivity of the Esscher Radon–Nikodym factor ensures equivalence of null sets, preserving almost-sure path regularity and the absence of positive jumps at every finite horizon.

Preamble

import Mathlib.MeasureTheory.Measure.WithDensity
import Mathlib.Probability.Process.Adapted
import Mathlib.Data.ENNReal.Real
import Mathlib.Analysis.Complex.Exponential
import Definitions.Def_AvramDividend_Classical_SpectrallyNegativeLevy
open MeasureTheory Set
open scoped NNReal ENNReal
open AvramDividend.Classical

Formal statement

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

Source

Apply the pinned Mathlib `withDensity_apply_eq_zero` and measurable positive exponential density, with `X.adapted.measurable` and ENNReal.ofReal_pos. This is finite-horizon mutual absolute continuity, not an unproved global Esscher change of measure.

View graph