trajectory_zero

formal source

  92  | 0 => r
  93  | n + 1 => f (trajectory f r n)
  94
  95theorem trajectory_zero (f : ℝ → ℝ) (r : ℝ) : trajectory f r 0 = r := rfl
  96
  97theorem trajectory_succ (f : ℝ → ℝ) (r : ℝ) (n : ℕ) :
  98    trajectory f r (n + 1) = f (trajectory f r n) := rfl
  99
 100/-! ## §3. Equilibrium fixed point -/
 101
 102theorem trajectory_at_equilibrium {f : ℝ → ℝ}
 103    (hf : RecognitionDescent f) (n : ℕ) : trajectory f 1 n = 1 := by
 104  induction n with
 105  | zero => rfl
 106  | succ k ih => rw [trajectory_succ, ih]; exact hf.fixes_equilibrium
 107
 108/-! ## §4. J-cost descent under iteration -/
 109
 110/-- If the controller exhibits recognition descent and the trajectory
 111preserves positivity (which it does, by `preserves_positive`), then
 112the per-step J-cost is non-increasing. Strict descent holds whenever
 113the current state is off equilibrium. -/
 114theorem trajectory_pos {f : ℝ → ℝ} (hf : RecognitionDescent f)
 115    {r : ℝ} (hr : 0 < r) (n : ℕ) : 0 < trajectory f r n := by
 116  induction n with
 117  | zero => exact hr
 118  | succ k ih =>
 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