integral_exp_smul_neg
plain-language theorem explainer
The declaration supplies the closed-form evaluation of the finite integral ∫ from 0 to B of exp(t • (-a)) dt, equaling (exp(B • (-a)) - 1) * (-a)^{-1} for nonzero complex a. Researchers deriving Debye kernels and transfer functions in causal response models cite this identity to convert time-domain integrals into algebraic expressions. The proof verifies the antiderivative derivative via chained HasDerivAt rules for scalar multiplication and exponentiation, applies the interval fundamental theorem of calculus, and finishes with algebraic ring-s
Claim. For nonzero $a$ in the complex numbers and real $B$, the integral from 0 to $B$ of the complex exponential of $t$ scaled by $-a$ equals the quantity (exponential of $B$ scaled by $-a$ minus 1) multiplied by the inverse of $-a$.
background
The module formalizes the single-timescale exponential memory kernel (Debye/single-pole response) and its frequency-domain properties, with the explicit goal of converting the time-domain causal kernel into transfer functions and their steady-state and high-frequency limits. This theorem supplies the explicit antiderivative evaluation required to compute truncated kernel responses of the form ∫ from 0 to B of the kernel times exp(-i ω t) dt. The local setting restricts attention to the Debye case; broader spectral densities are noted as requiring additional Fourier or Laplace machinery not yet present.
proof idea
The proof constructs the candidate antiderivative F(t) = Complex.exp(t • (-a)) * (-a)^{-1} and verifies its HasDerivAt derivative equals the integrand by successive applications of hasDerivAt_id, HasDerivAt.smul_const, Complex.hasDerivAt_exp composed with the inner map, and HasDerivAt.mul_const. It then confirms continuity of the integrand via fun_prop, obtains interval integrability, invokes intervalIntegral.integral_eq_sub_of_hasDerivAt to recover F(B) - F(0), and rewrites the difference algebraically with simp and ring, using the nonzero assumption on a to cancel factors.
why it matters
The result is invoked by the sibling definitions kernel_response_trunc and kernel_response_limit, which build the truncated frequency response of the Debye kernel and its limit as the horizon tends to infinity. It therefore supplies the concrete computational step that closes the time-domain to frequency-domain passage in the causal-kernel chain. The module doc-comment states that this realizes the single-pole case of the broader Recognition Science program for deriving transfer functions from exponential memory kernels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.