structure
definition
def or abbrev
RecognitionDescent
show as:
view Lean formalization →
formal statement (Lean)
82structure RecognitionDescent (f : ℝ → ℝ) : Prop where
83 fixes_equilibrium : f 1 = 1
84 preserves_positive : ∀ r : ℝ, 0 < r → 0 < f r
85 strict_descent_off :
86 ∀ r : ℝ, 0 < r → r ≠ 1 → Cost.Jcost (f r) < Cost.Jcost r
87
88/-! ## §2. Iterating the controller -/
89
90/-- The state trajectory under repeated controller application. -/