tendsto_exp_neg_mul_ofReal_atTop
plain-language theorem explainer
For a complex number a with positive real part, the map B ↦ exp(−B a) tends to zero in the complex plane as real B tends to positive infinity. Analysts formalizing frequency responses for causal exponential kernels cite this limit to justify convergence of truncated integrals. The proof reduces the complex claim to real exponential decay by equating the modulus and composing standard tendsto facts for multiplication, negation, and the exponential function.
Claim. If $a ∈ ℂ$ satisfies Re$(a) > 0$, then exp$(-B a) → 0$ as $B → +∞$ with $B ∈ ℝ$.
background
The result sits in the CausalKernelChain module, whose module documentation states the goal of formalizing the single-timescale exponential memory kernel (Debye/single-pole response), its frequency response H(iω), and the steady-state and Newtonian limits. The local setting is the Debye realization of causal kernels, where the time-domain kernel is the exponential case from the BIT kernel definition: kernel(KernelFamily.exponential, z, z0) = exp(−z/z0). Upstream results supply the norm identity norm_exp_neg_mul_ofReal and the tendsto primitives for real multiplication and the exponential map.
proof idea
The tactic proof first applies tendsto_zero_iff_norm_tendsto_zero to reduce to the modulus. It then shows B ↦ B · Re(a) tends to +∞ via tendsto_id.atTop_mul_const, negates the direction with tendsto_neg_atTop_atBot, and composes with Real.tendsto_exp_atBot to obtain real exponential decay to zero. The complex modulus is identified with the real exponential via norm_exp_neg_mul_ofReal, after which simpa closes the argument.
why it matters
The limit is invoked directly by kernel_response_limit to prove that the truncated Debye response kernel_response_trunc tends to the closed-form transfer function Δ / (1 + iωτ) as B → ∞. It thereby completes the passage from finite-horizon integrals to the full frequency response inside the causal-kernel chain. The module documentation notes that this covers only the single-pole Debye case; broader spectral densities remain outside the present formalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.