TransferFunction

formal source

  89    \(H(i\omega) = 1 + \frac{\Delta}{1 + i\omega\tau_\star}\)
  90
  91    where \(\Delta = w - 1\) is the DC enhancement. -/
  92structure TransferFunction where
  93  Δ : ℝ  -- DC enhancement (w - 1)
  94  τ : ℝ  -- Memory timescale
  95  τ_pos : 0 < τ
  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)