Lemma 8.6 — $W^-(x) \subseteq \omega_+(E)$ for every $x \in \omega_+(E)$ (8.11)

Proved

TeschlODE.HigherDim.unstableSet_subset_omegaPlusSet

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

attractordynamical-systemsp2o-batch-books5p2o-gran-per-chapterp2o-plan-bookp2o-v1unstable-set

Let $M \subseteq \mathbb{R}^n$ be open, $f \in C^1(M, \mathbb{R}^n)$ , $\Phi$ the flow of $\dot x = f(x)$ on $M$ , and $E$ a trapping region. Then

W^-(x) \subseteq \omega_+(E) \qquad \text{for all } x \in \omega_+(E), \qquad (8.11)

where $W^-(x) = W^-(\{x\})$ is the set of points whose solution exists for all negative times and tends to $x$ as $t \to -\infty$ .

In words: an attracting set obtained from a trapping region contains the unstable manifolds of all its points — which is why it can contain repelling fixed points (the example (8.3)).

Formalization Note. Standing assumptions as for Lemma 8.5. $W^-(x)$ is the unstable set (8.8) of the singleton $\{x\}$ , i.e. stableSet M I Φ (-1) {x}.

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_IsTrappingRegion

Formal statement

namespace TeschlODE.HigherDim

/-- Teschl, Lemma 8.6, p. 232, (8.11): for a trapping region `E`, the unstable set
`W⁻(x) = W⁻({x})` of every point `x ∈ ω₊(E)` is contained in `ω₊(E)`. -/
theorem unstableSet_subset_omegaPlusSet {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) :
    ∀ x ∈ omegaPlusSet M I Φ E, stableSet M I Φ (-1) {x} ⊆ 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.6, Eq. (8.11)

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 an open order-connected set containing $0$ ;
$\Phi(0,x) = x$ ;
$\Phi(t,x) \in M$ and $\partial_t \Phi(t,x) = f(\Phi(t,x))$ on $I(x)$ ;
every integral curve of $f$ in $M$ through $x$ at time $0$ , on an open order-connected $J \ni 0$ , has $J \subseteq I(x)$ and coincides with $\Phi(\cdot,x)$ on $J$ .

Hypothesis on $E$ . $E$ 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$ ;
every $x \in \overline{E}$ and every $t > 0$ satisfy $t \in I(x)$ and $\Phi(t,x) \in E$ .

The set $\omega_+(E)$ . Let $\omega_+(E)$ be the set of $y \in M$ for which there are $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. For every $x \in \omega_+(E)$ , the set

W^-(\{x\}) = \Big\{ z \in M \;:\; (-\infty,0] \subseteq I(z)\ \text{ and }\ \lim_{s\to+\infty} \|\Phi(-s,z) - x\| = 0 \Big\}

is contained in $\omega_+(E)$ . This is the set of points of $M$ whose solution exists for all non-positive times and converges to $x$ as time $\to -\infty$ .

Degenerate cases. If $\omega_+(E)$ is empty, the statement is vacuous. The trapping-region hypothesis forces $E \neq \emptyset$ . If $n = 0$ , everything reduces to the single point $0$ , and the inclusion is $\{0\} \subseteq \{0\}$ or trivially vacuous.

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.6 — W−(x)⊆ω+(E)W^-(x) \subseteq \omega_+(E)W−(x)⊆ω+​(E) for every x∈ω+(E)x \in \omega_+(E)x∈ω+​(E) (8.11)

Lemma 8.6 — $W^-(x) \subseteq \omega_+(E)$ for every $x \in \omega_+(E)$ (8.11)