Smooth tubular radii

The Euclidean tubular neighbourhood of a C² embedding of a smooth boundaryless manifold can be chosen with a positive smooth radius. Its entire closed normal disc bundle can be made to map into any prescribed open neighbourhood of the embedded image. The open normal tube retains the normal addition map as an open embedding.

This supplies smooth radii for fibrewise radial reparametrization. It asserts an open embedding, rather than smoothness of the inverse addition map, which requires a separate local normal-coordinate argument.

Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 6.24.

theorem TauCeti.exists_isOpenEmbedding_normalTubeOfRadius_contMDiff_subset {V : Type u_1} {E : Type u_2} {H : Type u_3} {M : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ V] [FiniteDimensional ℝ E] [I.Boundaryless] [IsManifold I (↑⊤) M] [SigmaCompactSpace M] {f : M → V} (hf : ContMDiff I (modelWithCornersSelf ℝ V) 2 f) (himm : ∀ (x : M), Function.Injective ⇑(mfderiv% f x)) (hind : Topology.IsInducing f) {O : Set V} (hO : IsOpen O) (hfO : Set.range f ⊆ O) : ∃ (r : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤), (∀ (x : M), 0 < r x) ∧ Topology.IsOpenEmbedding ((normalTubeOfRadius I f ⇑r).domRestrict fun (p : M × V) => f p.1 + p.2) ∧ ∀ (x : M) (v : V), ‖v‖ ≤ r x → f x + v ∈ O

A C² Euclidean embedding of a smooth manifold admits a positive smooth tubular radius. Even the ambient closed balls of this radius stay inside the prescribed neighbourhood.