def definition def or abbrev

`laplaceExponent`

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

formal statement (Lean)

 164def laplaceExponent (H : CaldeiraLeggett.TransferFunction) (ω : ℝ) : ℂ :=

Definition body.

 165  ((1 / H.τ : ℝ) : ℂ) + Complex.I * (ω : ℂ)
 166
 167
 168/-- Truncated Debye-kernel response tends to its closed form as `B → ∞`. -/

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

kernel_response_limit in IndisputableMonolith.Gravity.CausalKernelChain decl_use

Lean names referenced from this declaration's body.

H in IndisputableMonolith.Algebra.CostAlgebra decl_use
kernel in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
H in IndisputableMonolith.Cost.FunctionalEquation decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
TransferFunction in IndisputableMonolith.Gravity.CaldeiraLeggett decl_use
kernel in IndisputableMonolith.ILG.Kernel decl_use