pith. machine review for the scientific record. sign in
theorem proved term proof

critical_modes_specification

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)

 167theorem critical_modes_specification :
 168    ∀ (t g : ℝ), t > 0 → g > 0 →
 169    criticalModes t g = -Real.log (t / tau0_seconds) / (g * Real.log phi) := by

proof body

Term-mode proof.

 170  intro t g ht hg
 171  unfold criticalModes
 172  simp [ht, hg]
 173
 174/-! ## Qubit Decoherence Examples -/
 175
 176/-- Typical superconducting qubit parameters. -/

depends on (3)

Lean names referenced from this declaration's body.