Product-rule derivative for exponentially weighted scale kernels

Proved

AvramDividend.Classical.exp_weighted_scale_hasDerivAt

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

avram-classicalderivativeexponential-dampinggaussian-branchzero-discount

The weighted scale kernel g_theta(x)=exp(-theta x)W(x) has derivative g_theta'(x)=exp(-theta x)(W'(x)-theta W(x)) at every differentiability point. This exact product rule connects the proved weighted derivative integrability to a boundary-safe fundamental theorem of calculus.

Preamble

import Definitions.Def_AvramDividend_Classical_ScaleFunction
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Mathlib.Analysis.Calculus.Deriv.Basic
open AvramDividend.Classical MeasureTheory Set

Formal statement

theorem AvramDividend.Classical.exp_weighted_scale_hasDerivAt
    (W : ℝ → ℝ) (θ x : ℝ) (hW : DifferentiableAt ℝ W x) :
    HasDerivAt (fun y : ℝ => Real.exp (-(θ * y)) * W y)
      (Real.exp (-(θ * x)) * (deriv W x - θ * W x)) x := by sorry

Source

Real.hasDerivAt_exp, HasDerivAt.const_mul, HasDerivAt.comp and HasDerivAt.mul in Mathlib.

View graph