transfer_function_complex
plain-language theorem explainer
This definition supplies the complex frequency response H(iω) = 1 + Δ/(1 + iωτ) for the single-pole Debye kernel. Researchers formalizing memory effects or dissipation in gravitational models cite it when converting the time-domain exponential kernel into its frequency-domain counterpart. It is supplied as a direct algebraic expression that instantiates the fields of the TransferFunction structure.
Claim. For a single-pole transfer function structure with DC enhancement parameter Δ and memory timescale τ > 0, the complex-valued response at real frequency ω is given by $1 + Δ / (1 + i ω τ)$.
background
The module formalizes the causal-kernel chain from the time-domain exponential (Debye) kernel Γ(t) = (Δ/τ) exp(−t/τ) for t ≥ 0 to its frequency response and limits. The key imported structure is TransferFunction, which packages Δ (the DC enhancement, equal to w − 1) together with the positive timescale τ. Upstream, the exponential kernel itself appears in BITKernelFamilies.kernel under the exponential case and in CaldeiraLeggett, where the same structure is introduced with the explicit form H(iω) = 1 + Δ/(1 + iωτ⋆).
proof idea
One-line definition that directly encodes the standard single-pole complex response using the Δ and τ fields of the supplied TransferFunction structure.
why it matters
It supplies the complex transfer function that the downstream theorems kernel_response_limit, response_function_is_real_part and transfer_function_eq_one_plus_kernel rely on. Those results establish that the paper’s real-valued response function is exactly the real part of this expression and that the steady-state and Newtonian limits close as expected. The declaration therefore completes the frequency-domain half of the Debye realization described in the module goal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.