3.2. Asymptotic stability🔗

Global asymptotic stability requires that an equilibrium point is Lyapunov stable and all trajectories converge to the equilibrium point. In Lean, we are not defining a predicate for this, so to state that a point is asymptotic stable, one simply writes that it is stable and all trajectories converge. We note that in the case of the filter nhdsSet s, we can check convergence similarly to the convergence of points

variable {f : α → E} {l : Filter α}

example (hs₁ : IsCompact s) (hs₂ : Set.Nonempty s) :
    Tendsto f l (𝓝ˢ s) ↔
    ∀ ε > 0, ∀ᶠ x in l, infDist (f x) s < ε := byα:Type u_1E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:NormedSpace ℝ EΦ:ℝ → E → Ex₀:Es:Set Ef:α → El:Filter αhs₁:IsCompact shs₂:s.Nonempty⊢ Tendsto f l (𝓝ˢ s) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, infDist (f x) s < ε
  exact tendsto_nhdsSet hs₁ hs₂All goals completed! 🐙

Local asymptotic stability is defined being locally attractive and stable, where locally attractive means that the flow of points close to the set converge to the set:

def

Filter.IsAttractive.{u_1, u_2} {ι : Type u_1} {E : Type u_2}
  {l : Filter E} {Φ : ι → E → E} {l' : Filter ι} : Prop
Filter.IsAttractive.{u_1, u_2}
  {ι : Type u_1} {E : Type u_2}
  {l : Filter E} {Φ : ι → E → E}
  {l' : Filter ι} : Prop

A filter l is attractive with respect to a filter l' if l-eventually t ↦ Φ t x converges to l along l'. The main case is that l = 𝓝 x₀ and l' = atTop, then the condition becomes that for all x sufficiently close to x₀, t ↦ Φ t x converges to x₀ as t → +∞.

This condition is usually called local attractiveness. Global attractiveness means that for every x, Φ · x converges to l along l'.

For non-autonomous systems with flow Φ : ℝ → ℝ → E → E the forward attractiveness becomes ∀ t₀ ∈ Set.Ici t₀, l.IsAttractive (Φ t₀) atTop.