 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
 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, ?_, ?_⟩

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.