def
definition
def or abbrev
pidStabilityCert
show as:
view Lean formalization →
formal statement (Lean)
163noncomputable def pidStabilityCert : PIDStabilityCert where
164 fixes_equilibrium := fun _ hf => hf.fixes_equilibrium
proof body
Definition body.
165 preserves_positive_traj := fun _ hf r hr n => trajectory_pos hf hr n
166 trajectory_fixes_equilibrium := fun _ hf n => trajectory_at_equilibrium hf n
167 cost_descent_off_equilibrium := fun _ hf r hr hne => cost_descent_step hf hr hne
168 cost_zero_iff_equilibrium := fun x hx => cost_zero_iff_equilibrium hx
169
170/-! ## §7. One-statement summary -/
171