Chain rule for time-varying V along trajectories

theorem hasDerivAt_V_comp_traj_NA {n : ℕ} {f : ℝ → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} {V : ℝ → EuclideanSpace ℝ (Fin n) → ℝ} (hV_diff : Differentiable ℝ (Function.uncurry V)) {φ : ℝ → EuclideanSpace ℝ (Fin n)} (htraj : IsTrajectoryNA φ f) (t : ℝ) : HasDerivAt (fun (s : ℝ) => V s (φ s)) ((fderiv ℝ (Function.uncurry V) (t, φ t)) (1, f t (φ t))) t

V nonincreasing along trajectories

theorem V_NA_nonincreasing {n : ℕ} {f : ℝ → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} {V : ℝ → EuclideanSpace ℝ (Fin n) → ℝ} (hV_diff : Differentiable ℝ (Function.uncurry V)) {φ : ℝ → EuclideanSpace ℝ (Fin n)} (htraj : IsTrajectoryNA φ f) {a b : ℝ} (hab : a ≤ b) (hLie : ∀ t ∈ Set.Ioo a b, (fderiv ℝ (Function.uncurry V) (t, φ t)) (1, f t (φ t)) ≤ 0) : V b (φ b) ≤ V a (φ a)

theorem lyapunov_uniformly_stable_NA {n : ℕ} [NeZero n] (f : ℝ → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (r : ℝ) (hr : 0 < r) (V : ℝ → EuclideanSpace ℝ (Fin n) → ℝ) (hV_diff : Differentiable ℝ (Function.uncurry V)) (W₁ W₂ : EuclideanSpace ℝ (Fin n) → ℝ) (hW₁_cont : ContinuousOn W₁ (Metric.closedBall 0 r)) (hW₂_cont : ContinuousOn W₂ (Metric.closedBall 0 r)) (hW₁_zero : W₁ 0 = 0) (hW₂_zero : W₂ 0 = 0) (hW₁_pos : ∀ x ∈ Metric.closedBall 0 r, x ≠ 0 → 0 < W₁ x) (hW₂_pos : ∀ x ∈ Metric.closedBall 0 r, x ≠ 0 → 0 < W₂ x) (hV_sandwich : ∀ (t : ℝ), 0 ≤ t → ∀ (x : EuclideanSpace ℝ (Fin n)), ‖x‖ ≤ r → W₁ x ≤ V t x ∧ V t x ≤ W₂ x) (hLie_nonpos : ∀ (t : ℝ), 0 ≤ t → ∀ (x : EuclideanSpace ℝ (Fin n)), ‖x‖ ≤ r → (fderiv ℝ (Function.uncurry V) (t, x)) (1, f t x) ≤ 0) : UniformlyStableNA f 0

theorem lyapunov_uniformly_asymptotic_stable_NA {n : ℕ} [NeZero n] (f : ℝ → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (r : ℝ) (hr : 0 < r) (V : ℝ → EuclideanSpace ℝ (Fin n) → ℝ) (hV_diff : Differentiable ℝ (Function.uncurry V)) (W₁ W₂ W₃ : EuclideanSpace ℝ (Fin n) → ℝ) (hW₁_cont : ContinuousOn W₁ (Metric.closedBall 0 r)) (hW₂_cont : ContinuousOn W₂ (Metric.closedBall 0 r)) (hW₃_cont : ContinuousOn W₃ (Metric.closedBall 0 r)) (hW₁_zero : W₁ 0 = 0) (hW₂_zero : W₂ 0 = 0) (hW₃_zero : W₃ 0 = 0) (hW₁_pos : ∀ x ∈ Metric.closedBall 0 r, x ≠ 0 → 0 < W₁ x) (hW₂_pos : ∀ x ∈ Metric.closedBall 0 r, x ≠ 0 → 0 < W₂ x) (hW₃_pos : ∀ x ∈ Metric.closedBall 0 r, x ≠ 0 → 0 < W₃ x) (hV_sandwich : ∀ (t : ℝ), 0 ≤ t → ∀ (x : EuclideanSpace ℝ (Fin n)), ‖x‖ ≤ r → W₁ x ≤ V t x ∧ V t x ≤ W₂ x) (hLie_bound : ∀ (t : ℝ), 0 ≤ t → ∀ (x : EuclideanSpace ℝ (Fin n)), ‖x‖ ≤ r → (fderiv ℝ (Function.uncurry V) (t, x)) (1, f t x) ≤ -W₃ x) : UniformlyAsymptoticStableNA f 0