theorem
proved
tactic proof
response_function_is_real_part
show as:
view Lean formalization →
formal statement (Lean)
264theorem response_function_is_real_part (H : CaldeiraLeggett.TransferFunction) (ω : ℝ) :
265 CaldeiraLeggett.response_function H ω = (transfer_function_complex H ω).re := by
proof body
Tactic-mode proof.
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]
295
296 -- Finish: real part of `1 + z` is `1 + Re(z)`.
297 -- Note: `simp` can unfold `.re` of addition definitionaly once `hdiv` is in place.
298 -- We rewrite the divisor `w` back into the original denominator.
299 simp [hw, hdiv, Complex.add_re]
300
301end
302
303end CausalKernelChain
304end Gravity
305end IndisputableMonolith