Riemannian metrics on a vector space from coercive bilinear forms

A real normed space F is a manifold modelled on itself, and its tangent space at every point is F. Many Riemannian metrics are written in such global coordinates, as a field g : F → F →L[ℝ] F →L[ℝ] ℝ of symmetric bilinear forms; examples are the left-invariant metrics of the three-dimensional model geometries Nil and Sol on ℝ³. This file shows that such a field is a C^n Riemannian metric as soon as it is C^n and each g x is coercive (IsCoercive (g x): C ‖v‖² ≤ g x v v for some C > 0 depending on x). Coercivity makes g x positive definite and its unit ball bounded, as ContMDiffRiemannianMetric requires. Mathlib's riemannianMetricVectorSpace is the constant field given by the inner product of an inner product space.

Main definitions

• TauCeti.coerciveRiemannianMetric: the C^n Riemannian metric on F given by a C^n field of symmetric coercive bilinear forms.

noncomputable def TauCeti.coerciveRiemannianMetric {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : WithTop ℕ∞} (g : F → F →L[ℝ] F →L[ℝ] ℝ) (hg : ContDiff ℝ n g) (symm : ∀ (x v w : F), ((g x) v) w = ((g x) w) v) (coercive : ∀ (x : F), IsCoercive (g x)) : Bundle.ContMDiffRiemannianMetric (modelWithCornersSelf ℝ F) n F fun (x : F) => TangentSpace (modelWithCornersSelf ℝ F) x

A C^n field of symmetric coercive bilinear forms on a real normed space F is a C^n Riemannian metric on F, with inner product g x on the tangent space at x.

@[simp]

theorem TauCeti.coerciveRiemannianMetric_inner {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {n : WithTop ℕ∞} (g : F → F →L[ℝ] F →L[ℝ] ℝ) (hg : ContDiff ℝ n g) (symm : ∀ (x v w : F), ((g x) v) w = ((g x) w) v) (coercive : ∀ (x : F), IsCoercive (g x)) (x : F) (v w : TangentSpace (modelWithCornersSelf ℝ F) x) : (((coerciveRiemannianMetric g hg symm coercive).inner x) v) w = ((g x) ((tangentSpaceCastModel (modelWithCornersSelf ℝ F) x) v)) ((tangentSpaceCastModel (modelWithCornersSelf ℝ F) x) w)

The metric coerciveRiemannianMetric g is g x on the tangent space at x, read in the model space F.