kernel_response_limit
plain-language theorem explainer
The theorem shows that the truncated Debye-kernel response of a single-pole transfer function converges to its closed-form frequency expression as the upper integration limit tends to infinity. Modelers of dissipative systems with exponential memory would cite the result to justify replacing the time-domain integral by the algebraic transfer function. The proof first obtains an explicit antiderivative for each finite truncation via the exponential integral lemma, then passes to the limit using the known decay of the complex exponential when the
Claim. Let $H$ be a transfer function with real parameters $Δ$ and $τ>0$. For any real frequency $ω$, the limit as the truncation bound $B$ tends to infinity of the truncated response equals $Δ/(1+iωτ)$ in the complex numbers.
background
The module formalizes the single-timescale exponential (Debye) memory kernel and its frequency-domain transfer function. The kernel itself is the exponential case of the BIT kernel family, Real.exp(-z/z0). A transfer function record supplies the two real parameters $Δ$ and $τ$ that appear in the target limit expression. Upstream lemmas supply the closed-form integral of exp(t·(-a)) when Re(a)>0 and the corresponding tendsto statement for the exponential term as the upper limit tends to infinity.
proof idea
The tactic proof first defines the complex Laplace exponent a = 1/τ + iω and proves Re(a)>0. It then derives the closed-form expression for the truncated integral by rewriting the integrand and invoking the exponential-integral lemma. The limit B→∞ is obtained by applying the known tendsto for exp(B·(-a)) to zero, subtracting the constant 1, multiplying by the inverse, scaling by the prefactor Δ/τ, and finally simplifying the resulting algebraic expression back to Δ/(1+iωτ) via field arithmetic.
why it matters
The result supplies the missing limit step that justifies passage from the time-domain truncated kernel to the steady-state transfer function inside the causal-kernel chain. It therefore supports the frequency-domain calculations required by the gravity module and the single-pole case of the paper's Debye realization. No downstream theorems yet consume the declaration, indicating it is an intermediate building block whose use sites remain to be added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.