Lyapunov Functions for Discrete Systems in Lean

Start with a descending calculation

Let

Starting at \(x=4\) gives

The identities

show three different facts. The first identifies the reference value. The second is positive definiteness. The third is a quantified descent estimate. Together with the explicit orbit formula, this example exhibits convergence to zero. It does not establish a theorem for arbitrary maps or certificates.

Five ingredients, kept separate

For a region \(S\subseteq X\), the module records:

1. IsNonnegativeOn V S: \(0\le V(x)\) for \(x\in S\);
2. IsPositiveDefiniteOn V p S: \(p\in S\), \(V(p)=0\), and \(V(x)\gt0\) for \(x\in S\setminus\{p\}\);
3. IsWeakLyapunovDecreaseOn f V S: \(V(f(x))\le V(x)\) on \(S\);
4. IsStrictLyapunovDecreaseOn f V p S: \(V(f(x))\lt V(x)\) on \(S\setminus\{p\}\);
5. HasSublevelControlAt V p: every requested metric ball around \(p\) contains some positive open sublevel of \(V\).

The first and second conditions are not synonyms. The constant zero function is nonnegative, but it cannot distinguish \(p\) from any other state. The third and fourth conditions are also different. The identity map makes every certificate weakly decrease by equality, yet a nonfixed starting state never approaches \(p\).

The region parameter prevents a local calculation from being narrated as a global conclusion. Forward invariance is not hidden in either descent predicate. It is supplied separately whenever the proof follows an orbit through \(S\).

Difference notation and Mathlib minima

The source defines

def lyapunovDifference (f : X → X) (V : X → ℝ) (x : X) : ℝ :=
  V (f x) - V x

Thus weak descent is equivalent to \(\Delta V(x)\le0\), checked by isWeakLyapunovDecreaseOn_iff_difference_nonpos. Strict descent away from the reference point is equivalent to \(\Delta V(x)\lt0\), checked by isStrictLyapunovDecreaseOn_iff_difference_neg.

IsPositiveDefiniteOn.isNonnegativeOn proves the one-way sign implication. IsPositiveDefiniteOn.isMinOn connects the project predicate to Mathlib’s weak IsMinOn. If the selected region is a neighborhood, IsPositiveDefiniteOn.isLocallyPositiveDefiniteAt yields the local project predicate, and IsLocallyPositiveDefiniteAt.isLocalMin yields Mathlib’s weak local-minimum predicate. Mathlib’s minimum predicates do not encode strict positivity away from one point, so the project retains that information in a separate definition.

If \(p\) is fixed, strict descent away from \(p\) implies weak descent on the same region. The checked theorem is IsStrictLyapunovDecreaseOn.isWeakLyapunovDecreaseOn. Fixedness is necessary to handle the missing case \(x=p\): strict descent deliberately says nothing there.

Sublevels trap the scalar sequence

Suppose \(f(S)\subseteq S\) and \(V(f(x))\le V(x)\) for \(x\in S\). Then the closed sublevel

and the open sublevel \(S\cap\{x:V(x)\lt c\}\) are forward invariant. The source names these results IsWeakLyapunovDecreaseOn.mapsTo_closedSublevel and IsWeakLyapunovDecreaseOn.mapsTo_openSublevel.

Induction gives

for every start \(x\in S\); this is IsWeakLyapunovDecreaseOn.iterate_le. The stronger order statement IsWeakLyapunovDecreaseOn.antitone_orbit says that

is antitone. It proves monotonicity of scalar values, not convergence of states. An antitone nonnegative sequence has a scalar limit, but that limit need not be zero.

The stability bridge

Pointwise positive definiteness is not enough to manufacture a uniform lower bound away from \(p\) on an arbitrary noncompact or infinite-dimensional space. The module therefore names the needed comparison explicitly:

def HasSublevelControlAt [PseudoMetricSpace X]\n    (V : X → ℝ) (p : X) : Prop :=\n  ∀ ε > 0, ∃ c > 0, ∀ x, V x < c → dist x p < ε

The theorem isLyapunovStableFixedPoint_of_continuousAt_of_sublevelControl assumes:

• \(p\) is fixed;
• \(V(p)=0\);
• \(V\) is continuous at \(p\);
• HasSublevelControlAt V p;
• weak decrease on the whole state space.

Continuity makes each positive sublevel a neighborhood of \(p\). Weak descent keeps later iterates inside the same sublevel. Sublevel control places that trapped orbit inside the requested epsilon ball. The conclusion is the existing IsLyapunovStableFixedPoint f p, not attraction.

Attraction needs a zero limit

The theorem isAttractedTo_of_tendsto_lyapunov begins with an additional fact:

Sublevel control then turns eventual smallness of the scalar value into \(d(f^n(x),p)\to0\). This conclusion concerns one selected start. If the zero-limit premise holds for every start, isGloballyAttractingFixedPoint_of_tendsto_lyapunov gives the existing global attraction predicate. Finally, isAsymptoticallyStableFixedPoint_of_lyapunov combines the stability bridge with universal zero-energy convergence. Its conclusion is asymptotic stability; its premises still display the two separate obligations.

Strict one-step descent is not substituted for the zero-limit premise. On a noncompact space, a strictly decreasing scalar sequence may converge to a positive number. Compact trapping, coercive sublevels, comparison functions, or a discrete LaSalle argument can close that gap in later modules.

Declaration-complete source map

Six #print axioms commands audit the main order, stability, and attraction bridges. The warning-fatal full project check must report no sorryAx before this milestone is called checked.

Reproduce the checks

The countdown worksheet in the paired Deep Dive is a standalone tutorial that imports only Std:

elan run leanprover/lean4:v4.32.0 lean \
  site/content/knowledge-base/deep-dives/lyapunov-functions-and-the-direct-method-in-discrete-time/countdown-energy.lean

The authoritative source is a full project check using pinned Lean and Mathlib dependencies and may require substantial disk space or setup time:

git clone https://github.com/tdj28/nonlinear-dynamics-lean.git
cd nonlinear-dynamics-lean/formalization
lake env lean -DwarningAsError=true \
  NonlinearDynamics/Deterministic/Discrete/Lyapunov.lean

lake env lean selects the pinned project environment. The warning option rejects warnings. The command is portable across macOS and Linux after the dependencies are installed.

Lean’s elaborator constructs candidate proof terms and its kernel checks them against the formal statements. That process does not by itself establish that one certificate models a physical energy, nor that these definitions cover every convention in stability theory.

Exact nonclaims

This slice proves no compact LaSalle invariance principle, converse Lyapunov theorem, exponential rate, uniqueness theorem, invariant-set or periodic-orbit criterion, stable-manifold result, ODE theorem, derivative criterion, structural or stochastic robustness theorem, or Lyapunov-exponent statement. A local certificate gives no global basin conclusion. Weak descent does not imply attraction. Strict descent alone is not promoted to attraction without an explicit zero-limit, compactness, coercivity, or comparison argument.

The next Conjugacies and Semiconjugacies Research Note studies when a coordinate map transports iterates and attraction. It does not assume that a Lyapunov certificate or numerical decay rate survives an arbitrary change of coordinates.

References

• J. P. LaSalle, “Difference Equations. Discrete Semidynamical Systems,” especially sections 6, 7, and 10, in The Stability of Dynamical Systems, SIAM CBMS 25 (1976), pages 1–25, DOI 10.1137/1.9781611970432.ch1.
• Saber Elaydi, “Stability Theory,” Chapter 4 of An Introduction to Difference Equations, third edition, especially Theorems 4.20 and 4.24, DOI 10.1007/0-387-27602-5_4.
• S. P. Gordon, “On Converses to the Stability Theorems for Difference Equations,” SIAM Journal on Control 10(1), 76–81 (1972), DOI 10.1137/0310007.
• Mathlib 4.32.0, pinned revision 81a5d257, especially Topology.Order.LocalExtr, Order.Filter.Extr, Topology.MetricSpace.Pseudo.Defs, Data.Set.Function, and Logic.Function.Iterate.