structure
definition
def or abbrev
PIDStabilityCert
show as:
view Lean formalization →
formal statement (Lean)
148structure PIDStabilityCert where
149 fixes_equilibrium :
150 ∀ (f : ℝ → ℝ), RecognitionDescent f → f 1 = 1
151 preserves_positive_traj :
152 ∀ (f : ℝ → ℝ) (hf : RecognitionDescent f) (r : ℝ),
153 0 < r → ∀ n : ℕ, 0 < trajectory f r n
154 trajectory_fixes_equilibrium :
155 ∀ (f : ℝ → ℝ), RecognitionDescent f →
156 ∀ n : ℕ, trajectory f 1 n = 1
157 cost_descent_off_equilibrium :
158 ∀ (f : ℝ → ℝ) (hf : RecognitionDescent f) (r : ℝ),
159 0 < r → r ≠ 1 → Cost.Jcost (f r) < Cost.Jcost r
160 cost_zero_iff_equilibrium :
161 ∀ (x : ℝ), 0 < x → (Cost.Jcost x = 0 ↔ x = 1)
162