Riemannian vector bundles

Given a vector bundle over a manifold whose fibers are all endowed with a scalar product, we say that this bundle is Riemannian if the scalar product depends smoothly on the base point.

We introduce a typeclass [IsContMDiffRiemannianBundle IB n F E] registering this property. Under this assumption, we show that the scalar product of two smooth maps into the same fibers of the bundle is a smooth function.

If the fibers of a bundle E have a preexisting topology (like the tangent bundle), one cannot assume additionally [∀ b, InnerProductSpace ℝ (E b)] as this would create diamonds. Instead, use [RiemannianBundle E], which endows the fibers with a scalar product while ensuring that there is no diamond (for this, the Bundle scope should be open). We provide a constructor for [RiemannianBundle E] from a smooth family of metrics, which registers automatically [IsContMDiffRiemannianBundle IB n F E].

The following code block is the standard way to say "Let E be a smooth vector bundle equipped with a C^n Riemannian structure over a C^n manifold B":

variable {EB : Type*} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type*} [TopologicalSpace B] [ChartedSpace HB B] {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type*} [TopologicalSpace (TotalSpace F E)] [∀ x, NormedAddCommGroup (E x)] [∀ x, InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] [IsManifold IB n B] [ContMDiffVectorBundle n F E IB] [IsContMDiffRiemannianBundle IB n F E] 

class IsContMDiffRiemannianBundle {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] (E : B → Type u_5) [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] : Prop

Consider a real vector bundle in which each fiber is endowed with a scalar product. We that the bundle is Riemannian if the scalar product depends smoothly on the base point. This assumption is spelled IsContMDiffRiemannianBundle IB n F E where IB is the model space of the base, n is the smoothness, F is the model fiber, and E : B → Type* is the bundle.

• exists_contMDiff : ∃ (g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ), (ContMDiff IB (IB.prod (modelWithCornersSelf ℝ (F →L[ℝ] F →L[ℝ] ℝ))) n fun (b : B) => Bundle.TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) b (g b)) ∧ ∀ (x : B) (v w : E x), inner ℝ v w = ((g x) v) w

theorem IsContMDiffRiemannianBundle.of_le {EB : Type u_1} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n n' : WithTop ℕ∞} {B : Type u_3} [TopologicalSpace B] [ChartedSpace HB B] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] [h : IsContMDiffRiemannianBundle IB n F E] (h' : n' ≤ n) : IsContMDiffRiemannianBundle IB n' F E

instance instIsContMDiffRiemannianBundleOfSomeENatTopOfLEInfty {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] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] {a : WithTop ℕ∞} [IsContMDiffRiemannianBundle IB (↑⊤) F E] [h : ENat.LEInfty a] : IsContMDiffRiemannianBundle IB a F E

instance instIsContMDiffRiemannianBundleOfTopWithTopENat {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] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] {a : WithTop ℕ∞} [IsContMDiffRiemannianBundle IB ⊤ F E] : IsContMDiffRiemannianBundle IB a F E

instance instIsContMDiffRiemannianBundleOfNatWithTopENat {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] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] [IsContMDiffRiemannianBundle IB 1 F E] : IsContMDiffRiemannianBundle IB 0 F E

instance instIsContMDiffRiemannianBundleOfNatWithTopENat_1 {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] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] [IsContMDiffRiemannianBundle IB 2 F E] : IsContMDiffRiemannianBundle IB 1 F E

instance instIsContMDiffRiemannianBundleOfNatWithTopENat_2 {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] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] [IsContMDiffRiemannianBundle IB 3 F E] : IsContMDiffRiemannianBundle IB 2 F E

instance instIsContMDiffRiemannianBundleTrivial {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_6} [NormedAddCommGroup F₁] [InnerProductSpace ℝ F₁] : IsContMDiffRiemannianBundle IB n F₁ (Bundle.Trivial B F₁)

A trivial vector bundle, in which the model fiber has a scalar product, is a Riemannian bundle.

theorem ContMDiffWithinAt.inner_bundle {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] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] {EM : Type u_6} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_7} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_8} [TopologicalSpace M] [ChartedSpace HM M] [h : IsContMDiffRiemannianBundle IB n F E] {b : M → B} {v w : (x : M) → E (b x)} {s : Set M} {x : M} (hv : ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun (m : M) => { proj := b m, snd := v m }) s x) (hw : ContMDiffWithinAt IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun (m : M) => { proj := b m, snd := w m }) s x) : ContMDiffWithinAt IM (modelWithCornersSelf ℝ ℝ) n (fun (m : M) => inner ℝ (v m) (w m)) s x

Given two smooth maps into the same fibers of a Riemannian bundle, their scalar product is smooth.

theorem ContMDiffAt.inner_bundle {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] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] {EM : Type u_6} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_7} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_8} [TopologicalSpace M] [ChartedSpace HM M] [h : IsContMDiffRiemannianBundle IB n F E] {b : M → B} {v w : (x : M) → E (b x)} {x : M} (hv : ContMDiffAt IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun (m : M) => { proj := b m, snd := v m }) x) (hw : ContMDiffAt IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun (m : M) => { proj := b m, snd := w m }) x) : ContMDiffAt IM (modelWithCornersSelf ℝ ℝ) n (fun (b_1 : M) => inner ℝ (v b_1) (w b_1)) x

Given two smooth maps into the same fibers of a Riemannian bundle, their scalar product is smooth.

theorem ContMDiffOn.inner_bundle {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] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] {EM : Type u_6} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_7} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_8} [TopologicalSpace M] [ChartedSpace HM M] [h : IsContMDiffRiemannianBundle IB n F E] {b : M → B} {v w : (x : M) → E (b x)} {s : Set M} (hv : ContMDiffOn IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun (m : M) => { proj := b m, snd := v m }) s) (hw : ContMDiffOn IM (IB.prod (modelWithCornersSelf ℝ F)) n (fun (m : M) => { proj := b m, snd := w m }) s) : ContMDiffOn IM (modelWithCornersSelf ℝ ℝ) n (fun (b_1 : M) => inner ℝ (v b_1) (w b_1)) s

Given two smooth maps into the same fibers of a Riemannian bundle, their scalar product is smooth.

theorem ContMDiff.inner_bundle {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] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] {EM : Type u_6} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_7} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_8} [TopologicalSpace M] [ChartedSpace HM M] [h : IsContMDiffRiemannianBundle IB n F E] {b : M → B} {v w : (x : M) → E (b x)} (hv : ContMDiff IM (IB.prod (modelWithCornersSelf ℝ F)) n fun (m : M) => { proj := b m, snd := v m }) (hw : ContMDiff IM (IB.prod (modelWithCornersSelf ℝ F)) n fun (m : M) => { proj := b m, snd := w m }) : ContMDiff IM (modelWithCornersSelf ℝ ℝ) n fun (b_1 : M) => inner ℝ (v b_1) (w b_1)

Given two smooth maps into the same fibers of a Riemannian bundle, their scalar product is smooth.

theorem MDifferentiableWithinAt.inner_bundle {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] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] {EM : Type u_6} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_7} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_8} [TopologicalSpace M] [ChartedSpace HM M] [h : IsContMDiffRiemannianBundle IB 1 F E] {b : M → B} {v w : (x : M) → E (b x)} {s : Set M} {x : M} (hv : MDifferentiableWithinAt IM (IB.prod (modelWithCornersSelf ℝ F)) (fun (m : M) => { proj := b m, snd := v m }) s x) (hw : MDifferentiableWithinAt IM (IB.prod (modelWithCornersSelf ℝ F)) (fun (m : M) => { proj := b m, snd := w m }) s x) : MDifferentiableWithinAt IM (modelWithCornersSelf ℝ ℝ) (fun (m : M) => inner ℝ (v m) (w m)) s x

Given two differentiable maps into the same fibers of a Riemannian bundle, their scalar product is differentiable.

theorem MDifferentiableAt.inner_bundle {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] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] {EM : Type u_6} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_7} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_8} [TopologicalSpace M] [ChartedSpace HM M] [h : IsContMDiffRiemannianBundle IB 1 F E] {b : M → B} {v w : (x : M) → E (b x)} {x : M} (hv : MDifferentiableAt IM (IB.prod (modelWithCornersSelf ℝ F)) (fun (m : M) => { proj := b m, snd := v m }) x) (hw : MDifferentiableAt IM (IB.prod (modelWithCornersSelf ℝ F)) (fun (m : M) => { proj := b m, snd := w m }) x) : MDifferentiableAt IM (modelWithCornersSelf ℝ ℝ) (fun (b_1 : M) => inner ℝ (v b_1) (w b_1)) x

Given two differentiable maps into the same fibers of a Riemannian bundle, their scalar product is differentiable.

theorem MDifferentiableOn.inner_bundle {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] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] {EM : Type u_6} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_7} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_8} [TopologicalSpace M] [ChartedSpace HM M] [h : IsContMDiffRiemannianBundle IB 1 F E] {b : M → B} {v w : (x : M) → E (b x)} {s : Set M} (hv : MDifferentiableOn IM (IB.prod (modelWithCornersSelf ℝ F)) (fun (m : M) => { proj := b m, snd := v m }) s) (hw : MDifferentiableOn IM (IB.prod (modelWithCornersSelf ℝ F)) (fun (m : M) => { proj := b m, snd := w m }) s) : MDifferentiableOn IM (modelWithCornersSelf ℝ ℝ) (fun (b_1 : M) => inner ℝ (v b_1) (w b_1)) s

Given two differentiable maps into the same fibers of a Riemannian bundle, their scalar product is differentiable.

theorem MDifferentiable.inner_bundle {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] {E : B → Type u_5} [TopologicalSpace (Bundle.TotalSpace F E)] [(x : B) → NormedAddCommGroup (E x)] [(x : B) → InnerProductSpace ℝ (E x)] [FiberBundle F E] [VectorBundle ℝ F E] {EM : Type u_6} [NormedAddCommGroup EM] [NormedSpace ℝ EM] {HM : Type u_7} [TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_8} [TopologicalSpace M] [ChartedSpace HM M] [h : IsContMDiffRiemannianBundle IB 1 F E] {b : M → B} {v w : (x : M) → E (b x)} (hv : MDifferentiable IM (IB.prod (modelWithCornersSelf ℝ F)) fun (m : M) => { proj := b m, snd := v m }) (hw : MDifferentiable IM (IB.prod (modelWithCornersSelf ℝ F)) fun (m : M) => { proj := b m, snd := w m }) : MDifferentiable IM (modelWithCornersSelf ℝ ℝ) fun (b_1 : M) => inner ℝ (v b_1) (w b_1)

Given two differentiable maps into the same fibers of a Riemannian bundle, their scalar product is differentiable.

structure Bundle.ContMDiffRiemannianMetric {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] (E : B → Type u_5) [TopologicalSpace (TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)] [FiberBundle F E] [VectorBundle ℝ F E] : Type (max u_3 u_5)

A family of inner product space structures on the fibers of a fiber bundle, defining the same topology as the already existing one, and varying continuously with the base point. See also ContinuousRiemannianMetric for a continuous version.

This structure is used through RiemannianBundle for typeclass inference, to register the inner product space structure on the fibers without creating diamonds.

• inner (b : B) : E b →L[ℝ] E b →L[ℝ] ℝ

  The scalar product along the fibers of the bundle.

• symm (b : B) (v w : E b) : ((self.inner b) v) w = ((self.inner b) w) v
• pos (b : B) (v : E b) (hv : v ≠ 0) : 0 < ((self.inner b) v) v
• isVonNBounded (b : B) : Bornology.IsVonNBounded ℝ {v : E b | ((self.inner b) v) v < 1}
• contMDiff : ContMDiff IB (IB.prod (modelWithCornersSelf ℝ (F →L[ℝ] F →L[ℝ] ℝ))) n fun (b : B) => TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) b (self.inner b)

def Bundle.ContMDiffRiemannianMetric.toContinuousRiemannianMetric {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] {E : B → Type u_5} [TopologicalSpace (TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)] [FiberBundle F E] [VectorBundle ℝ F E] (g : ContMDiffRiemannianMetric IB n F E) : ContinuousRiemannianMetric F E

A smooth Riemannian metric defines in particular a continuous Riemannian metric.

Equations

• g.toContinuousRiemannianMetric = { inner := g.inner, symm := ⋯, pos := ⋯, isVonNBounded := ⋯, continuous := ⋯ }

def Bundle.ContMDiffRiemannianMetric.toRiemannianMetric {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] {E : B → Type u_5} [TopologicalSpace (TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)] [FiberBundle F E] [VectorBundle ℝ F E] (g : ContMDiffRiemannianMetric IB n F E) : RiemannianMetric E

A smooth Riemannian metric defines in particular a Riemannian metric.

Equations

• g.toRiemannianMetric = g.toContinuousRiemannianMetric.toRiemannianMetric

instance Bundle.instIsContMDiffRiemannianBundle {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] {E : B → Type u_5} [TopologicalSpace (TotalSpace F E)] [(b : B) → TopologicalSpace (E b)] [(b : B) → AddCommGroup (E b)] [(b : B) → Module ℝ (E b)] [∀ (b : B), IsTopologicalAddGroup (E b)] [∀ (b : B), ContinuousConstSMul ℝ (E b)] [FiberBundle F E] [VectorBundle ℝ F E] (g : ContMDiffRiemannianMetric IB n F E) : IsContMDiffRiemannianBundle IB n F E