def
definition
pidStabilityCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Robotics.PIDStabilityFromJCost on GitHub at line 163.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
160 cost_zero_iff_equilibrium :
161 ∀ (x : ℝ), 0 < x → (Cost.Jcost x = 0 ↔ x = 1)
162
163noncomputable def pidStabilityCert : PIDStabilityCert where
164 fixes_equilibrium := fun _ hf => hf.fixes_equilibrium
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
172theorem pid_stability_one_statement :
173 ∀ (f : ℝ → ℝ), RecognitionDescent f →
174 f 1 = 1 ∧
175 (∀ (r : ℝ), 0 < r → r ≠ 1 → Cost.Jcost (f r) < Cost.Jcost r) ∧
176 (∀ (x : ℝ), 0 < x → (Cost.Jcost x = 0 ↔ x = 1)) := by
177 intro f hf
178 refine ⟨hf.fixes_equilibrium, ?_, ?_⟩
179 · intro r hr hne
180 exact hf.strict_descent_off r hr hne
181 · intro x hx
182 exact cost_zero_iff_equilibrium hx
183
184end
185
186end PIDStabilityFromJCost
187end Robotics
188end IndisputableMonolith