Nonlinear dynamical systems & control theory

3.4. LaSalle's invariance principle🔗

In order to prove asymptotic stability, one either needs to invoke a variant Lyapunov's theorem with the stronger assumption that the Lyapunov function is strictly decreasing along the flow or invoke LaSalle's invariance principle. The later has the advantage that one can prove asymptotic stability even when the Lyapunov function is not strictly decreasing, but with the caveat that it only applies to autonomous systems.

The condition to conclude asymptotic stability becomes that there exist no trajectory other than the trivial trajectory in the zero set of \dot{V}(x). This condition has an obvious generalization to convergence to sets:

🔗theorem
IsLyapunovOn.tendsto_nhdsSet.{u_2} {E : Type u_2} {y : E} {v : E → ℝ}
  [TopologicalSpace E] {Φ : Flow ℝ E} {s s' : Set E} [T2Space E]
  (hs : IsCompact s) (h_lya : IsLyapunovOn v Φ.toFun s)
  (hΦ_mem : ∀ᶠ (t : ℝ) in Filter.atTop, Φ.toFun t y ∈ s) {f' : E → ℝ}
  (hf' : ∀ x ∈ s, HasDerivAt (fun x_1 ↦ v (Φ.toFun x_1 x)) (f' x) 0)
  (h : ∀ x ∈ s, x ∉ s' → ∃ t, 0 ≤ t ∧ Φ.toFun t x ∉ {x | f' x = 0}) :
  Filter.Tendsto (fun x ↦ Φ.toFun x y) Filter.atTop (𝓝ˢ s')
IsLyapunovOn.tendsto_nhdsSet.{u_2}
  {E : Type u_2} {y : E} {v : E → ℝ}
  [TopologicalSpace E] {Φ : Flow ℝ E}
  {s s' : Set E} [T2Space E]
  (hs : IsCompact s)
  (h_lya : IsLyapunovOn v Φ.toFun s)
  (hΦ_mem :
    ∀ᶠ (t : ℝ) in Filter.atTop,
      Φ.toFun t y ∈ s)
  {f' : E → ℝ}
  (hf' :
    ∀ x ∈ s,
      HasDerivAt
        (fun x_1 ↦ v (Φ.toFun x_1 x))
        (f' x) 0)
  (h :
    ∀ x ∈ s,
      x ∉ s' →
        ∃ t,
          0 ≤ t ∧
            Φ.toFun t x ∉
              {x | f' x = 0}) :
  Filter.Tendsto (fun x ↦ Φ.toFun x y)
    Filter.atTop (𝓝ˢ s')

LaSalle's invariance principle: if no trajectory is fully contained in the zero set of the derivative of the Lyapunov function, then Φ · y converges to the subset.

Version for local Lyapunov functions

🔗theorem
IsLyapunovOn.tendsto_nhds.{u_2} {E : Type u_2} {y : E} {v : E → ℝ}
  [TopologicalSpace E] {Φ : Flow ℝ E} {s : Set E} [T2Space E]
  (hs : IsCompact s) (h_lya : IsLyapunovOn v Φ.toFun s)
  (hΦ_mem : ∀ᶠ (t : ℝ) in Filter.atTop, Φ.toFun t y ∈ s) {f' : E → ℝ}
  (hf' : ∀ x ∈ s, HasDerivAt (fun x_1 ↦ v (Φ.toFun x_1 x)) (f' x) 0)
  {x₀ : E}
  (h : ∀ x ∈ s, x ≠ x₀ → ∃ t, 0 ≤ t ∧ Φ.toFun t x ∉ {x | f' x = 0}) :
  Filter.Tendsto (fun x ↦ Φ.toFun x y) Filter.atTop (𝓝 x₀)
IsLyapunovOn.tendsto_nhds.{u_2}
  {E : Type u_2} {y : E} {v : E → ℝ}
  [TopologicalSpace E] {Φ : Flow ℝ E}
  {s : Set E} [T2Space E]
  (hs : IsCompact s)
  (h_lya : IsLyapunovOn v Φ.toFun s)
  (hΦ_mem :
    ∀ᶠ (t : ℝ) in Filter.atTop,
      Φ.toFun t y ∈ s)
  {f' : E → ℝ}
  (hf' :
    ∀ x ∈ s,
      HasDerivAt
        (fun x_1 ↦ v (Φ.toFun x_1 x))
        (f' x) 0)
  {x₀ : E}
  (h :
    ∀ x ∈ s,
      x ≠ x₀ →
        ∃ t,
          0 ≤ t ∧
            Φ.toFun t x ∉
              {x | f' x = 0}) :
  Filter.Tendsto (fun x ↦ Φ.toFun x y)
    Filter.atTop (𝓝 x₀)

LaSalle's invariance principle: if no trajectory is fully contained in the zero set of the derivative of the Lyapunov function, then Φ · y converges to the fixed point.

Version for local Lyapunov functions

🔗theorem
IsLyapunov.tendsto_nhdsSet.{u_2} {E : Type u_2} {y : E} {v : E → ℝ}
  [TopologicalSpace E] {Φ : Flow ℝ E} {s s' : Set E} [T2Space E]
  (hs : IsCompact s) (h_lya : IsLyapunov v Φ.toFun)
  (hs' : ∀ ⦃x : E⦄, v x ≤ v y → x ∈ s) {f' : E → ℝ}
  (hf' : ∀ x ∈ s, HasDerivAt (fun x_1 ↦ v (Φ.toFun x_1 x)) (f' x) 0)
  (h : ∀ x ∈ s, x ∉ s' → ∃ t, 0 ≤ t ∧ Φ.toFun t x ∉ {x | f' x = 0}) :
  Filter.Tendsto (fun x ↦ Φ.toFun x y) Filter.atTop (𝓝ˢ s')
IsLyapunov.tendsto_nhdsSet.{u_2}
  {E : Type u_2} {y : E} {v : E → ℝ}
  [TopologicalSpace E] {Φ : Flow ℝ E}
  {s s' : Set E} [T2Space E]
  (hs : IsCompact s)
  (h_lya : IsLyapunov v Φ.toFun)
  (hs' : ∀ ⦃x : E⦄, v x ≤ v y → x ∈ s)
  {f' : E → ℝ}
  (hf' :
    ∀ x ∈ s,
      HasDerivAt
        (fun x_1 ↦ v (Φ.toFun x_1 x))
        (f' x) 0)
  (h :
    ∀ x ∈ s,
      x ∉ s' →
        ∃ t,
          0 ≤ t ∧
            Φ.toFun t x ∉
              {x | f' x = 0}) :
  Filter.Tendsto (fun x ↦ Φ.toFun x y)
    Filter.atTop (𝓝ˢ s')

LaSalle's invariance principle: if no trajectory is fully contained in the zero set of the derivative of the Lyapunov function, then Φ · y converges to the subset.

Version for global Lyapunov functions

🔗theorem
IsLyapunov.tendsto_nhds.{u_2} {E : Type u_2} {y : E} {v : E → ℝ}
  [TopologicalSpace E] {Φ : Flow ℝ E} {s : Set E} [T2Space E]
  (hs : IsCompact s) (h_lya : IsLyapunov v Φ.toFun)
  (hs' : ∀ ⦃x : E⦄, v x ≤ v y → x ∈ s) {f' : E → ℝ}
  (hf' : ∀ x ∈ s, HasDerivAt (fun x_1 ↦ v (Φ.toFun x_1 x)) (f' x) 0)
  {x₀ : E}
  (h : ∀ x ∈ s, x ≠ x₀ → ∃ t, 0 ≤ t ∧ Φ.toFun t x ∉ {x | f' x = 0}) :
  Filter.Tendsto (fun x ↦ Φ.toFun x y) Filter.atTop (𝓝 x₀)
IsLyapunov.tendsto_nhds.{u_2}
  {E : Type u_2} {y : E} {v : E → ℝ}
  [TopologicalSpace E] {Φ : Flow ℝ E}
  {s : Set E} [T2Space E]
  (hs : IsCompact s)
  (h_lya : IsLyapunov v Φ.toFun)
  (hs' : ∀ ⦃x : E⦄, v x ≤ v y → x ∈ s)
  {f' : E → ℝ}
  (hf' :
    ∀ x ∈ s,
      HasDerivAt
        (fun x_1 ↦ v (Φ.toFun x_1 x))
        (f' x) 0)
  {x₀ : E}
  (h :
    ∀ x ∈ s,
      x ≠ x₀ →
        ∃ t,
          0 ≤ t ∧
            Φ.toFun t x ∉
              {x | f' x = 0}) :
  Filter.Tendsto (fun x ↦ Φ.toFun x y)
    Filter.atTop (𝓝 x₀)

LaSalle's invariance principle: if no trajectory is fully contained in the zero set of the derivative of the Lyapunov function, then Φ · y converges to the fixed point.

Version for global Lyapunov functions

Note that we formulate the condition as its contrapositive.

This version of LaSalle's invariance principle can be specialized to the case that V is strictly decreasing along the flow:

🔗theorem
IsLyapunovOn.tendsto_nhdsSet_of_hasDerivAt_neg.{u_2} {E : Type u_2}
  {y : E} {v : E → ℝ} [TopologicalSpace E] {Φ : Flow ℝ E} {s s' : Set E}
  [T2Space E] (hs : IsCompact s) (h_lya : IsLyapunovOn v Φ.toFun s)
  (hΦ_mem : ∀ᶠ (t : ℝ) in Filter.atTop, Φ.toFun t y ∈ s) {f' : E → ℝ}
  (hf' : ∀ x ∈ s, HasDerivAt (fun x_1 ↦ v (Φ.toFun x_1 x)) (f' x) 0)
  (h : ∀ x ∈ s, x ∉ s' → f' x < 0) :
  Filter.Tendsto (fun x ↦ Φ.toFun x y) Filter.atTop (𝓝ˢ s')
IsLyapunovOn.tendsto_nhdsSet_of_hasDerivAt_neg.{u_2}
  {E : Type u_2} {y : E} {v : E → ℝ}
  [TopologicalSpace E] {Φ : Flow ℝ E}
  {s s' : Set E} [T2Space E]
  (hs : IsCompact s)
  (h_lya : IsLyapunovOn v Φ.toFun s)
  (hΦ_mem :
    ∀ᶠ (t : ℝ) in Filter.atTop,
      Φ.toFun t y ∈ s)
  {f' : E → ℝ}
  (hf' :
    ∀ x ∈ s,
      HasDerivAt
        (fun x_1 ↦ v (Φ.toFun x_1 x))
        (f' x) 0)
  (h : ∀ x ∈ s, x ∉ s' → f' x < 0) :
  Filter.Tendsto (fun x ↦ Φ.toFun x y)
    Filter.atTop (𝓝ˢ s')

If v is a strict Lyapunov function, then Φ · y converges to the subset.

🔗theorem
IsLyapunovOn.tendsto_nhds_of_hasDerivAt_neg.{u_2} {E : Type u_2} {y : E}
  {v : E → ℝ} [TopologicalSpace E] {Φ : Flow ℝ E} {s : Set E}
  [T2Space E] (hs : IsCompact s) (h_lya : IsLyapunovOn v Φ.toFun s)
  (hΦ_mem : ∀ᶠ (t : ℝ) in Filter.atTop, Φ.toFun t y ∈ s) {f' : E → ℝ}
  (hf' : ∀ x ∈ s, HasDerivAt (fun x_1 ↦ v (Φ.toFun x_1 x)) (f' x) 0)
  {x₀ : E} (h : ∀ x ∈ s, x ≠ x₀ → f' x < 0) :
  Filter.Tendsto (fun x ↦ Φ.toFun x y) Filter.atTop (𝓝 x₀)
IsLyapunovOn.tendsto_nhds_of_hasDerivAt_neg.{u_2}
  {E : Type u_2} {y : E} {v : E → ℝ}
  [TopologicalSpace E] {Φ : Flow ℝ E}
  {s : Set E} [T2Space E]
  (hs : IsCompact s)
  (h_lya : IsLyapunovOn v Φ.toFun s)
  (hΦ_mem :
    ∀ᶠ (t : ℝ) in Filter.atTop,
      Φ.toFun t y ∈ s)
  {f' : E → ℝ}
  (hf' :
    ∀ x ∈ s,
      HasDerivAt
        (fun x_1 ↦ v (Φ.toFun x_1 x))
        (f' x) 0)
  {x₀ : E}
  (h : ∀ x ∈ s, x ≠ x₀ → f' x < 0) :
  Filter.Tendsto (fun x ↦ Φ.toFun x y)
    Filter.atTop (𝓝 x₀)

If v is a strict Lyapunov function, then Φ · y converges to the fixed point.

🔗theorem
IsLyapunov.tendsto_nhdsSet_of_hasDerivAt_neg.{u_2} {E : Type u_2}
  {y : E} {v : E → ℝ} [TopologicalSpace E] {Φ : Flow ℝ E} {s s' : Set E}
  [T2Space E] (hs : IsCompact s) (h_lya : IsLyapunov v Φ.toFun)
  (hs' : ∀ ⦃x : E⦄, v x ≤ v y → x ∈ s) {f' : E → ℝ}
  (hf' : ∀ x ∈ s, HasDerivAt (fun x_1 ↦ v (Φ.toFun x_1 x)) (f' x) 0)
  (h : ∀ x ∈ s, x ∉ s' → f' x < 0) :
  Filter.Tendsto (fun x ↦ Φ.toFun x y) Filter.atTop (𝓝ˢ s')
IsLyapunov.tendsto_nhdsSet_of_hasDerivAt_neg.{u_2}
  {E : Type u_2} {y : E} {v : E → ℝ}
  [TopologicalSpace E] {Φ : Flow ℝ E}
  {s s' : Set E} [T2Space E]
  (hs : IsCompact s)
  (h_lya : IsLyapunov v Φ.toFun)
  (hs' : ∀ ⦃x : E⦄, v x ≤ v y → x ∈ s)
  {f' : E → ℝ}
  (hf' :
    ∀ x ∈ s,
      HasDerivAt
        (fun x_1 ↦ v (Φ.toFun x_1 x))
        (f' x) 0)
  (h : ∀ x ∈ s, x ∉ s' → f' x < 0) :
  Filter.Tendsto (fun x ↦ Φ.toFun x y)
    Filter.atTop (𝓝ˢ s')

If v is a strict Lyapunov function, then Φ · y converges to the subset.

🔗theorem
IsLyapunov.tendsto_nhds_of_hasDerivAt_neg.{u_2} {E : Type u_2} {y : E}
  {v : E → ℝ} [TopologicalSpace E] {Φ : Flow ℝ E} {s : Set E}
  [T2Space E] (hs : IsCompact s) (h_lya : IsLyapunov v Φ.toFun)
  (hs' : ∀ ⦃x : E⦄, v x ≤ v y → x ∈ s) {f' : E → ℝ}
  (hf' : ∀ x ∈ s, HasDerivAt (fun x_1 ↦ v (Φ.toFun x_1 x)) (f' x) 0)
  {x₀ : E} (h : ∀ x ∈ s, x ≠ x₀ → f' x < 0) :
  Filter.Tendsto (fun x ↦ Φ.toFun x y) Filter.atTop (𝓝 x₀)
IsLyapunov.tendsto_nhds_of_hasDerivAt_neg.{u_2}
  {E : Type u_2} {y : E} {v : E → ℝ}
  [TopologicalSpace E] {Φ : Flow ℝ E}
  {s : Set E} [T2Space E]
  (hs : IsCompact s)
  (h_lya : IsLyapunov v Φ.toFun)
  (hs' : ∀ ⦃x : E⦄, v x ≤ v y → x ∈ s)
  {f' : E → ℝ}
  (hf' :
    ∀ x ∈ s,
      HasDerivAt
        (fun x_1 ↦ v (Φ.toFun x_1 x))
        (f' x) 0)
  {x₀ : E}
  (h : ∀ x ∈ s, x ≠ x₀ → f' x < 0) :
  Filter.Tendsto (fun x ↦ Φ.toFun x y)
    Filter.atTop (𝓝 x₀)

If v is a strict Lyapunov function, then Φ · y converges to the fixed point.