Anosov plugs II: hyperbolic sets and Anosov vector fields

Definition

AnosovPlugs_Hyperbolic

by Lucas · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

3-manifoldsanosov-flowsdynamical-systemshyperbolic-dynamics

Let $X$ be a vector field on a 3-manifold $M$ and $\Lambda\subset M$ .

Hyperbolic set. $\Lambda$ is a hyperbolic set of $X$ (with one-dimensional strong stable and strong unstable bundles) if there are a continuous Riemannian metric $g$ on $M$ , lines $E^s(x),E^u(x)\subset T_xM$ for $x\in\Lambda$ , and constants $C>0,\lambda>0$ such that for every $x\in\Lambda$ :

$T_xM = E^s(x)+\mathbb R X(x)+E^u(x)$ with $\dim E^s(x)=\dim E^u(x)=1$ (so the sum is direct and $X(x)\neq0$ );
$DX^t_x(E^s(x))=E^s(X^t x)$ and $DX^t_x(E^u(x))=E^u(X^t x)$ for all $t\in\mathbb R$ ;
for all $t\ge0$ ,

\|DX^t_x v\|\le C e^{-\lambda t}\|v\| \ (v\in E^s(x)),\qquad \|DX^{-t}_x v\|\le C e^{-\lambda t}\|v\| \ (v\in E^u(x)).

Anosov vector field. $X$ is Anosov if it is C¹ and the whole manifold $M$ is a hyperbolic set.

This is the hyperbolicity notion of Definition 3.2 (applied to the maximal invariant set of plugs) and of §1.1 (for Anosov flows on closed manifolds).

Formalization Note The paper also asks the splitting to depend continuously on $x$ ; this is omitted since it follows from the uniform estimates. The paper's "time-one map contracts/expands for some metric" is replaced by the equivalent estimate with constants $C,\lambda$ for an arbitrary continuous metric.

Definition code

import Mathlib
import Definitions.Def_AnosovPlugs_Flows

/-!
Béguin–Bonatti–Yu, *Building Anosov flows on 3-manifolds*, Geom. Topol. 21 (2017).
Hyperbolic invariant sets of flows on 3-manifolds (with 1-dimensional strong stable and strong
unstable bundles), and Anosov vector fields (§1.1, Definition 3.2).
-/

open scoped Manifold ContDiff Topology
open Set

namespace AnosovPlugs

variable {M : Type} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace 3) M]
  [IsManifold I3 ∞ M]

/-- A continuous Riemannian metric on the 3-manifold `M` (a continuously varying inner product
on the tangent spaces). -/
abbrev RiemannianMetric3 (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace 3) M]
    [IsManifold I3 ∞ M] :=
  Bundle.ContinuousRiemannianMetric (EuclideanSpace ℝ (Fin 3)) (TangentSpace I3 : M → Type)

/-- The norm of a tangent vector `v ∈ T_x M` for the Riemannian metric `g`. -/
noncomputable def RiemannianMetric3.norm (g : RiemannianMetric3 M) (x : M)
    (v : TangentSpace I3 x) : ℝ :=
  Real.sqrt (g.inner x v v)

/-- `Λ` is a hyperbolic set of the vector field `X`, with one-dimensional strong stable and
strong unstable bundles: there are a continuous Riemannian metric `g`, line fields
`E^s, E^u` over `Λ` and constants `C > 0`, `λ > 0` such that for every `x ∈ Λ`:
* `T_x M = E^s(x) + ℝ·X(x) + E^u(x)` with `dim E^s(x) = dim E^u(x) = 1` (so the sum is direct
  and `X(x) ≠ 0`);
* `E^s` and `E^u` are invariant under the derivative of the time-`t` map of the flow, for all
  real `t`;
* `‖D X^t (v)‖ ≤ C e^{-λ t} ‖v‖` for `v ∈ E^s(x)`, `t ≥ 0`, and
  `‖D X^{-t} (v)‖ ≤ C e^{-λ t} ‖v‖` for `v ∈ E^u(x)`, `t ≥ 0`.
(Continuity of the splitting is not required: it is a consequence of these estimates.) -/
def IsHyperbolicSet (X : (x : M) → TangentSpace I3 x) (Λ : Set M) : Prop :=
  ∃ (g : RiemannianMetric3 M) (Es Eu : (x : M) → Submodule ℝ (TangentSpace I3 x)) (C lam : ℝ),
    0 < C ∧ 0 < lam ∧ ∀ x ∈ Λ,
      Module.finrank ℝ (Es x) = 1 ∧ Module.finrank ℝ (Eu x) = 1 ∧
      Es x ⊔ Submodule.span ℝ {X x} ⊔ Eu x = ⊤ ∧
      (∀ t : ℝ, (Es x).map (mfderiv I3 I3 (flowMap X t) x).toLinearMap = Es (flowMap X t x)) ∧
      (∀ t : ℝ, (Eu x).map (mfderiv I3 I3 (flowMap X t) x).toLinearMap = Eu (flowMap X t x)) ∧
      (∀ t : ℝ, 0 ≤ t → ∀ v ∈ Es x,
        g.norm (flowMap X t x) (mfderiv I3 I3 (flowMap X t) x v)
          ≤ C * Real.exp (-lam * t) * g.norm x v) ∧
      (∀ t : ℝ, 0 ≤ t → ∀ v ∈ Eu x,
        g.norm (flowMap X (-t) x) (mfderiv I3 I3 (flowMap X (-t)) x v)
          ≤ C * Real.exp (-lam * t) * g.norm x v)

/-- `X` is an Anosov vector field on `M`: a C¹ vector field for which the whole manifold is a
hyperbolic set (intended for closed `M`, where the flow is complete). -/
def IsAnosov (X : (x : M) → TangentSpace I3 x) : Prop :=
  IsC1VectorField X ∧ IsHyperbolicSet X univ

end AnosovPlugs

Source

F. Béguin, C. Bonatti, B. Yu, *Building Anosov flows on 3-manifolds*, Geom. Topol. 21 (2017) 1837–1930, https://doi.org/10.2140/gt.2017.21.1837, §1.1 (definition of Anosov vector fields) and Definition 3.2, p. 1850

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source paper and of the intended meaning. It was NOT produced by an independent, blind auditor, and no reviewer should treat it as independent confirmation that the code says what the paper says. Compare it against the Lean code yourself.

$M$ is a charted space over the half-space $\{x_0\ge0\}\subset\mathbb R^3$ with a $C^\infty$ manifold structure (no compactness or boundary assumption in this file).

RiemannianMetric3 $M$ is Mathlib's type of continuous Riemannian metrics on the tangent bundle of $M$ : for each $x$ a symmetric, positive-definite continuous bilinear form $g_x$ on $T_xM$ (defining the usual topology), depending continuously on $x$ . The associated norm is $\|v\|_x=\sqrt{g_x(v,v)}$ .
IsHyperbolicSet $X\,\Lambda$ holds iff there exist such a metric $g$ , a family of subspaces $E^s(x),E^u(x)\subseteq T_xM$ indexed by all $x\in M$ , and reals $C>0$ , $\lambda>0$ , such that for every $x\in\Lambda$ :
1. $\dim E^s(x)=\dim E^u(x)=1$ and $E^s(x)+\operatorname{span}\{X(x)\}+E^u(x)=T_xM$ ;
2. for every real $t$ , the image of $E^s(x)$ (resp. $E^u(x)$ ) under the manifold derivative at $x$ of the map $\varphi_t=\mathrm{flowMap}\,X\,t$ equals $E^s(\varphi_t x)$ (resp. $E^u(\varphi_t x)$ );
3. for every $t\ge0$ and $v\in E^s(x)$ : $\|D\varphi_t(x)v\|_{\varphi_t x}\le C e^{-\lambda t}\|v\|_x$ ;
4. for every $t\ge0$ and $v\in E^u(x)$ : $\|D\varphi_{-t}(x)v\|_{\varphi_{-t}x}\le C e^{-\lambda t}\|v\|_x$ .
Here $D\varphi_t(x)$ is Mathlib's mfderiv, which is $0$ if $\varphi_t$ is not differentiable at $x$ ; flowMap returns $x$ itself at times where the orbit is undefined. No continuity of $E^s,E^u$ in $x$ , no invariance of $\Lambda$ and no nonemptiness of $\Lambda$ is required; for $\Lambda=\emptyset$ the condition reduces to the existence of a continuous Riemannian metric.
IsAnosov $X$ : $X$ is a $C^1$ vector field and IsHyperbolicSet $X$ holds for $\Lambda=M$ . Nothing in this definition requires $M$ to be compact or boundaryless; those assumptions are supplied separately in the theorems.

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph