kernel_response_trunc

formal source

 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
 167
 168/-- Truncated Debye-kernel response tends to its closed form as `B → ∞`. -/
 169theorem kernel_response_limit (H : CaldeiraLeggett.TransferFunction) (ω : ℝ) :
 170    Filter.Tendsto (fun B => kernel_response_trunc H ω B) Filter.atTop
 171      (nhds ((H.Δ : ℂ) / ((1 : ℂ) + Complex.I * (ω : ℂ) * (H.τ : ℂ)))) := by
 172  -- Abbreviate `a = (1/τ) + iω`.
 173  set a : ℂ := laplaceExponent H ω with ha_def
 174
 175  have ha_re : 0 < a.re := by