Lemma 8.5 — a trapping region yields a nonempty, invariant, compact, connected attracting set $\omega_+(E)$

Proved

TeschlODE.HigherDim.trapping_region_attracting

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

attractordynamical-systemslimit-setp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1trapping-region

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)$ on $M$ . Let $E$ be a trapping region. Then

\Lambda = \omega_+(E) = \bigcap_{t \ge 0} \Phi(t, E) \qquad (8.10)

is a nonempty, invariant, compact, and connected attracting set.

Lemma 8.5 is how attracting sets are found in practice: exhibit a region into which the vector field points (for the Lorenz equation, a sublevel set of a Liapunov-type function), and $\omega_+(E)$ is the attractor.

Formalization Note. The standing assumptions of Chapter 6 ( $M$ open, $f \in C^1$ ) are binders. The book assumes the flow complete in Chapter 8; the statement uses the local flow, which is more general: the trapping-region definition already makes every point of $\overline E$ forward complete. "Invariant" is the book's two-sided invariance (every orbit through $\Lambda$ stays in $\Lambda$ ); "attracting" is $W^+(\Lambda)$ being a neighborhood of $\Lambda$ .

Preamble

import Mathlib
import Definitions.Def_TeschlODE_HigherDim_IsIntegralCurve
import Definitions.Def_TeschlODE_HigherDim_IsMaximalFlow
import Definitions.Def_TeschlODE_HigherDim_omegaPlusSet
import Definitions.Def_TeschlODE_HigherDim_stableSet
import Definitions.Def_TeschlODE_HigherDim_IsInvariant
import Definitions.Def_TeschlODE_HigherDim_IsAttracting
import Definitions.Def_TeschlODE_HigherDim_IsTrappingRegion

Formal statement

namespace TeschlODE.HigherDim

/-- Teschl, Lemma 8.5, p. 232, (8.10): for a trapping region `E` of the flow of a `C¹` vector
field on the open set `M ⊆ ℝⁿ`, `Λ = ω₊(E) = ⋂_{t ≥ 0} Φ(t, E)` is a nonempty, invariant,
compact, and connected attracting set. -/
theorem trapping_region_attracting {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 Φ)
    (E : Set (EuclideanSpace ℝ (Fin n))) (hE : IsTrappingRegion M I Φ E) :
    omegaPlusSet M I Φ E = (⋂ t : ℝ, ⋂ (_ : 0 ≤ t), Φ t '' E) ∧
      (omegaPlusSet M I Φ E).Nonempty ∧ IsInvariant M I Φ (omegaPlusSet M I Φ E) ∧
      IsCompact (omegaPlusSet M I Φ E) ∧ IsConnected (omegaPlusSet M I Φ E) ∧
      IsAttracting M I Φ (omegaPlusSet M I Φ E) := by sorry

end TeschlODE.HigherDim

Source

Teschl, Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS GSM 140, 2012), p. 232, Lemma 8.5, Eq. (8.10)

Read-back

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

Inputs. Fix the following:

a natural number $n$ ;
an open set $M \subseteq \mathbb{R}^n$ (Euclidean);
a map $f : \mathbb{R}^n \to \mathbb{R}^n$ that is $C^1$ on $M$ ;
time sets $I(x) \subseteq \mathbb{R}$ ;
a map $\Phi : \mathbb{R} \times \mathbb{R}^n \to \mathbb{R}^n$ .

Hypothesis on $(I, \Phi)$ . $(I,\Phi)$ is a maximal flow of $f$ on $M$ . This means that for every $x \in M$ all of the following hold:

$I(x)$ is open and order-connected and contains $0$ ;
$\Phi(0,x) = x$ ;
$\Phi(t,x) \in M$ and $\partial_t \Phi(t,x) = f(\Phi(t,x))$ for all $t \in I(x)$ ;
every curve $\psi$ with $\psi(0) = x$ that is an integral curve of $f$ in $M$ on an open order-connected $J \ni 0$ has $J \subseteq I(x)$ and $\psi = \Phi(\cdot,x)$ on $J$ .

Hypothesis on $E$ . $E \subseteq \mathbb{R}^n$ is a trapping region. This means all of the following:

$E$ is open, nonempty and connected;
$\overline{E}$ is compact and $\overline{E} \subseteq M$ ;
for every $x \in \overline{E}$ and every $t > 0$ : $t \in I(x)$ and $\Phi(t,x) \in E$ .

The set $\Lambda$ . Let $\Lambda = \omega_+(E)$ be the set of $y \in M$ for which there are sequences $x_k \in E$ and $t_k \in I(x_k)$ with $t_k \to +\infty$ and $\Phi(t_k,x_k) \to y$ .

Conclusion. All of the following hold:

$\displaystyle \Lambda = \bigcap_{t \ge 0} \Phi_t(E)$ , where $\Phi_t(E) = \{\Phi(t,x) : x \in E\}$ .
$\Lambda$ is nonempty.
$\Lambda$ is invariant: $\Lambda \subseteq M$ , and $\Phi(t,x) \in \Lambda$ for all $x \in \Lambda$ and $t \in I(x)$ .
$\Lambda$ is compact.
$\Lambda$ is connected, which includes being nonempty.
$\Lambda$ is attracting. This means $\Lambda$ is invariant and the set

W^+(\Lambda) = \Big\{x \in M : [0,\infty) \subseteq I(x),\ \lim_{s\to+\infty} \inf_{w\in\Lambda}\|\Phi(s,x) - w\| = 0\Big\}

contains an open set that contains $\Lambda$ .

Degenerate cases. The trapping-region hypothesis forces $E \neq \emptyset$ . If $n = 0$ , $\mathbb{R}^0$ is a single point $\{0\}$ ; the only possible $E$ is $\{0\} = M$ , $f \equiv 0$ , and $\Phi(t,0) = 0$ on $I(0) = \mathbb{R}$ .

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

Lemma 8.5 — a trapping region yields a nonempty, invariant, compact, connected attracting set ω+(E)\omega_+(E)ω+​(E)

Lemma 8.5 — a trapping region yields a nonempty, invariant, compact, connected attracting set $\omega_+(E)$