transfer_function_complex

formal source

 124\]
 125This matches the structure in `Gravity.CaldeiraLeggett.TransferFunction`, but is a complex-valued
 126frequency response rather than its extracted real part. -/
 127def transfer_function_complex (H : CaldeiraLeggett.TransferFunction) (ω : ℝ) : ℂ :=
 128  (1 : ℂ) + (H.Δ : ℂ) / ((1 : ℂ) + Complex.I * (ω : ℂ) * (H.τ : ℂ))
 129
 130
 131/-- The Debye exponential kernel for a single-timescale response:
 132\[
 133\Gamma(t) = \frac{\Delta}{\tau} e^{-t/\tau},\quad t \ge 0.
 134\]
 135We treat it as a function on `ℝ` and integrate it on `[0,B]` (then take `B → ∞`). -/
 136def debye_kernel (H : CaldeiraLeggett.TransferFunction) (t : ℝ) : ℝ :=
 137  (H.Δ / H.τ) * Real.exp (-t / H.τ)
 138
 139
 140/-- Truncated (finite-horizon) frequency response contribution from the Debye kernel:
 141\[
 142K_B(\omega)=\int_0^B \Gamma(t)\,e^{-i\omega t}\,dt.
 143\]
 144The full transfer function is `1 + K_∞(ω)`. -/
 145def kernel_response_trunc (H : CaldeiraLeggett.TransferFunction) (ω B : ℝ) : ℂ :=
 146  ∫ t in (0 : ℝ)..B,
 147    ((debye_kernel H t : ℝ) : ℂ) * Complex.exp (-(Complex.I * (ω : ℂ) * (t : ℂ)))
 148
 149
 150/-!
 151### Bridge lemma (frequency-domain closed form)
 152
 153For τ>0, define `a = (1/τ) + i ω`. Then
 154
 155  exp(-t/τ) * exp(-i ω t) = exp(-(a * t)).
 156
 157The truncated integral can be evaluated in closed form using `integral_exp_smul_neg`,