Gradients of height functions on the round sphere

For a ∈ E, the height function p ↦ ⟪a, p⟫ on the unit sphere Sⁿ of E differentiates along a tangent vector v as ⟪a, v⟫, with v read in E through the differential of the inclusion. For the round metric its gradient, read in E, is the tangential part a - ⟪a, p⟫ p of a, so its squared length is ‖a‖² - ⟪a, p⟫². In particular, for a unit vector a the squared length of the gradient of the height h is 1 - h², which vanishes exactly at the poles ±a.

These gradients span every tangent space of the sphere; they are the vector fields from which the curvature of the round sphere is computed, and the negative gradient flow of a height function moves points along the meridians towards the south pole.

Main results

• TauCeti.mvfderiv_inner_coe_sphere: the differential of the height function p ↦ ⟪a, p⟫.
• TauCeti.mvfderiv_coe_mgradient_inner_coe_sphere: its round gradient, read in E, is a - ⟪a, p⟫ p.
• TauCeti.norm_mgradient_inner_coe_sphere_sq: the squared length of that gradient is ‖a‖² - ⟪a, p⟫².

References

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

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

The differential of the height function p ↦ ⟪a, p⟫ on the unit sphere sends a tangent vector v to ⟪a, v⟫, with v read in E through the differential of the inclusion.

theorem TauCeti.mvfderiv_coe_mgradient_inner_coe_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (a : E) (p : ↑(Metric.sphere 0 1)) : (d% Subtype.val p) (Manifold.mgradient (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (fun (q : ↑(Metric.sphere 0 1)) => inner ℝ a ↑q) p) = a - inner ℝ a ↑p • ↑p

The round gradient of a height function. Read in E, the gradient at p of the height function q ↦ ⟪a, q⟫ for the round metric is the tangential part a - ⟪a, p⟫ p of a.

theorem TauCeti.norm_mgradient_inner_coe_sphere_sq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (a : E) (p : ↑(Metric.sphere 0 1)) : ‖Manifold.mgradient (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (fun (q : ↑(Metric.sphere 0 1)) => inner ℝ a ↑q) p‖ ^ 2 = ‖a‖ ^ 2 - inner ℝ a ↑p ^ 2

The length of the round gradient of a height function. The squared length at p of the round gradient of q ↦ ⟪a, q⟫ is ‖a‖² - ⟪a, p⟫².