Esscher exponential tilt preserves pointwise cross-derivative order

Proved

AvramDividend.Classical.exponential_tilt_preserves_cross_derivative_order

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

avram-classicalderivative-ratioesscherlog-concavityscale-functions

For any real differentiable function f at two points x and y, the cross-multiplied slope inequality f'(y)f(x)≤f'(x)f(y) is preserved by multiplication by exp(-φz), for any real Esscher exponent φ. The proof computes the derivative of the tilted function and cancels equal logarithmic-derivative shifts algebraically. This enables the root-connected unbounded q-scale derivative comparison from corrected first passage to transfer to tilted scales without assuming global C1 continuity.

Preamble

import Theorems.Thm_AvramDividend_Classical_esscher_exponential_derivative
import Mathlib.Analysis.Calculus.Deriv.Basic
import Mathlib.Tactic.FunProp
import Mathlib.Tactic.Ring
open AvramDividend.Classical

Formal statement

theorem AvramDividend.Classical.exponential_tilt_preserves_cross_derivative_order
    (f : ℝ → ℝ) (φ x y : ℝ)
    (hcross : deriv f y * f x ≤ deriv f x * f y)
    (hdx : DifferentiableAt ℝ f x)
    (hdy : DifferentiableAt ℝ f y) :
    deriv (fun z : ℝ => Real.exp (-φ * z) * f z) y *
        (Real.exp (-φ * x) * f x) ≤
      deriv (fun z : ℝ => Real.exp (-φ * z) * f z) x *
        (Real.exp (-φ * y) * f y) := by sorry

Source

Exact Esscher exponential derivative and local product rule; apply to q-scale logarithmic concavity under the Avram dividend two-sided exit identity.

View graph