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. The compactness statement holds more generally for fiber norms that are continuous on the total space and for which each trivialization is locally bounded, as for the operator norm on covectors.

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. The proof is local: near each point of the base, the fiber norm bounds the model norm of the coordinates in the trivialization at that point (in the Riemannian case by eventually_norm_trivializationAt_lt), so the coordinates of a convergent ultrafilter of bounded vectors converge too.

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.
• IsCompact.norm_le_bundle_of_continuous: the same for a continuous fiber norm with locally bounded trivializations.
• Bundle.RiemannianMetric.isSymm_toBilinForm_inner: the inner product of a Riemannian metric on a fiber is a symmetric bilinear form.

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_of_continuous {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)] [FiniteDimensional ℝ F] [(x : B) → NormedSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] (hnorm : Continuous fun (z : Bundle.TotalSpace F E) => ‖z.snd‖) (hloc : ∀ (x : B), ∃ (C : ℝ), ∀ᶠ (y : B) in nhds x, ∀ (w : E y), ‖(Bundle.Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y) w‖ ≤ C * ‖w‖) {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 normed vector bundle over a compact set is compact. Let the fibers of a vector bundle with finite-dimensional model fiber carry norms, such that the fiber norm is continuous on the total space and each trivialization is bounded in norm near its base point. Then the vectors of norm at most r lying over a compact subset of the base form a compact subset of 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)] [FiniteDimensional ℝ F] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] [IsContinuousRiemannianBundle F E] {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.

theorem Bundle.RiemannianMetric.isSymm_toBilinForm_inner {B : Type u_4} {E : B → Type u_5} [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)] (g : RiemannianMetric E) (b : B) : (g.inner b).toBilinForm.IsSymm

The inner product of a Riemannian metric on a fiber is a symmetric bilinear form.