Gaussian Esscher tilted q-scale vanishes in the right-hand origin limit

Proved

AvramDividend.Classical.gaussian_esscher_tilt_vanishes_right_origin

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

avram-classicalesschergaussianorigin-zeroright-limit

For a positive Gaussian Lévy process, the q-scale function vanishes at zero and is continuous there, both already formally Proved. Any function matching its exponential Esscher tilt on positive levels therefore tends to zero as the surplus tends to zero from the right. This establishes the precise hVlim required by Gaussian right-slope normalisation without demanding V be defined at zero by that tilt.

Preamble

import Mathlib.Analysis.Complex.Exponential
import Mathlib.Topology.NhdsWithin
import Mathlib.Tactic.FunProp
import Definitions.Def_AvramDividend_Classical_SpectrallyNegativeLevy
import Definitions.Def_AvramDividend_Classical_ScaleFunction
import Theorems.Thm_AvramDividend_Classical_scaleFunction_zero_origin_gaussian_without_standing
import Theorems.Thm_AvramDividend_Classical_scaleFunction_continuous_of_zero_origin
open AvramDividend.Classical MeasureTheory Set Filter
open scoped Topology NNReal ENNReal

Formal statement

namespace AvramDividend.Classical
/-- A positive Gaussian Esscher-tilted scale function vanishes in the right-hand origin limit. -/
theorem gaussian_esscher_tilt_vanishes_right_origin
    {Ω : Type*} [mΩ : MeasurableSpace Ω]
    {P : Measure Ω} {𝓕 : Filtration ℝ≥0 mΩ}
    (X : SpectrallyNegativeLevy P 𝓕)
    (q : ℝ) (hq : 0 < q)
    (W : ℝ → ℝ) (hW : IsScaleFunction X q W)
    (hσ : 0 < X.σ) (φ : ℝ) (V : ℝ → ℝ)
    (hV : ∀ x : ℝ, 0 < x → V x = Real.exp (-(φ * x)) * W x) :
    Tendsto V (𝓝[>] (0 : ℝ)) (𝓝 0) := by
  sorry
end AvramDividend.Classical

Source

Proved Gaussian scale zero-origin theorem and global continuity, exponential continuity, filter eventually equality on (0,infinity).

View graph