Exponential damping factors through finite causal convolutions

Proved

AvramDividend.Classical.exponential_causal_convolution_factorisation

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

avram-classicalcausal-convolutionexponential-dampingresolventzero-discount

Multiplying a causal convolution by an exponential damping factor equals the convolution of its exponentially damped inputs. The identity follows from exp(a+b)=exp(a)exp(b) and holds even for singular causal kernels. It converts the undamped scale-function resolvent into the exact weighted equation needed by the proved C1 transfer.

Preamble

import Definitions.Def_AvramDividend_Classical_ScaleFunction
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Mathlib.MeasureTheory.Integral.Bochner.Basic
open AvramDividend.Classical MeasureTheory Set

Formal statement

theorem AvramDividend.Classical.exponential_causal_convolution_factorisation
    (f g : ℝ → ℝ) (θ x : ℝ) :
    Real.exp (-(θ * x)) *
      (∫ s in Ioc (0 : ℝ) x, f (x - s) * g s ∂volume) =
    ∫ s in Ioc (0 : ℝ) x,
      (Real.exp (-(θ * (x - s))) * f (x - s)) *
        (Real.exp (-(θ * s)) * g s) ∂volume := by sorry

Source

Real.exp_add and MeasureTheory.integral_const_mul; application to Proved unbounded_scale_resolvent_convolution and causal_resolvent_C1_of_L1_primitive.

View graph