The round metric on the unit sphere

The unit sphere Sⁿ of a real inner product space E of dimension n + 1 is an analytic manifold modelled on ℝⁿ (Mathlib's stereographic atlas), and its inclusion into E is an analytic immersion. The round metric is the Riemannian metric induced by this immersion: the inner product of two tangent vectors is the inner product in E of their images under the differential of the inclusion. This file installs it as the RiemannianBundle instance on the tangent bundle of the sphere, together with its analyticity.

With E = EuclideanSpace ℝ (Fin 4) this is the round three-sphere S³, the spherical one of Thurston's eight model geometries.

Main definitions

• TauCeti.sphereTangentEquiv: the isometric identification of tangent spaces with the orthogonal complements of their radius vectors.
• TauCeti.sphereRoundMetric: the analytic round metric on the unit sphere.
• TauCeti.instRiemannianBundleSphere, TauCeti.instIsContMDiffRiemannianBundleSphere and TauCeti.instIsContinuousRiemannianBundleSphere: the corresponding instances.

Main statements

• TauCeti.inner_tangentSpace_sphere: the round inner product of two tangent vectors is the inner product of their images in E.
• TauCeti.norm_tangentSpace_sphere: the round norm of a tangent vector is the norm of its image in E.
• TauCeti.inner_coe_mvfderiv_subtypeVal_sphere: tangent vectors are orthogonal to the radius.
• TauCeti.edist_le_riemannianEDist_sphere: the chordal distance in E is at most the round distance.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 2 (the round metric as an induced metric).

noncomputable def TauCeti.sphereRoundMetric {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] : Bundle.ContMDiffRiemannianMetric (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ (EuclideanSpace ℝ (Fin n)) fun (x : ↑(Metric.sphere 0 1)) => TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) x

The round metric on the unit sphere of E: the analytic Riemannian metric induced by the inclusion of the sphere into E.

@[simp]

theorem TauCeti.sphereRoundMetric_inner {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (x : ↑(Metric.sphere 0 1)) (v w : TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) x) : ((sphereRoundMetric.inner x) v) w = inner ℝ ((d% Subtype.val x) v) ((d% Subtype.val x) w)

The round metric evaluates the inner product of E on the images of tangent vectors under the differential of the inclusion.

@[instance_reducible]

noncomputable instance TauCeti.instRiemannianBundleSphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] : Bundle.RiemannianBundle fun (x : ↑(Metric.sphere 0 1)) => TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) x

The unit sphere is a Riemannian manifold for its round metric.

instance TauCeti.instIsContMDiffRiemannianBundleSphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] : IsContMDiffRiemannianBundle (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ⊤ (EuclideanSpace ℝ (Fin n)) fun (x : ↑(Metric.sphere 0 1)) => TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) x

The round metric is analytic.

instance TauCeti.instIsContinuousRiemannianBundleSphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] : IsContinuousRiemannianBundle (EuclideanSpace ℝ (Fin n)) fun (x : ↑(Metric.sphere 0 1)) => TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) x

The round metric is continuous.

@[simp]

theorem TauCeti.inner_tangentSpace_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (x : ↑(Metric.sphere 0 1)) (v w : TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) x) : inner ℝ v w = inner ℝ ((d% Subtype.val x) v) ((d% Subtype.val x) w)

The round inner product of two tangent vectors to the sphere is the inner product in E of their images under the differential of the inclusion.

@[simp]

theorem TauCeti.norm_tangentSpace_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (x : ↑(Metric.sphere 0 1)) (v : TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) x) : ‖v‖ = ‖(d% Subtype.val x) v‖

The round norm of a tangent vector to the sphere is the norm in E of its image under the differential of the inclusion.

noncomputable def TauCeti.sphereTangentEquiv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (x : ↑(Metric.sphere 0 1)) : TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) x ≃ₗᵢ[ℝ] ↥(ℝ ∙ ↑x)ᗮ

The differential of the unit-sphere inclusion identifies its round tangent space isometrically with the orthogonal complement of the radius vector.

@[simp]

theorem TauCeti.coe_sphereTangentEquiv_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (x : ↑(Metric.sphere 0 1)) (v : TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) x) : ↑((sphereTangentEquiv x) v) = (mfderiv% Subtype.val x) v

In ambient coordinates, the tangent-space identification is the differential of inclusion.

theorem TauCeti.inner_coe_mvfderiv_subtypeVal_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (x : ↑(Metric.sphere 0 1)) (v : TangentSpace (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) x) : inner ℝ (↑x) ((d% Subtype.val x) v) = 0

The image of a tangent vector under the differential of the sphere inclusion is orthogonal to the radius vector.

theorem TauCeti.edist_le_riemannianEDist_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (x y : ↑(Metric.sphere 0 1)) : edist x y ≤ Manifold.riemannianEDist (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) x y

The chordal distance is at most the round distance. The distance in E between two points of the unit sphere is at most their Riemannian distance for the round metric: the inclusion of the sphere into E preserves the length of tangent vectors, so every path on the sphere is at least as long as the chord between its endpoints.