module module

`IndisputableMonolith.Robotics.PIDStabilityFromJCost`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (12)

structure RecognitionDescent L82
def trajectory L91
theorem trajectory_zero L95
theorem trajectory_succ L97
theorem trajectory_at_equilibrium L102
theorem trajectory_pos L114
theorem cost_descent_step L122
theorem cost_zero_iff_equilibrium L129
theorem cost_pos_off_equilibrium L142
structure PIDStabilityCert L148
def pidStabilityCert L163
theorem pid_stability_one_statement L172