response_function_is_real_part

formal source

 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
 288  -- Reduce the real part using `Complex.div_re`.
 289  -- Since `H.Δ` is real, its imaginary part is 0.
 290  have hdiv :
 291      ((H.Δ : ℂ) / w).re = H.Δ / (1 + (ω * H.τ) ^ (2 : ℕ)) := by
 292    -- Apply `div_re` and simplify with `wre` and `wnormSq`.
 293    simp [Complex.div_re, wre, wnormSq, hw, mul_assoc, mul_left_comm, mul_comm, add_assoc,
 294      add_left_comm, add_comm]