Nonlinear dynamical systems & control theory

3.1. Lyapunov stability🔗

Consider a dynamical system \dot{x} = f(x) a subset s is called stable if all trajectories that are close to s stay close to s. This condition can be naturally phrased in terms of Filter:

🔗def
Filter.IsStableOn.{u_1, u_2} {ι : Type u_1} {E : Type u_2}
  (l : Filter E) (Φ : ι → E → E) (I : Set ι) : Prop
Filter.IsStableOn.{u_1, u_2}
  {ι : Type u_1} {E : Type u_2}
  (l : Filter E) (Φ : ι → E → E)
  (I : Set ι) : Prop

A filter is stable if for every s ∈ l there exists a s' ∈ l such that for all x ∈ s' the flow of x is contained in s.

Version for arbitrary time sets I. Forward stability is l.IsStableOn Φ (Set.Ici 0). For non-autonomous systems with flow Φ : ℝ → ℝ → E → E the forward stability becomes ∀ t₀, l.IsStableOn (Φ t₀) (Set.Ici t₀).

The typical case is that l is given by the neighbourhood filter nhds x₀. Then we recover the usual definition:

example (x₀ : E) : (𝓝 x₀).IsStableOn Φ (Ici 0) ↔ ∀ ε > 0, ∃ δ > 0, ∀ t ≥ 0, ∀ x, dist x x₀ < δ → dist (Φ t x) x₀ < ε := α:Type u_1E:Type u_2inst✝:PseudoMetricSpace EΦ:ℝ → E → Ex₀✝:Es:Set Ex₀:E⊢ (𝓝 x₀).IsStableOn Φ (Ici 0) ↔ ∀ ε > 0, ∃ δ > 0, ∀ t ≥ 0, ∀ (x : E), dist x x₀ < δ → dist (Φ t x) x₀ < ε α:Type u_1E:Type u_2inst✝:PseudoMetricSpace EΦ:ℝ → E → Ex₀✝:Es:Set Ex₀:E⊢ (∀ (i : ℝ), 0 < i → ∃ i', 0 < i' ∧ ∀ t ∈ Ici 0, ∀ x ∈ ball x₀ i', Φ t x ∈ ball x₀ i) ↔ ∀ ε > 0, ∃ δ > 0, ∀ t ≥ 0, ∀ (x : E), dist x x₀ < δ → dist (Φ t x) x₀ < ε α:Type u_1E:Type u_2inst✝:PseudoMetricSpace EΦ:ℝ → E → Ex₀✝:Es:Set Ex₀:Eε:ℝhε:0 < εδ:ℝ⊢ (∀ t ∈ Ici 0, ∀ x ∈ ball x₀ δ, Φ t x ∈ ball x₀ ε) ↔ ∀ t ≥ 0, ∀ (x : E), dist x x₀ < δ → dist (Φ t x) x₀ < ε All goals completed! 🐙

More generally, we can take the set neighbourhood filter nhdsSet s, then we have

example (hs : IsCompact s) (hs' : s.Nonempty) : (𝓝ˢ s).IsStableOn Φ (Ici 0) ↔ ∀ ε > 0, ∃ δ > 0, ∀ t ≥ 0, ∀ x, infDist x s < δ → infDist (Φ t x) s < ε := α:Type u_1E:Type u_2inst✝:PseudoMetricSpace EΦ:ℝ → E → Ex₀:Es:Set Ehs:IsCompact shs':s.Nonempty⊢ (𝓝ˢ s).IsStableOn Φ (Ici 0) ↔ ∀ ε > 0, ∃ δ > 0, ∀ t ≥ 0, ∀ (x : E), infDist x s < δ → infDist (Φ t x) s < ε α:Type u_1E:Type u_2inst✝:PseudoMetricSpace EΦ:ℝ → E → Ex₀:Es:Set Ehs:IsCompact shs':s.Nonempty⊢ (∀ (i : ℝ), 0 < i → ∃ i', 0 < i' ∧ ∀ t ∈ Ici 0, ∀ x ∈ thickening i' s, Φ t x ∈ thickening i s) ↔ ∀ ε > 0, ∃ δ > 0, ∀ t ≥ 0, ∀ (x : E), infDist x s < δ → infDist (Φ t x) s < ε α:Type u_1E:Type u_2inst✝:PseudoMetricSpace EΦ:ℝ → E → Ex₀:Es:Set Ehs:IsCompact shs':s.Nonemptyε:ℝhε:0 < εδ:ℝ⊢ (∀ t ∈ Ici 0, ∀ x ∈ thickening δ s, Φ t x ∈ thickening ε s) ↔ ∀ t ≥ 0, ∀ (x : E), infDist x s < δ → infDist (Φ t x) s < ε All goals completed! 🐙