Basic Riemannian bundle constructions

This file provides conversions between Mathlib's Riemannian bundle classes and bundled Riemannian metrics, and records that the Riemannian norm of the differential of a C¹ map, applied to a fixed vector, depends continuously on the base point.

Main definitions

• Bundle.ContMDiffRiemannianMetric.ofIsContMDiffRiemannianBundle: package the metric of a C^n Riemannian bundle.
• Bundle.ContMDiffRiemannianMetric.InducesRiemannianDistance: express that a smooth metric induces the ambient Riemannian distance.
• Bundle.ContMDiffRiemannianMetric.ofIsContMDiffRiemannianBundle_inner: the packaged metric is the bundle's inner product.
• Bundle.IsContinuousRiemannianBundle.toIsContMDiffZero: view a continuous Riemannian bundle as a C^0 Riemannian bundle.
• IsContMDiffRiemannianBundle.toIsContinuousRiemannianBundle: conversely, view a C^n Riemannian bundle as a continuous Riemannian bundle.
• ContMDiffOn.continuousOn_norm_mfderiv: for a C¹ map f from an open subset of a normed space to a Riemannian manifold, z ↦ ‖df_z ξ‖ is continuous.
• ContMDiffOn.contDiffOn_inner_mfderiv: for a C^(m+1) map f from an open subset of a normed space to a C^m Riemannian manifold, z ↦ ⟪df_z ξ, df_z η⟫ is C^m.

noncomputable def Bundle.ContMDiffRiemannianMetric.ofIsContMDiffRiemannianBundle {EB : Type u_1} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : B → Type u_5} [TopologicalSpace (TotalSpace F V)] [(b : B) → TopologicalSpace (V b)] [(b : B) → AddCommGroup (V b)] [(b : B) → Module ℝ (V b)] [∀ (b : B), IsTopologicalAddGroup (V b)] [∀ (b : B), ContinuousConstSMul ℝ (V b)] [FiberBundle F V] [VectorBundle ℝ F V] [RiemannianBundle V] [IsContMDiffRiemannianBundle IB n F V] : ContMDiffRiemannianMetric IB n F V

Package the metric of a C^n Riemannian bundle as a C^n Riemannian metric.

Equations

• Bundle.ContMDiffRiemannianMetric.ofIsContMDiffRiemannianBundle = { inner := Bundle.RiemannianBundle.g.inner, symm := ⋯, pos := ⋯, isVonNBounded := ⋯, contMDiff := ⋯ }

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.ofIsContMDiffRiemannianBundle_inner {EB : Type u_1} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : B → Type u_5} [TopologicalSpace (TotalSpace F V)] [(b : B) → TopologicalSpace (V b)] [(b : B) → AddCommGroup (V b)] [(b : B) → Module ℝ (V b)] [∀ (b : B), IsTopologicalAddGroup (V b)] [∀ (b : B), ContinuousConstSMul ℝ (V b)] [FiberBundle F V] [VectorBundle ℝ F V] [RiemannianBundle V] [IsContMDiffRiemannianBundle IB n F V] (x : B) (v w : V x) : ((ofIsContMDiffRiemannianBundle.inner x) v) w = ((RiemannianBundle.g.inner x) v) w

The Riemannian metric packaged from a C^n Riemannian bundle is its inner product.

theorem Bundle.IsContinuousRiemannianBundle.toIsContMDiffZero {EB : Type u_1} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {B : Type u_3} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : B → Type u_5} [TopologicalSpace (TotalSpace F V)] [(b : B) → NormedAddCommGroup (V b)] [(b : B) → InnerProductSpace ℝ (V b)] [FiberBundle F V] [VectorBundle ℝ F V] [IsContinuousRiemannianBundle F V] : IsContMDiffRiemannianBundle IB 0 F V

A continuous Riemannian bundle is a C^0 Riemannian bundle. This is deliberately a theorem, not an instance, because Mathlib avoids the corresponding inference path.

theorem IsContMDiffRiemannianBundle.toIsContinuousRiemannianBundle {EB : Type u_1} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {V : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F V)] [(b : B) → NormedAddCommGroup (V b)] [(b : B) → InnerProductSpace ℝ (V b)] [FiberBundle F V] [VectorBundle ℝ F V] [IsContMDiffRiemannianBundle IB n F V] : IsContinuousRiemannianBundle F V

A C^n Riemannian bundle is a continuous Riemannian bundle. Like Bundle.IsContinuousRiemannianBundle.toIsContMDiffZero, this is a theorem rather than an instance: the model IB and the smoothness n do not appear in its conclusion.

def Bundle.ContMDiffRiemannianMetric.InducesRiemannianDistance {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [MetricSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) : Prop

The metric g induces the Riemannian distance on M through the ambient metric space.

Equations

• g.InducesRiemannianDistance = IsRiemannianManifold I M

theorem Bundle.ContMDiffRiemannianMetric.InducesRiemannianDistance.toIsRiemannianManifold {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [MetricSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (g : ContMDiffRiemannianMetric I (↑⊤) E fun (x : M) => TangentSpace I x) (h : g.InducesRiemannianDistance) : IsRiemannianManifold I M

The metric's induced-distance condition yields the corresponding Riemannian-manifold structure after installing its metric bundle.

theorem ContMDiffOn.continuousOn_norm_mfderiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : F → M} {U : Set F} {n : WithTop ℕ∞} (hf : ContMDiffOn (modelWithCornersSelf ℝ F) I n f U) (hn : 1 ≤ n) (hU : IsOpen U) (ξ : F) : ContinuousOn (fun (z : F) => ‖(mfderiv% f z) ξ‖) U

Let f be a C^n map, 1 ≤ n, from an open subset U of a real normed space to a manifold whose tangent spaces carry a continuous Riemannian metric. For each fixed vector ξ, the Riemannian norm of df_z ξ depends continuously on z ∈ U.

theorem ContMDiffOn.contDiffOn_inner_mfderiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : F → M} {U : Set F} {m n : WithTop ℕ∞} [IsContMDiffRiemannianBundle I m E fun (x : M) => TangentSpace I x] (hf : ContMDiffOn (modelWithCornersSelf ℝ F) I n f U) (hmn : m + 1 ≤ n) (hU : IsOpen U) (ξ η : F) : ContDiffOn ℝ m (fun (z : F) => inner ℝ ((mfderiv% f z) ξ) ((mfderiv% f z) η)) U

Let f be a C^n map from an open subset U of a real normed space to a manifold whose tangent spaces carry a C^m Riemannian metric, with m + 1 ≤ n. For fixed vectors ξ and η, the Riemannian inner product ⟪df_z ξ, df_z η⟫ is a C^m function of z ∈ U.