Theorem 6.14 (Krasovskii–LaSalle principle)

Proved

TeschlODE.Stability.krasovskii_lasalle

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

lasalleliapunov-functionordinary-differential-equationsp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1stability

Let $M \subseteq \mathbb{R}^n$ be open, $f \in C^1(M, \mathbb{R}^n)$ , and $\Phi$ the flow of $\dot x = f(x)$ with maximal intervals $I_x$ and orbits $\gamma(y) = \Phi(I_y \times \{y\})$ . Suppose $x_0 \in M$ is a fixed point of $f$ and $L$ is a Liapunov function at $x_0$ on the open neighborhood $U = U(x_0) \subseteq M$ . Say that $L$ is not constant on any orbit lying entirely in $U \setminus \{x_0\}$ if

\forall y \in M:\quad \gamma(y) \subseteq U \setminus \{x_0\} \ \Longrightarrow\ \exists\, a, b \in \gamma(y),\ L(a) \ne L(b). \qquad (\ast)

Then:

if $(\ast)$ holds, $x_0$ is asymptotically stable;
if $L$ is a strict Liapunov function, $(\ast)$ holds;
if $(\ast)$ holds, then every $x \in M$ whose forward orbit $\gamma_+(x)$ lies in a compact subset $C$ of $U$ has $\Phi(t, x)$ defined for all $t \ge 0$ and $\Phi(t, x) \to x_0$ as $t \to \infty$ .

This is the central stability criterion of the chapter: asymptotic stability from a Liapunov function that is merely non-increasing, provided it is not constant on a whole orbit.

Formalization Note. The flow is local; no completeness is assumed anywhere. Part 3 corrects the book's "every orbit lying entirely in $U(x_0)$ converges to $x_0$ ", which is false as printed: for $\dot x_1 = -6x_1/(1+x_1^2)^2 + 2x_2$ , $\dot x_2 = -2(x_1 + x_2)/(1+x_1^2)^2$ on $M = U = \mathbb{R}^2$ , $L = x_1^2/(1+x_1^2) + x_2^2$ is a strict Liapunov function, yet orbits starting in $\{x_1 > \sqrt2,\ x_2 > 2/(x_1 - \sqrt2)\}$ stay in that region and do not converge to $0$ (Khalil, Nonlinear Systems, 3rd ed., §4.1). The book's argument (the text before Theorem 6.14) needs $\omega_+(x)$ to be a nonempty subset of $U$ , which is exactly what a forward orbit inside a compact $C \subseteq U$ provides. Parts 1 and 2 are as printed.

Preamble

import Mathlib
import Definitions.Def_TeschlODE_Stability_IsIntegralCurve
import Definitions.Def_TeschlODE_Stability_IsMaximalFlow
import Definitions.Def_TeschlODE_Stability_IsLiapunovFunction
import Definitions.Def_TeschlODE_Stability_IsStrictLiapunovFunction
import Definitions.Def_TeschlODE_Stability_semiOrbit
import Definitions.Def_TeschlODE_Stability_orbit
import Definitions.Def_TeschlODE_Stability_IsStable
import Definitions.Def_TeschlODE_Stability_IsAsymptoticallyStable

Formal statement

namespace TeschlODE.Stability

theorem krasovskii_lasalle {n : ℕ}
    (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (M : Set (EuclideanSpace ℝ (Fin n))) (hM : IsOpen M) (hf : ContDiffOn ℝ 1 f M)
    (I : EuclideanSpace ℝ (Fin n) → Set ℝ)
    (Φ : ℝ → EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hΦ : IsMaximalFlow f M I Φ)
    (x₀ : EuclideanSpace ℝ (Fin n)) (hx₀ : x₀ ∈ M) (hfix : f x₀ = 0)
    (U : Set (EuclideanSpace ℝ (Fin n))) (L : EuclideanSpace ℝ (Fin n) → ℝ)
    (hL : IsLiapunovFunction f M x₀ U L) :
    -- (i) L not constant on any orbit lying entirely in U \ {x₀} ⇒ x₀ asymptotically stable
    ((∀ y ∈ M, orbit I Φ y ⊆ U \ {x₀} → ∃ a ∈ orbit I Φ y, ∃ b ∈ orbit I Φ y, L a ≠ L b) →
      IsAsymptoticallyStable M I Φ x₀) ∧
    -- (ii) a strict Liapunov function is not constant on any orbit lying entirely in U \ {x₀}
    (IsStrictLiapunovFunction f M x₀ U L →
      ∀ y ∈ M, orbit I Φ y ⊆ U \ {x₀} → ∃ a ∈ orbit I Φ y, ∃ b ∈ orbit I Φ y, L a ≠ L b) ∧
    -- (iii) under the hypothesis of (i), every forward orbit lying in a compact subset of U
    -- exists for all t ≥ 0 and converges to x₀
    ((∀ y ∈ M, orbit I Φ y ⊆ U \ {x₀} → ∃ a ∈ orbit I Φ y, ∃ b ∈ orbit I Φ y, L a ≠ L b) →
      ∀ x ∈ M, ∀ C : Set (EuclideanSpace ℝ (Fin n)), IsCompact C → C ⊆ U →
        semiOrbit 1 I Φ x ⊆ C →
        (∀ t : ℝ, 0 ≤ t → t ∈ I x) ∧
          Filter.Tendsto (fun t => Φ t x) Filter.atTop (nhds x₀)) := by sorry

end TeschlODE.Stability

Source

Teschl, Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS GSM 140, 2012), p. 202, Theorem 6.14

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

The declaration concerns vectors in $\mathbb{R}^n$ (the Euclidean space $\mathbb{R}^n$ with coordinates indexed by $\{0,\dots,n-1\}$ ), where $n\ge 0$ is any natural number. It takes the following data and hypotheses:

$f:\mathbb{R}^n\to\mathbb{R}^n$ is a vector field defined on all of $\mathbb{R}^n$ .
$M\subseteq\mathbb{R}^n$ is an open set, and $f$ is continuously differentiable ( $C^1$ ) on $M$ . Nothing is assumed about $f$ outside $M$ .
$I$ assigns to each point $x\in\mathbb{R}^n$ a set of times $I(x)\subseteq\mathbb{R}$ . Nothing is assumed about $I(x)$ being an interval, containing $0$ , or being nonempty, except what the next hypothesis supplies.
$\Phi:\mathbb{R}\times\mathbb{R}^n\to\mathbb{R}^n$ , written $\Phi(t,x)$ , is defined for every real $t$ and every $x$ . Its values at times $t\notin I(x)$ are whatever $\Phi$ happens to return.
The bundle predicate $\mathrm{IsMaximalFlow}(f,M,I,\Phi)$ holds. Its body is not shown here. The statement relies on it for any link between $\Phi$ , $I$ and solutions of $\dot x=f(x)$ in $M$ , and for any properties of $I$ .
$x_0\in M$ is a point with $f(x_0)=0$ .
$U\subseteq\mathbb{R}^n$ is a set, and $L:\mathbb{R}^n\to\mathbb{R}$ is a real function. The bundle predicate $\mathrm{IsLiapunovFunction}(f,M,x_0,U,L)$ holds, and its body is not shown here. The statement itself does not require $U$ to be open, to contain $x_0$ , to be a neighbourhood of $x_0$ , or to lie inside $M$ . Any such property can only come from that predicate.

Two bundle notions describe trajectories. $\mathrm{orbit}(I,\Phi,y)$ is the set named "orbit" of $y$ , built from $I$ and $\Phi$ . $\mathrm{semiOrbit}(1,I,\Phi,x)$ is the set named "semiOrbit", built from the parameter $1$ , $I$ , $\Phi$ and $x$ . Their definitions are not shown, so it is not visible here which times they use, or whether the parameter $1$ selects the forward direction. $\mathrm{IsAsymptoticallyStable}(M,I,\Phi,x_0)$ and $\mathrm{IsStrictLiapunovFunction}(f,M,x_0,U,L)$ are also bundle predicates whose bodies are not shown. $\mathrm{IsAsymptoticallyStable}$ depends only on $M$ , $I$ , $\Phi$ and $x_0$ , and not on $f$ , $U$ or $L$ .

To shorten the conclusions, write $(\mathrm{N})$ for the following condition. For every $y\in M$ with

\mathrm{orbit}(I,\Phi,y)\subseteq U\setminus\{x_0\},

there exist $a,b\in\mathrm{orbit}(I,\Phi,y)$ with $L(a)\neq L(b)$ . In words: $L$ takes at least two distinct values on every orbit that starts in $M$ and lies entirely in $U\setminus\{x_0\}$ . Orbits that leave $U$ at any point, or that contain $x_0$ , are not constrained by $(\mathrm{N})$ .

Under all the hypotheses above, the declaration asserts that the following three statements all hold:

(i) If $(\mathrm{N})$ holds, then $\mathrm{IsAsymptoticallyStable}(M,I,\Phi,x_0)$ holds.
(ii) If $\mathrm{IsStrictLiapunovFunction}(f,M,x_0,U,L)$ holds, then $(\mathrm{N})$ holds.
(iii) Suppose $(\mathrm{N})$ $(N)$ holds. Take any $x\in M$ $x \in M$ and any compact set $C\subseteq\mathbb{R}^n$ $C \subseteq R^{n}$ with $C\subseteq U$ $C \subseteq U$ and $\mathrm{semiOrbit}(1,I,\Phi,x)\subseteq C$ $semiOrbit (1, I, Φ, x) \subseteq C$ . Then:
- every $t\ge 0$ lies in $I(x)$ , that is, $[0,\infty)\subseteq I(x)$ ; and

\lim_{t\to+\infty}\Phi(t,x)=x_0,

where the limit is taken over real $t$ in the usual topology of $\mathbb{R}^n$ .

Part (iii) does not assume that $x\neq x_0$ , that $x\in U$ , or that $C$ is nonempty. Its only link to the trajectory is the containment of the semi-orbit in $C$ .

Degenerate cases, with the caveat that several depend on bundle definitions not shown here:

$n=0$ . The space $\mathbb{R}^0$ is a single point, so $f\equiv 0$ , $x_0$ is that point, and $M=\mathbb{R}^0$ . Then $U\setminus\{x_0\}=\varnothing$ . An orbit lies inside it only if the orbit is empty, and then no $a,b$ can be found in it. So $(\mathrm{N})$ holds exactly when no $y\in M$ has an empty orbit. The limit in (iii) holds automatically, because every function into a one-point space converges to that point.
$M$ empty. This is impossible, since $x_0\in M$ .
$U$ empty, or $x_0\notin U$ . The statement itself allows both. For $U=\varnothing$ , the only compact $C\subseteq U$ is $C=\varnothing$ .
$C=\varnothing$ . The premise $\mathrm{semiOrbit}(1,I,\Phi,x)\subseteq\varnothing$ holds only if that semi-orbit is empty. In that case (iii) still requires $[0,\infty)\subseteq I(x)$ and $\Phi(t,x)\to x_0$ . Whether a semi-orbit can be empty (for example, when $I(x)=\varnothing$ ) is decided by the unseen definitions of $\mathrm{semiOrbit}$ and $\mathrm{IsMaximalFlow}$ .
An empty orbit $\mathrm{orbit}(I,\Phi,y)$ . It is contained in $U\setminus\{x_0\}$ , but no $a,b$ exist in it. So $(\mathrm{N})$ fails if any $y\in M$ has an empty orbit. In that case (i) and (iii) become vacuous, and (ii) asserts that strictness excludes empty orbits.
Values of $\Phi$ at times outside $I(x)$ . These are unconstrained by the statement. The limit in (iii) only involves large $t$ , and the first conclusion of (iii) places all such $t$ in $I(x)$ .
Hypotheses that may be unsatisfiable. Whether $\mathrm{IsMaximalFlow}$ or $\mathrm{IsLiapunovFunction}$ can be satisfied, and so whether the whole statement is vacuous, depends on their definitions, which are not shown.

Human review

Endorsed by Shuze Chen · Oct 2, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 2, 2026
Confirmed by the mission captain (proposal self-audit).

View graph