def
definition
def or abbrev
is_locked_regime
show as:
view Lean formalization →
formal statement (Lean)
37def is_locked_regime (Q : ℝ) : Prop := Q ≤ Q_lock
proof body
Definition body.
38
39/-- The physical coupling including the lock-in effect. -/