Gluing plugs (Béguin–Bonatti–Yu, Prop. 1.1): Λ_X, Λ_Y and the connecting orbits lie in the maximal invariant set of the glued field
ProvedAnosovPlugs.plugGluing_maxInvSet_supersetLet and be vector fields on the compact 3-manifolds with boundary and , let , and let . Write for the set of boundary points of at which points strictly outward and for the set of boundary points of at which points strictly inward. Let be a gluing of and along : C¹ embeddings and with injective derivatives cover the compact 3-manifold , identify exactly the points with , and satisfy , . Write , , for the maximal invariant sets (points whose orbit is defined for all times), for the exit lamination of (points of whose backward orbit is defined for all times) and for the entrance lamination of (points of whose forward orbit is defined for all times). The connecting set is the -orbit of : the set of points that lie on a complete integral curve of with for some with . Then the three pieces lie in the maximal invariant set of :
This is the inclusion in the sentence " is the union of , and the -orbit of " of the proof of Proposition 1.1.
Formalization Note No plug or hyperbolicity hypothesis is needed for this inclusion: only the gluing identities. is not assumed to be C¹. The connecting set is phrased by the existence of a complete integral curve of through the gluing point (see the companion statement plugGluing_maxInvSet_subset).
import Mathlib import Definitions.Def_AnosovPlugs_Gluing open scoped Manifold ContDiff Topology open Set
namespace AnosovPlugs
theorem plugGluing_maxInvSet_superset
{U : Type} [TopologicalSpace U] [ChartedSpace (EuclideanHalfSpace 3) U]
[IsManifold I3 ∞ U] [T2Space U] [CompactSpace U]
{V : Type} [TopologicalSpace V] [ChartedSpace (EuclideanHalfSpace 3) V]
[IsManifold I3 ∞ V] [T2Space V] [CompactSpace V]
{W : Type} [TopologicalSpace W] [ChartedSpace (EuclideanHalfSpace 3) W]
[IsManifold I3 ∞ W] [T2Space W] [CompactSpace W]
(X : (x : U) → TangentSpace I3 x) (Y : (y : V) → TangentSpace I3 y)
(Tout : Set U) (φ : U → V)
(Z : (w : W) → TangentSpace I3 w) (iU : U → W) (iV : V → W)
(hglue : IsPlugGluing X Y Tout φ Z iU iV) :
iU '' maxInvSet X ∪ iV '' maxInvSet Y ∪
{w | ∃ x ∈ exitLamination X ∩ Tout, φ x ∈ entranceLamination Y ∧
∃ γ : ℝ → W, γ 0 = iU x ∧ IsMIntegralCurve γ Z ∧ w ∈ range γ} ⊆ maxInvSet Z := by sorry
end AnosovPlugs