Smooth disc neighbourhoods in Riemannian vector bundles

Every open neighbourhood of the zero section contains a closed disc bundle of positive smooth radius, with the radius smaller than any prescribed positive continuous bound. Only a continuous fibre metric is needed for this selection. If the metric is smooth, radial compression then identifies the entire total space diffeomorphically with a smaller open neighbourhood of the zero section, preserving base points and fixing zero vectors.

This permits tubular coordinates initially defined only near the zero section to be parametrized by the whole normal bundle, including over noncompact submanifolds. The radius selection uses Mathlib's exists_contMDiffMap_forall_mem_convex_of_local_const; compression uses TauCeti.vectorBundleRadialPartialDiffeomorphOfRadius.

References

• J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 6.24.
• M. W. Hirsch, Differential Topology, Chapter 4, Theorem 6.3.

theorem IsOpen.exists_contMDiffMap_norm_le_subset_bundle {B : Type u_1} {F : Type u_2} {E : Type u_3} {H : Type u_4} [TopologicalSpace B] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [ChartedSpace H B] [IsManifold I (↑⊤) B] [T2Space B] [SigmaCompactSpace B] [NormedAddCommGroup F] [NormedSpace ℝ F] {V : B → Type u_5} [(b : B) → NormedAddCommGroup (V b)] [(b : B) → InnerProductSpace ℝ (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] {n : ℕ∞} [IsContinuousRiemannianBundle F V] {U : Set (Bundle.TotalSpace F V)} (hU : IsOpen U) (hzero : ∀ (b : B), Bundle.zeroSection F V b ∈ U) {ε : B → ℝ} (hε : Continuous ε) (hεpos : ∀ (b : B), 0 < ε b) : ∃ (r : ContMDiffMap I (modelWithCornersSelf ℝ ℝ) B ℝ ↑n), (∀ (b : B), 0 < r b) ∧ (∀ (b : B), r b < ε b) ∧ ∀ (b : B) (v : V b), ‖v‖ ≤ r b → ⟨b, v⟩ ∈ U

An open neighbourhood of the zero section contains closed fibre discs of a positive C^n radius smaller than any prescribed positive continuous bound. The fibre metric need only be continuous, and the fibres need not be finite-dimensional.

theorem TauCeti.exists_diffeomorph_subset_zeroSection {B : Type u_1} {F : Type u_2} {E : Type u_3} {H : Type u_4} [TopologicalSpace B] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [ChartedSpace H B] [IsManifold I (↑⊤) B] [T2Space B] [SigmaCompactSpace B] [NormedAddCommGroup F] [NormedSpace ℝ F] {V : B → Type u_5} [(b : B) → NormedAddCommGroup (V b)] [(b : B) → InnerProductSpace ℝ (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] {n : ℕ∞} [IsContMDiffRiemannianBundle I (↑n) F V] {U : Set (Bundle.TotalSpace F V)} (hU : IsOpen U) (hzero : ∀ (b : B), Bundle.zeroSection F V b ∈ U) : ∃ (W : TopologicalSpace.Opens (Bundle.TotalSpace F V)), ↑W ⊆ U ∧ ∃ (Φ : Diffeomorph (I.prod (modelWithCornersSelf ℝ F)) (I.prod (modelWithCornersSelf ℝ F)) (Bundle.TotalSpace F V) ↥W ↑n), (∀ (p : Bundle.TotalSpace F V), (↑(Φ p)).proj = p.proj) ∧ ∀ (b : B), ↑(Φ (Bundle.zeroSection F V b)) = Bundle.zeroSection F V b

The whole total space of a smooth Riemannian vector bundle is diffeomorphic, over the base and fixing the zero section, to an open neighbourhood inside any prescribed open neighbourhood of the zero section. No compactness of the base or finite rank is required.