Shrinking tubular neighbourhoods inside the normal bundle

A Euclidean tubular neighbourhood can be chosen so that its closed normal discs lie in any prescribed open neighbourhood of the zero section in the normal bundle. At the same time, the ambient closed balls fit inside a prescribed neighbourhood of the embedded image. The radius is positive and smooth, and normal addition remains an open embedding.

This is the shrinking step for assembling smooth tubular inverses: choose a zero-section neighbourhood on which normal addition is a local diffeomorphism, then shrink the globally injective tube into it. The normal bundle retains its topology induced from M × V.

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

theorem TauCeti.exists_isOpenEmbedding_normalTubeOfRadius_contMDiff_subset_zeroSection {V : Type u_1} {E : Type u_2} {F : Type u_3} {H : Type u_4} {M : Type u_5} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [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) {U : Set (Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x))} (hU : IsOpen U) (hzero : ∀ (x : M), Bundle.zeroSection F (fun (x : M) => ↥(normalSubspace I f x)) x ∈ U) {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) ∧ ∀ (p : Bundle.TotalSpace F fun (x : M) => ↥(normalSubspace I f x)), ‖↑p.snd‖ ≤ r p.proj → p ∈ U

A C² Euclidean embedding of a smooth manifold admits a positive smooth tubular radius whose closed normal discs lie in any prescribed open neighbourhood of the zero section. Even the ambient closed balls map into the prescribed neighbourhood of the embedded image.