debye_kernel

formal source

 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`,
 158then the `B → ∞` limit is obtained from `tendsto_exp_neg_mul_ofReal_atTop`.
 159-/
 160
 161/-! ### Laplace transform limit and transfer-function bridge -/
 162
 163/-- The complex exponent `a = (1/τ) + i ω` appearing in the Debye kernel transform. -/
 164def laplaceExponent (H : CaldeiraLeggett.TransferFunction) (ω : ℝ) : ℂ :=
 165  ((1 / H.τ : ℝ) : ℂ) + Complex.I * (ω : ℂ)
 166