pith. machine review for the scientific record. sign in
def definition def or abbrev

transfer_function_complex

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 127def transfer_function_complex (H : CaldeiraLeggett.TransferFunction) (ω : ℝ) : ℂ :=

proof body

Definition body.

 128  (1 : ℂ) + (H.Δ : ℂ) / ((1 : ℂ) + Complex.I * (ω : ℂ) * (H.τ : ℂ))
 129
 130
 131/-- The Debye exponential kernel for a single-timescale response:
 132\[
 133\Gamma(t) = \frac{\Delta}{\tau} e^{-t/\tau},\quad t \ge 0.
 134\]
 135We treat it as a function on `ℝ` and integrate it on `[0,B]` (then take `B → ∞`). -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (9)

Lean names referenced from this declaration's body.