Convex Laplace-type exponent has a finite right-shift secant limit at every positive interior point
ProvedAvramDividend.Classical.esscher_convex_positive_shift_right_secant_limitavram-classicalconvex-analysisesscherone-sided-derivativeroot-asymptotics
For any genuine real convex function f on [0,∞) and any φ>0, the shifted secant quotient (f(φ+h)-f(φ))/h tends to the finite Mathlib right derivative derivWithin f (Ioi φ) φ as h↓0. This does not presuppose a full two-sided HasDerivAt or differentiate the Lévy–Khintchine jump integral; it follows from the pinned convex one-sided derivative theorem and the exact slope reformulation. When a source-specific convexity proof for the actual Lévy Laplace exponent is available, it supplies the finite positive Esscher tilted slope needed for C1 root quotient asymptotics without a full derivative premise.
Preamble
import Mathlib.Analysis.Convex.Deriv import Mathlib.Topology.Order.Basic import Mathlib.LinearAlgebra.AffineSpace.Slope open Filter Set
Formal statement
theorem AvramDividend.Classical.esscher_convex_positive_shift_right_secant_limit
(f : ℝ → ℝ) (φ : ℝ) (hφ : 0 < φ)
(hconv : ConvexOn ℝ (Ici (0 : ℝ)) f) :
Tendsto (fun h : ℝ => (f (φ + h) - f φ) / h)
(nhdsWithin (0 : ℝ) (Ioi 0))
(nhds (derivWithin f (Ioi φ) φ)) := by sorrySource
Pinned Mathlib ConvexOn.hasDerivWithinAt_rightDeriv_of_mem_interior, hasDerivWithinAt_iff_tendsto_slope, slope_def_field. No Wiener–Hopf scalar assumed.