cost_zero_iff_equilibrium

formal source

 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 : ℝ),
 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