Lowering the smoothness of a Riemannian metric

A C^n Riemannian metric on a vector bundle is in particular a C^m Riemannian metric for every m ≤ n. This lets a metric built with more regularity than needed, such as an analytic model metric, be used by results stated for smooth metrics.

Main definitions

• Bundle.ContMDiffRiemannianMetric.ofLE: a C^n metric regarded as a C^m metric, m ≤ n.

def Bundle.ContMDiffRiemannianMetric.ofLE {EB : Type u_1} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {m 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) (h : m ≤ n) : ContMDiffRiemannianMetric IB m F E

A C^n Riemannian metric regarded as a C^m Riemannian metric, for m ≤ n.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.ofLE_inner {EB : Type u_1} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {m 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) (h : m ≤ n) : (g.ofLE h).inner = g.inner

Lowering the smoothness of a metric does not change its inner products.

@[simp]

theorem Bundle.ContMDiffRiemannianMetric.toRiemannianMetric_ofLE {EB : Type u_1} [NormedAddCommGroup EB] [NormedSpace ℝ EB] {HB : Type u_2} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {m 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) (h : m ≤ n) : (g.ofLE h).toRiemannianMetric = g.toRiemannianMetric

Lowering the smoothness of a metric does not change the underlying Riemannian metric.

theorem Bundle.ContMDiffRiemannianMetric.inner_eq {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] [∀ (x : B), IsTopologicalAddGroup (E x)] [∀ (x : B), ContinuousConstSMul ℝ (E x)] (g : ContMDiffRiemannianMetric IB n F E) (x : B) (v w : E x) : Inner.inner ℝ v w = ((g.inner x) v) w

The native fibre inner product installed from a metric evaluates to that metric.

theorem Bundle.ContMDiffRiemannianMetric.norm_sq {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] [∀ (x : B), IsTopologicalAddGroup (E x)] [∀ (x : B), ContinuousConstSMul ℝ (E x)] (g : ContMDiffRiemannianMetric IB n F E) (x : B) (v : E x) : ‖v‖ ^ 2 = ((g.inner x) v) v

The squared fibre norm installed from a metric is its diagonal value.