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

coupling_from_spectral

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)

  63def coupling_from_spectral (J : ℝ → ℝ) (ω : ℝ) : ℝ :=

proof body

Definition body.

  64  sqrt (2 * J ω * ω / Real.pi)
  65
  66/-! ## Single-Pole (Debye) Spectral Density -/
  67
  68/-- The Debye (single-pole) spectral density:
  69    \(J_{\rm Debye}(\Omega) = \frac{2\lambda\gamma}{\pi} \cdot \frac{\Omega}{\gamma^2 + \Omega^2}\)
  70
  71    where \(\gamma = 1/\tau_\star\) is the cutoff frequency (inverse memory time)
  72    and \(\lambda\) is the coupling strength. -/

depends on (11)

Lean names referenced from this declaration's body.