transfer_function_eq_one_plus_kernel

formal source

 254
 255
 256/-- `transfer_function_complex` is exactly the Debye single-pole transfer function form. -/
 257theorem transfer_function_eq_one_plus_kernel (H : CaldeiraLeggett.TransferFunction) (ω : ℝ) :
 258    transfer_function_complex H ω =
 259      (1 : ℂ) + (H.Δ : ℂ) / ((1 : ℂ) + Complex.I * (ω : ℂ) * (H.τ : ℂ)) := by
 260  simp [transfer_function_complex]
 261
 262
 263/-- The paper’s real-valued response function is the real part of the complex transfer function. -/
 264theorem response_function_is_real_part (H : CaldeiraLeggett.TransferFunction) (ω : ℝ) :
 265    CaldeiraLeggett.response_function H ω = (transfer_function_complex H ω).re := by
 266  -- Unfold both sides.
 267  unfold CaldeiraLeggett.response_function transfer_function_complex
 268  -- Let the complex denominator be `w = 1 + i ω τ`.
 269  set w : ℂ := (1 : ℂ) + Complex.I * (ω : ℂ) * (H.τ : ℂ) with hw
 270  have wre : w.re = 1 := by
 271    -- `Re(i * real) = 0`.
 272    simp [hw, mul_assoc, mul_left_comm, mul_comm]
 273  have wnormSq : Complex.normSq w = 1 + (ω * H.τ) ^ (2 : ℕ) := by
 274    -- `normSq w = w.re^2 + w.im^2`, and here `w.re = 1`, `w.im = ωτ`.
 275    -- We compute directly using `normSq_apply`.
 276    have : w.im = ω * H.τ := by
 277      simp [hw, mul_assoc, mul_left_comm, mul_comm]
 278    -- Expand `normSq` and simplify.
 279    -- Use `pow_two` (as `x^2 = x*x`) in the reverse direction.
 280    calc
 281      Complex.normSq w = w.re * w.re + w.im * w.im := by
 282        simpa [Complex.normSq_apply]
 283      _ = (1 : ℝ) * 1 + (ω * H.τ) * (ω * H.τ) := by
 284        simp [wre, this]
 285      _ = 1 + (ω * H.τ) ^ (2 : ℕ) := by
 286        simp [pow_two, mul_assoc]
 287