Riemannian Metric Definitions #
This module defines the Riemannian metric, building on pseudo-Riemannian metrics.
A RiemannianMetric on a manifold M modeled on H with corners I (over the model space E
, typically ℝ^m) is a family of inner products on the tangent spaces TangentSpace I x
for each x : M. This family is required to vary smoothly with x, specifically with smoothness
C^n.
This structure extends PseudoRiemannianMetric, inheriting the core properties of a
pseudo-Riemannian metric, such as being a symmetric, non-degenerate, C^n-smooth tensor field
of type (0,2). The key distinguishing feature of a Riemannian metric is its positive-definiteness.
The pos_def' field ensures that for any point x on the manifold and any non-zero tangent
vector v at x, the inner product gₓ(v, v) (denoted val x v v) is strictly positive.
This condition makes each val x (the metric at point x) a positive-definite symmetric
bilinear form, effectively an inner product, on the tangent space TangentSpace I x.
Parameters:
I: TheModelWithCornersfor the manifoldM. This defines the model spaceE(e.g.,ℝ^d) and the model space for the boundaryH.n: The smoothness class of the metric, anℕ∞value. The metric tensor components areC^nfunctions.M: The type of the manifold.[TopologicalSpace M]: AssumesMhas a topological structure.[ChartedSpace H M]: AssumesMis equipped with an atlas of charts toH.[IsManifold I (n + 1) M]: AssumesMis a manifold of smoothnessC^(n+1). The manifold needs to be slightly smoother than the metric itself for certain constructions.[inst_tangent_findim : ∀ (x : M), FiniteDimensional ℝ (TangentSpace I x)]: Ensures that each tangent space is a finite-dimensional real vector space.
Fields:
toPseudoRiemannianMetric: The underlying pseudo-Riemannian metric. This provides the smooth family of symmetric bilinear formsval : M → SymBilinForm ℝ (TangentSpace I ·).pos_def': The positive-definiteness condition:∀ x v, v ≠ 0 → val x v v > 0. This asserts that for any pointxand any non-zero tangent vectorvatx, the metric evaluated on(v, v)is strictly positive.
- nondegenerate (x : M) (v : TangentSpace I x) : (∀ (w : TangentSpace I x), ((self.val x) v) w = 0) → v = 0
- smooth_in_charts' (x₀ : M) (v w : E) : let e := extChartAt I x₀; ContDiffWithinAt ℝ (↑n) (fun (y : E) => ((self.val (↑e.symm y)) ((mfderiv I I (↑e.symm) y) v)) ((mfderiv I I (↑e.symm) y) w)) e.target (↑e x₀)
- negDim_isLocallyConstant : IsLocallyConstant fun (x : M) => let_fun this := ⋯; (pseudoRiemannianMetricValToQuadraticForm✝ self.val ⋯ x).negDim
gₓ(v, v) > 0for all nonzerov.valis inherited fromPseudoRiemannianMetric.
Instances For
Coercion from RiemannianMetric to its underlying PseudoRiemannianMetric.
Equations
- PseudoRiemannianMetric.RiemannianMetric.instCoeSomeENat = { coe := fun (g : PseudoRiemannianMetric.RiemannianMetric I n M) => g.toPseudoRiemannianMetric }
The quadratic form associated with a Riemannian metric is positive definite.
InnerProductSpace structure from RiemannianMetric #
The InnerProductSpace.Core structure for TₓM induced by a Riemannian metric g.
This provides the properties of an inner product: symmetry,
non-negativity, linearity, and definiteness.
Each gₓ is an inner product on TₓM (O'Neill, p. 55).
Equations
- g.tangentInnerCore x = { inner := fun (v w : TangentSpace I x) => g.inner x v w, conj_inner_symm := ⋯, re_inner_nonneg := ⋯, add_left := ⋯, smul_left := ⋯, definite := ⋯ }
Instances For
Local NormedAddCommGroup and InnerProductSpace Instances #
These instances are defined locally to be used when a specific Riemannian metric g
and point x are in context. They are not global instances to avoid typeclass conflicts
and to respect the fact that a manifold might not have a canonical Riemannian metric,
or might be studied with an indefinite (pseudo-Riemannian) metric where these
standard norm structures are not appropriate.
Creates a NormedAddCommGroup structure on TₓM from a Riemannian metric g.
Equations
Instances For
Creates an InnerProductSpace structure on TₓM from a Riemannian metric g.
Alternative implementation using letI.
Equations
Instances For
Creates an InnerProductSpace structure on TₓM from a Riemannian metric g.
Equations
Instances For
The norm on a tangent space induced by a Riemannian metric, defined as the square root of the inner product of a vector with itself.
Instances For
Helper function to compute the norm on a tangent space from a Riemannian metric,
using the underlying NormedAddCommGroup structure.
Instances For
Curve #
Calculates the length of a curve γ between parameters t₀ and t₁
using the Riemannian metric g. This is defined as the integral of the norm of
the tangent vector along the curve.