Shadowing lemma

AbbreviationEuclidean model space for the shadowing lemma#✓fully proved

For a natural number \(d\), \(E_d\) is the Euclidean space \(\mathbb{R}^d\), the real \(d\)-tuples with the Euclidean norm.

abbrev E (d : ℕ) := EuclideanSpace ℝ (Fin d)

Used by 5

Used byShadowing property · Anosov–Bowen shadowing lemma · Hyperbolic structure · Hyperbolic invariant set · Pseudo-orbit

StructureHyperbolic structure#✓fully proved

Let \(T : \mathbb{R}^d \to \mathbb{R}^d\) be a homeomorphism and let \(K \subseteq \mathbb{R}^d\). Write \(DF_x\) for the derivative of a map \(F\) at \(x\), \(T^n\) for the \(n\)-fold iterate of \(T\) and \(T^{-n}\) for the \(n\)-fold iterate of \(T^{-1}\). A hyperbolic structure for \(T\) on \(K\) consists of the following: \(T\) and \(T^{-1}\) are \(C^1\); \(T(K) = K\); to every \(x \in \mathbb{R}^d\) are assigned linear subspaces \(E^s(x)\) and \(E^u(x)\) of \(\mathbb{R}^d\) such that for every \(x \in K\) we have \(\mathbb{R}^d = E^s(x) \oplus E^u(x)\), \(DT_x(E^s(x)) = E^s(T(x))\) and \(DT_x(E^u(x)) = E^u(T(x))\); and there are real numbers \(\lambda\) with \(0 < \lambda < 1\) and \(C > 0\) such that for every \(x \in K\) and every \(n \in \mathbb{N}\), \(\|D(T^n)_x v\| \le C \lambda^n \|v\|\) for all \(v \in E^s(x)\) and \(\|D(T^{-n})_x v\| \le C \lambda^n \|v\|\) for all \(v \in E^u(x)\).

MathlibExt.Dynamics.HyperbolicShadowingWanted.Dynamics.HyperbolicShadowingProblem.HyperbolicStructure · 20 lines

structure HyperbolicStructure (T : E d ≃ₜ E d) (K : Set (E d)) where
  contDiff_fwd : ContDiff ℝ 1 (T : E d → E d)
  contDiff_bwd : ContDiff ℝ 1 (T.symm : E d → E d)
  invariant : (T : E d → E d) '' K = K
  stable : E d → Submodule ℝ (E d)
  unstable : E d → Submodule ℝ (E d)
  isCompl_stable_unstable : ∀ x ∈ K, IsCompl (stable x) (unstable x)
  stable_invariant : ∀ x ∈ K,
    (stable x).map (fderiv ℝ (T : E d → E d) x : E d →ₗ[ℝ] E d) = stable (T x)
  unstable_invariant : ∀ x ∈ K,
    (unstable x).map (fderiv ℝ (T : E d → E d) x : E d →ₗ[ℝ] E d) = unstable (T x)
  rate : ℝ
  rate_pos : 0 < rate
  rate_lt_one : rate < 1
  const : ℝ
  const_pos : 0 < const
  contract_stable : ∀ x ∈ K, ∀ v : E d, v ∈ stable x → ∀ n : ℕ,
    ‖fderiv ℝ ((T : E d → E d)^[n]) x v‖ ≤ const * rate ^ n * ‖v‖
  contract_unstable : ∀ x ∈ K, ∀ v : E d, v ∈ unstable x → ∀ n : ℕ,
    ‖fderiv ℝ ((T.symm : E d → E d)^[n]) x v‖ ≤ const * rate ^ n * ‖v‖

Uses 1 · Used by 1

Statement usesEuclidean model space for the shadowing lemma

Used byHyperbolic invariant set

DefinitionHyperbolic invariant set#✓fully proved

Let \(T : \mathbb{R}^d \to \mathbb{R}^d\) be a homeomorphism. A set \(K \subseteq \mathbb{R}^d\) is a hyperbolic invariant set for \(T\) if there exists a hyperbolic structure for \(T\) on \(K\).

def IsHyperbolic (T : E d ≃ₜ E d) (K : Set (E d)) : Prop :=
  Nonempty (HyperbolicStructure T K)

Uses 2 · Used by 1

Statement usesEuclidean model space for the shadowing lemma · Hyperbolic structure

Used byAnosov–Bowen shadowing lemma

DefinitionPseudo-orbit#✓fully proved

Let \(d\) be a natural number, let \(\mathbb{R}^d\) carry the Euclidean norm, let \(T : \mathbb{R}^d \to \mathbb{R}^d\) be a map and let \(\varepsilon\) be a real number. A sequence \((x_n)_{n \in \mathbb{N}}\) in \(\mathbb{R}^d\) is an \(\varepsilon\)-pseudo orbit of \(T\) if \(\|x_{n+1} - T(x_n)\| < \varepsilon\) for every \(n \in \mathbb{N}\).

def IsPseudoOrbit (T : E d → E d) (ε : ℝ) (x : ℕ → E d) : Prop :=
  ∀ n : ℕ, ‖x (n + 1) - T (x n)‖ < ε

Uses 1 · Used by 1

Statement usesEuclidean model space for the shadowing lemma

Used byShadowing property

DefinitionShadowing property#✓fully proved

Let \(T : \mathbb{R}^d \to \mathbb{R}^d\) be a map, write \(T^n\) for its \(n\)-fold iterate, and let \(K \subseteq \mathbb{R}^d\). The set \(K\) has the shadowing property for \(T\) if there is an open set \(U \subseteq \mathbb{R}^d\) containing \(K\) such that for every \(\delta > 0\) there is \(\varepsilon > 0\) with the following property: for every \(\varepsilon\)-pseudo orbit \((x_n)_{n \in \mathbb{N}}\) of \(T\) with \(x_n \in U\) for all \(n\), there is a point \(y \in \mathbb{R}^d\) with \(\|x_n - T^n(y)\| < \delta\) for all \(n \in \mathbb{N}\).

def HasShadowing (T : E d → E d) (K : Set (E d)) : Prop :=
  ∃ U : Set (E d), IsOpen U ∧ K ⊆ U ∧
    ∀ δ > 0, ∃ ε > 0, ∀ x : ℕ → E d,
      (∀ n, x n ∈ U) → IsPseudoOrbit T ε x →
      ∃ y : E d, ∀ n : ℕ, ‖x n - T^[n] y‖ < δ

Uses 2 · Used by 1

Statement usesEuclidean model space for the shadowing lemma · Pseudo-orbit

Used byAnosov–Bowen shadowing lemma

TheoremAnosov–Bowen shadowing lemma#●ready to prove

Let \(T : \mathbb{R}^d \to \mathbb{R}^d\) be a homeomorphism and let \(K \subseteq \mathbb{R}^d\) be a compact set that is a hyperbolic invariant set for \(T\). Then \(K\) has the shadowing property for \(T\).

public theorem_wanted hyperbolic_has_shadowing
    (T : E d ≃ₜ E d) (K : Set (E d))
    (_hKc : IsCompact K) (_hK : IsHyperbolic T K) :
    HasShadowing (T : E d → E d) K

Sources

• D.V. Anosov, 'Geodesic flows on closed Riemannian manifolds with negative curvature', Trudy Mat. Inst. Steklov. 90 (1967); R. Bowen, 'ω-limit sets for Axiom A diffeomorphisms', J. Differential Equations 18 (1975) 333–339. Listed as §67 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem anosov_bowen_shadowing of the lean-eval benchmark.

Uses 3

Statement usesEuclidean model space for the shadowing lemma · Shadowing property · Hyperbolic invariant set

5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.