Length of radial geodesic segments #
In a normal domain, the radial exponential curve has length equal to the norm of its initial
velocity times the elapsed parameter on every subinterval of [0, 1]. This formula gives the
length of the radial candidate path in a normal neighbourhood.
The length calculation uses the constant-speed formula for maximal geodesics in
TauCeti.Manifold.pathELength_maximalGeodesic.
References #
- M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 3, §3.
- J. M. Lee, Introduction to Riemannian Manifolds, Springer, 2018, Ch. 6.
theorem
TauCeti.Manifold.pathELength_riemannianExp_smul
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[EMetricSpace M]
[ChartedSpace H M]
[FiniteDimensional ℝ E]
[I.Boundaryless]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
[IsManifold I (↑⊤) M]
[IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x]
{p : M}
{U : Set (TangentSpace I p)}
(h : IsNormalDomain I M p U)
{v : TangentSpace I p}
(hv : v ∈ U)
{s t : ℝ}
(hs : s ∈ Set.Icc 0 1)
(ht : t ∈ Set.Icc 0 1)
:
Manifold.pathELength I (fun (u : ℝ) => riemannianExp I M p (u • v)) s t = ‖v‖ₑ * ENNReal.ofReal (t - s)
In a normal domain, the radial exponential curve between parameters s and t in [0, 1]
has length ‖v‖ * ENNReal.ofReal (t - s).
theorem
TauCeti.Manifold.pathELength_riemannianExp_smul_zero_one
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{M : Type u_3}
[EMetricSpace M]
[ChartedSpace H M]
[FiniteDimensional ℝ E]
[I.Boundaryless]
[Bundle.RiemannianBundle fun (x : M) => TangentSpace I x]
[IsManifold I (↑⊤) M]
[IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x]
{p : M}
{U : Set (TangentSpace I p)}
(h : IsNormalDomain I M p U)
{v : TangentSpace I p}
(hv : v ∈ U)
:
In a normal domain, the radial exponential curve from 0 to 1 has length ‖v‖.