Small fibre discs near the zero section

An open neighbourhood of the zero section in a continuous real Riemannian vector bundle contains discs of a fixed positive radius over a neighbourhood of each base point. The radius is measured in the fibre metric, rather than in a chosen trivialization. This local uniformity permits continuous or smooth selection of a radius on the whole base, even when the bundle is nontrivial and the base is noncompact. Over a compact subset of the base, a single positive radius works at every point.

The proof uses Sébastien Gouëzel's eventually_norm_trivializationAt_lt to compare the fibre norm with coordinates in a bundle chart. No finite-dimensionality is required.

Reference: J. M. Lee, Introduction to Smooth Manifolds, second edition, Theorem 6.24, the shrinking step in the tubular neighbourhood theorem.

Main results

• IsOpen.exists_pos_forall_norm_le_subset_bundle: fibre discs of one positive radius over a neighbourhood of a base point.
• IsCompact.exists_pos_forall_norm_le_subset_bundle: fibre discs of one positive radius over a compact subset of the base.

theorem IsOpen.exists_pos_forall_norm_le_subset_bundle {B : Type u_1} {F : Type u_2} [TopologicalSpace B] [NormedAddCommGroup F] [NormedSpace ℝ F] {V : B → Type u_3} [(b : B) → NormedAddCommGroup (V b)] [(b : B) → InnerProductSpace ℝ (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [IsContinuousRiemannianBundle F V] {U : Set (Bundle.TotalSpace F V)} (hU : IsOpen U) {b : B} (hzero : Bundle.zeroSection F V b ∈ U) : ∃ r > 0, ∀ᶠ (y : B) in nhds b, ∀ (v : V y), ‖v‖ ≤ r → { proj := y, snd := v } ∈ U

Near each point of the base, a neighbourhood of the zero section contains all fibre vectors of sufficiently small norm, with one positive bound valid throughout that neighbourhood. No compactness or finite-dimensionality is required.

theorem IsCompact.exists_pos_forall_norm_le_subset_bundle {B : Type u_1} {F : Type u_2} [TopologicalSpace B] [NormedAddCommGroup F] [NormedSpace ℝ F] {V : B → Type u_3} [(b : B) → NormedAddCommGroup (V b)] [(b : B) → InnerProductSpace ℝ (V b)] [TopologicalSpace (Bundle.TotalSpace F V)] [FiberBundle F V] [VectorBundle ℝ F V] [IsContinuousRiemannianBundle F V] {K : Set B} (hK : IsCompact K) {U : Set (Bundle.TotalSpace F V)} (hU : IsOpen U) (hzero : ∀ b ∈ K, Bundle.zeroSection F V b ∈ U) : ∃ r > 0, ∀ b ∈ K, ∀ (v : V b), ‖v‖ ≤ r → { proj := b, snd := v } ∈ U

Over a compact set K of the base, an open neighbourhood of the zero section contains all fibre vectors of norm at most r, for one positive r valid at every point of K.