kernel_response_limit

formal source

 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
 176    have h : 0 < (1 / H.τ) := one_div_pos.2 H.τ_pos
 177    -- `a.re = 1/τ` since `Re(iω)=0`.
 178    simpa [ha_def, laplaceExponent] using h
 179
 180  have ha : a ≠ 0 := by
 181    have hne : a.re ≠ 0 := ne_of_gt ha_re
 182    intro h0
 183    apply hne
 184    simpa [h0]
 185
 186  -- Closed form for each truncation bound `B`.
 187  have hclosed (B : ℝ) :
 188      kernel_response_trunc H ω B =
 189        (H.Δ / H.τ : ℂ) * ((Complex.exp (B • (-a)) - 1) * (-a)⁻¹) := by
 190    -- Rewrite the integrand into the `exp (t • (-a))` shape and apply `integral_exp_smul_neg`.
 191    unfold kernel_response_trunc
 192    -- Push the real kernel into `ℂ`, and turn `Real.exp` into `Complex.exp`.
 193    simp_rw [debye_kernel]
 194    simp_rw [Complex.ofReal_mul, Complex.ofReal_div, Complex.ofReal_exp]
 195    -- Combine the two exponentials.
 196    simp_rw [← Complex.exp_add, ← mul_assoc, ← mul_left_comm, ← mul_comm]
 197    -- Pull out the constant factor and evaluate the remaining exponential integral.
 198    -- (At this point the integrand is exactly `exp (t • (-a))` after simp.)
 199    simp [ha_def, laplaceExponent, Complex.real_smul, intervalIntegral.integral_const_mul,