Riemannian and Finsler geometry

Manifolds with smoothly varying inner products or norms on tangent spaces: connections, curvature, geodesics, differential operators and rigidity theorems.

• Conformal classes of Riemannian metrics
• Curvature of Riemannian manifolds
• Finsler metrics
• Hopf–Rinow theorem
• Levi-Civita connection
• Geodesic flow
• Killing vector fields
• Mostow rigidity theorem
• Riemannian gradient and Hessian
• Laplace–Beltrami operator
• Ricci solitons
• Riemannian volume
• Spaces of Riemannian metrics
• Sphere theorem

TheoremExistence of Riemannian metrics#✓fully proved

Let \(E\) be a finite-dimensional real normed space and let \(M\) be a Hausdorff, second-countable \(C^\infty\) manifold modeled on \(E\) (possibly with boundary or corners). Then \(M\) admits a \(C^\infty\) Riemannian metric on its tangent bundle.

theorem riemannianMetricExistence
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
    {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (⊤ : ℕ∞) M]
    [T2Space M] [SecondCountableTopology M]
    : Nonempty (Bundle.ContMDiffRiemannianMetric I (⊤ : ℕ∞) E (fun (x : M) => TangentSpace I x))

Sources

• J. Lee, Introduction to Smooth Manifolds, 2nd ed. existence of Riemannian metrics via partition of unity; also Lee, Riemannian Manifolds; Lean states finite-dimensional Hausdorff second-countable specialization.

Used by 1

Used byClassification of connected \(1\)-manifolds without boundary

DefinitionManifolds admitting a metric of positive scalar curvature#✓fully proved

A smooth manifold \(M\) without boundary modeled on \(\mathbb{R}^n\) admits a metric of positive scalar curvature when some \(C^\infty\) Riemannian metric \(g\) on its tangent bundle has scalar curvature, computed for \(g\), strictly positive at every point of \(M\).

def AdmitsPositiveScalarCurvatureMetric (n : ℕ) (M : Type*) [TopologicalSpace M]
    [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] [IsManifold (𝓡 n) ∞ M] : Prop :=
  ∃ g : ContMDiffRiemannianMetric (𝓡 n) ∞ (EuclideanSpace ℝ (Fin n))
      (fun x : M ↦ TangentSpace (𝓡 n) x),
    letI : RiemannianBundle (fun x : M ↦ TangentSpace (𝓡 n) x) := ⟨g.toRiemannianMetric⟩
    ∀ x : M, 0 < scalarCurvature (𝓡 n) x

Uses 1

Statement usesScalar curvature

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.