response_function

formal source

  96
  97/-- The real part of the transfer function (response function).
  98    \(C(\omega) = \text{Re}[H(i\omega)] = 1 + \frac{\Delta}{1 + (\omega\tau)^2}\) -/
  99def response_function (H : TransferFunction) (ω : ℝ) : ℝ :=
 100  1 + H.Δ / (1 + (ω * H.τ)^2)
 101
 102/-- The imaginary part of the transfer function (quadrature function).
 103    \(S(\omega) = \text{Im}[H(i\omega)] = -\frac{\Delta \cdot \omega\tau}{1 + (\omega\tau)^2}\) -/
 104def quadrature_function (H : TransferFunction) (ω : ℝ) : ℝ :=
 105  -H.Δ * ω * H.τ / (1 + (ω * H.τ)^2)
 106
 107/-! ## Key Properties -/
 108
 109/-- At zero frequency, the response equals \(1 + \Delta = w\). -/
 110theorem response_at_zero (H : TransferFunction) :
 111    response_function H 0 = 1 + H.Δ := by
 112  unfold response_function
 113  simp
 114
 115/-- At infinite frequency, the response approaches 1 (Newtonian limit). -/
 116theorem response_limit_high_freq (H : TransferFunction) (hΔ : H.Δ ≠ 0) :
 117    Filter.Tendsto (response_function H) Filter.atTop (nhds 1) := by
 118  -- As ω → ∞, Δ/(1 + (ωτ)²) → 0
 119  unfold response_function
 120  -- Show the denominator tends to `+∞` as ω → +∞.
 121  have hmul : Filter.Tendsto (fun ω : ℝ => ω * H.τ) Filter.atTop Filter.atTop := by
 122    simpa using ((Filter.tendsto_id).atTop_mul_const H.τ_pos)
 123  have hsq : Filter.Tendsto (fun ω : ℝ => (ω * H.τ) ^ (2 : ℕ)) Filter.atTop Filter.atTop :=
 124    (Filter.tendsto_pow_atTop (α := ℝ) (n := 2) (by decide)).comp hmul
 125  have hmono :
 126      (fun ω : ℝ => (ω * H.τ) ^ (2 : ℕ))
 127        ≤ᶠ[Filter.atTop] (fun ω : ℝ => 1 + (ω * H.τ) ^ (2 : ℕ)) :=
 128    Filter.Eventually.of_forall (fun _ω => by linarith)
 129  have hden :