Compactness of norm-bounded parts of a Riemannian vector bundle

In a vector bundle whose fibers carry inner products depending continuously on the base point, the fiber norm is a continuous function on the total space. When the model fiber is finite-dimensional, this file proves that the vectors of norm at most r lying over a compact subset of the base form a compact subset of the total space.

This is the properness statement that turns a bound on the speed of a curve in the base together with relative compactness of its image into relative compactness of its velocity lift. The part of the bundle lying over a compact set need not be compact on its own: the fibers of a bundle with a positive-dimensional model fiber are noncompact, so the norm bound is what makes the statement true, and the proof is local: over a compact set inside the base set of one trivialization, the fiber norm and the model norm are comparable by eventually_norm_trivializationAt_lt, and the general case follows by a finite cover.

Main results

• Continuous.norm_bundle: the fiber norm of a continuous map into the fibers of a continuous Riemannian bundle is continuous, with TauCeti.continuous_norm_bundle its tautological case.
• IsCompact.norm_le_bundle: the vectors of norm at most r over a compact set form a compact subset of the total space.

theorem Continuous.norm_bundle {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] [IsContinuousRiemannianBundle F E] {X : Type u_4} [TopologicalSpace X] {b : X → B} {v : (x : X) → E (b x)} (hv : Continuous fun (x : X) => { proj := b x, snd := v x }) : Continuous fun (x : X) => ‖v x‖

Given a continuous map into the fibers of a continuous Riemannian bundle, its fiber norm is a continuous function.

theorem TauCeti.continuous_norm_bundle {B : Type u_1} [TopologicalSpace B] (F : Type u_2) [NormedAddCommGroup F] [NormedSpace ℝ F] (E : B → Type u_3) [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] [IsContinuousRiemannianBundle F E] : Continuous fun (z : Bundle.TotalSpace F E) => ‖z.snd‖

In a continuous Riemannian bundle, the fiber norm is a continuous function on the total space.

theorem IsCompact.norm_le_bundle {B : Type u_1} [TopologicalSpace B] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_3} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] [IsContinuousRiemannianBundle F E] [FiniteDimensional ℝ F] [T2Space B] {K : Set B} (hK : IsCompact K) (r : ℝ) : IsCompact {z : Bundle.TotalSpace F E | z.proj ∈ K ∧ ‖z.snd‖ ≤ r}

The norm-bounded part of a Riemannian bundle over a compact set is compact. In a continuous Riemannian vector bundle with finite-dimensional model fiber, the vectors of norm at most r lying over a compact subset of the base form a compact subset of the total space.