Stability.LaSalle

LaSalle's invariance principle and its corollaries (Barbashin–Krasovskii theorems).

Main results

• lasalle_invariance_principle — if Ω is compact and positively invariant, V is C¹ with V̇ ≤ 0 on Ω, and ω(φ) ⊆ M for a closed set M, then φ(t) → M.
• lasalle_local_asymptotic_stable (Barbashin's theorem) — local asymptotic stability via a compact sublevel set and LaSalle.
• lasalle_global_asymptotic_stable (Krasovskii's theorem) — global asymptotic stability when V is radially unbounded and V̇ ≤ 0 everywhere.

Proof strategy

1. V_antitoneOn_lasalle: V ∘ φ is antitone on [0, ∞) (Lie derivative ≤ 0 on Ω).
2. lasalle_V_tendsto: V(φ t) → L via monotone convergence on the compact orbit.
3. V_const_on_omegaLimit: V = L on ω(φ) (cluster-point argument).
4. omegaLimit_subset_of_invariant: ω(φ) ⊆ Ω since Ω is closed and φ stays in Ω.
5. The main theorem combines these to show φ t → M via the open-neighborhood criterion.

noncomputable def omegaLimitTraj {n : ℕ} (φ : ℝ → EuclideanSpace ℝ (Fin n)) : Set (EuclideanSpace ℝ (Fin n))

ω-limit set of trajectory φ, using Mathlib's omegaLimit with the trivial flow.

Equations

• omegaLimitTraj φ = omegaLimit Filter.atTop (fun (t : ℝ) (x : Unit) => φ t) Set.univ

Lemma 1: V antitone on [0,∞) along trajectories

theorem V_antitoneOn_lasalle {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} {V : EuclideanSpace ℝ (Fin n) → ℝ} {Ω : Set (EuclideanSpace ℝ (Fin n))} (hV_c1 : ContDiff ℝ 1 V) (hLie : ∀ x ∈ Ω, (fderiv ℝ V x) (f x) ≤ 0) {φ : ℝ → EuclideanSpace ℝ (Fin n)} (htraj : IsTrajectory φ f) (hphi : ∀ t ≥ 0, φ t ∈ Ω) : AntitoneOn (V ∘ φ) (Set.Ici 0)

V(φ t) is antitone on [0, ∞) when the Lie derivative V̇ ≤ 0 on Ω and φ stays in Ω.

Lemma 2: V(φ t) converges to its infimum

theorem lasalle_V_tendsto {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} {V : EuclideanSpace ℝ (Fin n) → ℝ} {Ω : Set (EuclideanSpace ℝ (Fin n))} (hV_c1 : ContDiff ℝ 1 V) (hΩ_compact : IsCompact Ω) (hΩ_inv : IsPositivelyInvariant Ω f) (hLie : ∀ x ∈ Ω, (fderiv ℝ V x) (f x) ≤ 0) {φ : ℝ → EuclideanSpace ℝ (Fin n)} (htraj : IsTrajectory φ f) (hφ0 : φ 0 ∈ Ω) : ∃ (L : ℝ), Filter.Tendsto (V ∘ φ) Filter.atTop (nhds L)

If Ω is compact and positively invariant and the Lie derivative V̇ ≤ 0 on Ω, then V(φ t) converges to some limit L as t → ∞.

Lemma 3: V is constant on omegaLimitTraj(φ)

theorem V_const_on_omegaLimit {n : ℕ} {V : EuclideanSpace ℝ (Fin n) → ℝ} {φ : ℝ → EuclideanSpace ℝ (Fin n)} {L : ℝ} (hV_cont : Continuous V) (hVphi_tendsto : Filter.Tendsto (V ∘ φ) Filter.atTop (nhds L)) (y : EuclideanSpace ℝ (Fin n)) : y ∈ omegaLimitTraj φ → V y = L

If V(φ t) → L, then V(y) = L for every y ∈ ω(φ).

Lemma 4: omegaLimitTraj(φ) ⊆ Ω when Ω is compact and positively invariant

theorem omegaLimit_subset_of_invariant {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} {Ω : Set (EuclideanSpace ℝ (Fin n))} (hΩ_compact : IsCompact Ω) (hΩ_inv : IsPositivelyInvariant Ω f) {φ : ℝ → EuclideanSpace ℝ (Fin n)} (htraj : IsTrajectory φ f) (hφ0 : φ 0 ∈ Ω) : omegaLimitTraj φ ⊆ Ω

If Ω is compact, positively invariant, and φ 0 ∈ Ω, then ω(φ) ⊆ Ω.

Main theorem: LaSalle's invariance principle

theorem lasalle_invariance_principle {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} {V : EuclideanSpace ℝ (Fin n) → ℝ} {Ω M : Set (EuclideanSpace ℝ (Fin n))} (hΩ_compact : IsCompact Ω) (hΩ_inv : IsPositivelyInvariant Ω f) (hV_c1 : ContDiff ℝ 1 V) (hLie : ∀ x ∈ Ω, (fderiv ℝ V x) (f x) ≤ 0) {φ : ℝ → EuclideanSpace ℝ (Fin n)} (htraj : IsTrajectory φ f) (hφ0 : φ 0 ∈ Ω) (_hM_closed : IsClosed M) (hω_sub_M : omegaLimitTraj φ ⊆ M) : Filter.Tendsto φ Filter.atTop (nhdsSet M)

LaSalle's invariance principle.

Let Ω be compact and positively invariant for ẋ = f(x), V : ℝⁿ → ℝ a C¹ Lyapunov function with V̇(x) = DV(x)[f(x)] ≤ 0 on Ω, and M a closed set contained in Ω. If ω(φ) ⊆ M (which in the classical theorem follows from M being the largest invariant subset of E = {x ∈ Ω | V̇(x) = 0}, via ODE uniqueness), then φ(t) → M.

Barbashin–Krasovskii theorems

theorem lasalle_local_asymptotic_stable {n : ℕ} {D : Set (EuclideanSpace ℝ (Fin n))} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} {V : EuclideanSpace ℝ (Fin n) → ℝ} {x_eq : EuclideanSpace ℝ (Fin n)} (hn : 0 < n) (hV_c1 : ContDiff ℝ 1 V) (hV_local : IsLocalLyapunovFunction f V x_eq D) {c : ℝ} (hc_pos : 0 < c) (hΩ_sub_D : SublevelSet V c ⊆ D) (hΩ_compact : IsCompact (SublevelSet V c)) (hΩ_inv : IsPositivelyInvariant (SublevelSet V c) f) (hLasalle : ∀ (φ : ℝ → EuclideanSpace ℝ (Fin n)), IsTrajectory φ f → φ 0 ∈ SublevelSet V c → omegaLimitTraj φ ⊆ {x_eq}) : LocalAsymptoticStable f x_eq

Barbashin's theorem: local asymptotic stability via LaSalle. V C¹ and positive definite on D, V̇ ≤ 0 on D, compact sublevel set Ωc ⊆ D, every trajectory starting in Ωc has ω-limit set ⊆ {x_eq}.

theorem lasalle_global_asymptotic_stable {n : ℕ} {f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)} {V : EuclideanSpace ℝ (Fin n) → ℝ} {x_eq : EuclideanSpace ℝ (Fin n)} (hn : 0 < n) (hV_c1 : ContDiff ℝ 1 V) (hzero : V x_eq = 0) (hpos : ∀ (x : EuclideanSpace ℝ (Fin n)), x ≠ x_eq → 0 < V x) (hLie : ∀ (x : EuclideanSpace ℝ (Fin n)), (fderiv ℝ V x) (f x) ≤ 0) (hradial : Filter.Tendsto V (Filter.comap norm Filter.atTop) Filter.atTop) (hLasalle : ∀ (φ : ℝ → EuclideanSpace ℝ (Fin n)), IsTrajectory φ f → omegaLimitTraj φ ⊆ {x_eq}) : GlobalAsymptoticStable f x_eq

Krasovskii's theorem: global asymptotic stability via LaSalle. V C¹, positive definite, radially unbounded, V̇ ≤ 0 on ℝⁿ, every trajectory has ω-limit set ⊆ {x_eq}.