cost_descent_step

formal source

 119      rw [trajectory_succ]
 120      exact hf.preserves_positive _ ih
 121
 122theorem cost_descent_step {f : ℝ → ℝ} (hf : RecognitionDescent f)
 123    {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
 124    Cost.Jcost (f r) < Cost.Jcost r :=
 125  hf.strict_descent_off r hr hne
 126
 127/-! ## §5. Equilibrium is the unique zero of the J-cost -/
 128
 129theorem cost_zero_iff_equilibrium {x : ℝ} (hx : 0 < x) :
 130    Cost.Jcost x = 0 ↔ x = 1 := by
 131  refine ⟨?_, ?_⟩
 132  · intro h
 133    by_contra hne
 134    have hpos : 0 < Cost.Jcost x := Cost.Jcost_pos_of_ne_one x hx hne
 135    linarith
 136  · intro h
 137    rw [h]
 138    exact Cost.Jcost_unit0
 139
 140/-- Rewrite of `cost_zero_iff_equilibrium` in the equivalent contrapositive:
 141off equilibrium, the J-cost is strictly positive. -/
 142theorem cost_pos_off_equilibrium {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) :
 143    0 < Cost.Jcost x :=
 144  Cost.Jcost_pos_of_ne_one x hx hne
 145
 146/-! ## §6. Master certificate -/
 147
 148structure PIDStabilityCert where
 149  fixes_equilibrium :
 150    ∀ (f : ℝ → ℝ), RecognitionDescent f → f 1 = 1
 151  preserves_positive_traj :
 152    ∀ (f : ℝ → ℝ) (hf : RecognitionDescent f) (r : ℝ),