## Formalized Name Shadowing Lemma for Hyperbolic Sets ## Formalized Statement Let $M$ be a smooth manifold equipped with a Riemannian distance $d$, let $f:M\to M$ be a $C^1$ diffeomorphism, and let $\Lambda\subset M$ be a compact hyperbolic $f$-invariant set. Then there is a neighbourhood $N$ of $\Lambda$ with the following property. For every sufficiently small $\delta>0$, there exists $\varepsilon>0$ such that every bi-infinite $\varepsilon$-pseudo-orbit $(x_n)_{n\in\mathbb Z}$ contained in $\Lambda$, meaning \begin{align*} d(f(x_n),x_{n+1})<\varepsilon \end{align*} for every $n\in\mathbb Z$, is $\delta$-shadowed by a true orbit: there exists $y\in N$ such that \begin{align*} d(f^n(y),x_n)<\delta \end{align*} for every $n\in\mathbb Z$. If $\Lambda$ is locally maximal, then $N$ and $\delta$ may be chosen so that the shadowing point $y$ lies in $\Lambda$. ## Proof [proofplan] Use the local product structure and uniform hyperbolicity on a compact neighbourhood of $\Lambda$. A sufficiently accurate pseudo-orbit determines a sequence of local plaques; the bracket operation sends consecutive errors into stable and unstable coordinates. Solving the resulting bi-infinite correction equations by contraction gives a unique orbit that stays close to the pseudo-orbit. In the locally maximal case, the shadowing orbit remains in an isolating neighbourhood, hence belongs to $\Lambda$. [/proofplan] [step:Set up uniform hyperbolic coordinates] Because $\Lambda$ is compact and hyperbolic, the stable and unstable splitting \begin{align*} T_\Lambda M=E^s\oplus E^u \end{align*} has uniform contraction and expansion constants. Choose a neighbourhood $N$ of $\Lambda$ on which stable and unstable cone fields are defined and remain invariant under $Df$ and $Df^{-1}$ with uniform estimates. After shrinking $N$, the local stable and unstable plaques have a uniform size and the local product structure map is defined whenever two points of $N$ are sufficiently close. [/step] [step:Convert a pseudo-orbit into a contraction problem] Fix a small shadowing scale $\delta>0$. Choose $\varepsilon>0$ so small that every $\varepsilon$-pseudo-orbit $(x_n)_{n\in\mathbb Z}$ in $\Lambda$ has consecutive points lying in the common product-structure neighbourhood after applying $f$. In the adapted coordinates at each $x_n$, a candidate shadowing orbit can be written as a sequence of small corrections \begin{align*} v_n\in E^s_{x_n}\oplus E^u_{x_n}. \end{align*} The equation that the corrected points form an exact orbit is a bi-infinite system whose linear part is hyperbolic and whose nonlinear part has arbitrarily small Lipschitz constant once $\varepsilon$ and $\delta$ are chosen small enough. The inverse for the linear part is obtained by summing forward along stable directions and backward along unstable directions. The uniform hyperbolic estimates make this inverse bounded on the Banach space of bounded correction sequences. Therefore the full nonlinear correction operator is a contraction on the closed ball of correction sequences with norm at most a constant multiple of $\delta$. [/step] [step:Apply the contraction mapping theorem] By the contraction mapping theorem, the correction operator has a unique fixed correction sequence $(v_n)_{n\in\mathbb Z}$. Let $y$ be the corrected point at time $0$. The fixed-point equation gives \begin{align*} f^n(y)=\exp_{x_n}(v_n) \end{align*} in the chosen local coordinates for every $n\in\mathbb Z$. The correction norm bound gives \begin{align*} d(f^n(y),x_n)<\delta \end{align*} for every $n\in\mathbb Z$. Thus the pseudo-orbit is $\delta$-shadowed by the true orbit of $y$. [/step] [step:Use local maximality to keep the shadowing point in the hyperbolic set] Assume now that $\Lambda$ is locally maximal. Choose an isolating neighbourhood $U$ such that \begin{align*} \Lambda=\bigcap_{n\in\mathbb Z}f^n(U). \end{align*} Take $\delta>0$ small enough that the closed $\delta$-neighbourhood of $\Lambda$ in $N$ is contained in $U$. Since the pseudo-orbit lies in $\Lambda$ and the shadowing orbit satisfies \begin{align*} d(f^n(y),x_n)<\delta \end{align*} for every $n\in\mathbb Z$, the full orbit of $y$ remains in $U$. Hence \begin{align*} y\in\bigcap_{n\in\mathbb Z}f^n(U)=\Lambda. \end{align*} [guided] In the locally maximal case, choose an isolating neighbourhood $U$ such that \begin{align*} \Lambda=\bigcap_{n\in\mathbb Z}f^n(U). \end{align*} The shadowing estimate says \begin{align*} d(f^n(y),x_n)<\delta \end{align*} for every $n\in\mathbb Z$, and the pseudo-orbit points $x_n$ lie in $\Lambda$. If $\delta$ is small enough, every $f^n(y)$ lies in $U$. Therefore \begin{align*} y\in\bigcap_{n\in\mathbb Z}f^n(U)=\Lambda. \end{align*} This proves the locally maximal conclusion. [/guided] [/step]