`trajectory`

definition

show as: view math explainer →

module: IndisputableMonolith.Robotics.PIDStabilityFromJCost
domain: Robotics
line: 91 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Robotics.PIDStabilityFromJCost on GitHub at line 91.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  88/-! ## §2. Iterating the controller -/
  89
  90/-- The state trajectory under repeated controller application. -/
  91def trajectory (f : ℝ → ℝ) (r : ℝ) : ℕ → ℝ
  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

papers checked against this theorem

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