3.3. Lyapunov functions🔗

The most common way to prove stability of equilibrium points (or limit cycles) is to employ Lyapunov's direct method, also known as the method of Lyapunov functions. A Lyapunov function is a continuous function that is

strictly positive except at the equilibrium point,
zero at the equilibrium point,
decreasing along the flow.

Lyapunov's theorem asserts that if such a function exists, then the equilibrium point is stable. In addition if the Lyapunov function is strictly decreasing along the flow, then the equilibrium is asymptotically stable.

Currently, we only prove Lyapunov's theorem for Lyapunov functions that are independent of the time variable.

We provide a local and a global version of a Lyapunov function:

structure

IsLyapunovOn.{u_1, u_3, u_4} {ι : Type u_1} {E : Type u_3}
  {F : Type u_4} [TopologicalSpace E] [Preorder F] [Zero F]
  [TopologicalSpace F] [Preorder ι] (v : E → F) (Φ : ι → E → E)
  (s : Set E) : Prop
IsLyapunovOn.{u_1, u_3, u_4}
  {ι : Type u_1} {E : Type u_3}
  {F : Type u_4} [TopologicalSpace E]
  [Preorder F] [Zero F]
  [TopologicalSpace F] [Preorder ι]
  (v : E → F) (Φ : ι → E → E)
  (s : Set E) : Prop

A Lyapunov function is a continuous non-negative function that is non-increasing with respect to a given flow.

Note that we assume that v is non-negative and continuous everywhere, but only decreasing on s.

Constructor

IsLyapunovOn.mk.{u_1, u_3, u_4}

Fields

pos : ∀ (x : E), 0 ≤ v x

A Lyapunov function is non-negative everywhere

cont : Continuous v

A Lyapunov function is continuous everywhere

antitone : ∀ ⦃x : E⦄ ⦃t₀ t₁ : ι⦄, Φ t₀ x ∈ s → Φ t₁ x ∈ s → t₀ ≤ t₁ → v (Φ t₁ x) ≤ v (Φ t₀ x)

A Lyapunov function is monotonically decreasing along the flow for all values t such that Φ t x is contained in s.

structure

IsLyapunov.{u_1, u_3, u_4} {ι : Type u_1} {E : Type u_3} {F : Type u_4}
  [TopologicalSpace E] [Preorder F] [Zero F] [TopologicalSpace F]
  [Preorder ι] (v : E → F) (Φ : ι → E → E) : Prop
IsLyapunov.{u_1, u_3, u_4} {ι : Type u_1}
  {E : Type u_3} {F : Type u_4}
  [TopologicalSpace E] [Preorder F]
  [Zero F] [TopologicalSpace F]
  [Preorder ι] (v : E → F)
  (Φ : ι → E → E) : Prop

A Lyapunov function is a continuous non-negative function that is non-increasing with respect to a given flow.

Constructor

IsLyapunov.mk.{u_1, u_3, u_4}

Fields

pos : ∀ (x : E), 0 ≤ v x

A Lyapunov function is non-negative everywhere

cont : Continuous v

A Lyapunov function is continuous everywhere

antitone : ∀ (x : E) ⦃t₀ t₁ : ι⦄, t₀ ≤ t₁ → v (Φ t₁ x) ≤ v (Φ t₀ x)

A Lyapunov function is monotonically decreasing along the flow.

Lyapunov's theorem can be stated as

theorem

IsLyapunovOn.isStableOn_nhdsSet.{u_1, u_3} {ι : Type u_1} {E : Type u_3}
  {Φ : ι → E → E} {s : Set E} [TopologicalSpace E] [Preorder ι]
  [FirstCountableTopology E] {v : E → ℝ} {t₀ : ι} {s' : Set E}
  (h_lya : IsLyapunovOn v Φ s) (h_cpt : IsCompact s)
  (hs : ∀ x ∈ s, ∀ t ∈ Set.Ici t₀, Φ t x ∈ s)
  (hvx₀ : ∀ (x : E), v x = 0 ↔ x ∈ s') (h_id : ∀ (x : E), Φ t₀ x = x)
  {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (h_subset : {p | v p ≤ δ₀} ⊆ s) :
  (𝓝ˢ s').IsStableOn Φ (Set.Ici t₀)
IsLyapunovOn.isStableOn_nhdsSet.{u_1, u_3}
  {ι : Type u_1} {E : Type u_3}
  {Φ : ι → E → E} {s : Set E}
  [TopologicalSpace E] [Preorder ι]
  [FirstCountableTopology E] {v : E → ℝ}
  {t₀ : ι} {s' : Set E}
  (h_lya : IsLyapunovOn v Φ s)
  (h_cpt : IsCompact s)
  (hs :
    ∀ x ∈ s, ∀ t ∈ Set.Ici t₀, Φ t x ∈ s)
  (hvx₀ : ∀ (x : E), v x = 0 ↔ x ∈ s')
  (h_id : ∀ (x : E), Φ t₀ x = x) {δ₀ : ℝ}
  (hδ₀ : 0 < δ₀)
  (h_subset : {p | v p ≤ δ₀} ⊆ s) :
  (𝓝ˢ s').IsStableOn Φ (Set.Ici t₀)

Lyapunov stability for time-independent Lyapunov functions.

Version for stability of subsets and local Lyapunov functions.

theorem

IsLyapunovOn.isStableOn_nhds.{u_1, u_3} {ι : Type u_1} {E : Type u_3}
  {Φ : ι → E → E} {x₀ : E} {s : Set E} [TopologicalSpace E] [Preorder ι]
  [FirstCountableTopology E] {v : E → ℝ} {t₀ : ι}
  (h_lya : IsLyapunovOn v Φ s) (h_cpt : IsCompact s)
  (hs : ∀ x ∈ s, ∀ t ∈ Set.Ici t₀, Φ t x ∈ s)
  (hvx₀ : ∀ (x : E), v x = 0 ↔ x = x₀) (h_id : ∀ (x : E), Φ t₀ x = x)
  {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (h_subset : {p | v p ≤ δ₀} ⊆ s) :
  (𝓝 x₀).IsStableOn Φ (Set.Ici t₀)
IsLyapunovOn.isStableOn_nhds.{u_1, u_3}
  {ι : Type u_1} {E : Type u_3}
  {Φ : ι → E → E} {x₀ : E} {s : Set E}
  [TopologicalSpace E] [Preorder ι]
  [FirstCountableTopology E] {v : E → ℝ}
  {t₀ : ι} (h_lya : IsLyapunovOn v Φ s)
  (h_cpt : IsCompact s)
  (hs :
    ∀ x ∈ s, ∀ t ∈ Set.Ici t₀, Φ t x ∈ s)
  (hvx₀ : ∀ (x : E), v x = 0 ↔ x = x₀)
  (h_id : ∀ (x : E), Φ t₀ x = x) {δ₀ : ℝ}
  (hδ₀ : 0 < δ₀)
  (h_subset : {p | v p ≤ δ₀} ⊆ s) :
  (𝓝 x₀).IsStableOn Φ (Set.Ici t₀)

Lyapunov stability for time-independent Lyapunov functions.

Version for stability of points and local Lyapunov functions.

theorem

IsLyapunov.isStableOn_nhdsSet.{u_1, u_3} {ι : Type u_1} {E : Type u_3}
  {Φ : ι → E → E} [TopologicalSpace E] [Preorder ι]
  [FirstCountableTopology E] {v : E → ℝ} {t₀ : ι} {s' : Set E}
  (h_lya : IsLyapunov v Φ) (hvx₀ : ∀ (x : E), v x = 0 ↔ x ∈ s')
  (h_id : ∀ (x : E), Φ t₀ x = x) {δ₀ : ℝ} (hδ₀ : 0 < δ₀)
  (h_cpt : IsCompact {p | v p ≤ δ₀}) : (𝓝ˢ s').IsStableOn Φ (Set.Ici t₀)
IsLyapunov.isStableOn_nhdsSet.{u_1, u_3}
  {ι : Type u_1} {E : Type u_3}
  {Φ : ι → E → E} [TopologicalSpace E]
  [Preorder ι] [FirstCountableTopology E]
  {v : E → ℝ} {t₀ : ι} {s' : Set E}
  (h_lya : IsLyapunov v Φ)
  (hvx₀ : ∀ (x : E), v x = 0 ↔ x ∈ s')
  (h_id : ∀ (x : E), Φ t₀ x = x) {δ₀ : ℝ}
  (hδ₀ : 0 < δ₀)
  (h_cpt : IsCompact {p | v p ≤ δ₀}) :
  (𝓝ˢ s').IsStableOn Φ (Set.Ici t₀)

Lyapunov stability for time-independent Lyapunov functions.

Version for stability of a point and global Lyapunov functions.

theorem

IsLyapunov.isStableOn_nhds.{u_1, u_3} {ι : Type u_1} {E : Type u_3}
  {Φ : ι → E → E} {x₀ : E} [TopologicalSpace E] [Preorder ι]
  [FirstCountableTopology E] {v : E → ℝ} {t₀ : ι}
  (h_lya : IsLyapunov v Φ) (hvx₀ : ∀ (x : E), v x = 0 ↔ x = x₀)
  (h_id : ∀ (x : E), Φ t₀ x = x) {δ₀ : ℝ} (hδ₀ : 0 < δ₀)
  (h_cpt : IsCompact {p | v p ≤ δ₀}) : (𝓝 x₀).IsStableOn Φ (Set.Ici t₀)
IsLyapunov.isStableOn_nhds.{u_1, u_3}
  {ι : Type u_1} {E : Type u_3}
  {Φ : ι → E → E} {x₀ : E}
  [TopologicalSpace E] [Preorder ι]
  [FirstCountableTopology E] {v : E → ℝ}
  {t₀ : ι} (h_lya : IsLyapunov v Φ)
  (hvx₀ : ∀ (x : E), v x = 0 ↔ x = x₀)
  (h_id : ∀ (x : E), Φ t₀ x = x) {δ₀ : ℝ}
  (hδ₀ : 0 < δ₀)
  (h_cpt : IsCompact {p | v p ≤ δ₀}) :
  (𝓝 x₀).IsStableOn Φ (Set.Ici t₀)

Lyapunov stability for time-independent Lyapunov functions.

Version for stability of a point and global Lyapunov functions.