Normal domains and the Riemannian logarithm

A normal domain at a point p of a Riemannian manifold is an open star-shaped neighbourhood U of the origin of T_p M, inside the natural domain of the exponential map, on which exp_p restricts to a diffeomorphism onto its image. The image exp_p '' U is the associated normal neighbourhood of p.

Since the differential of exp_p at the origin is the identity, the inverse function theorem produces a ball of some positive radius that is a normal domain at every point. On a normal neighbourhood the restricted exponential map has an inverse, the Riemannian logarithm log_p, which is again smooth; it is the chart underlying normal coordinates, and it turns a point of the normal neighbourhood into the initial velocity of the radial geodesic reaching it.

The logarithm is defined as a total function taking a junk value outside the normal neighbourhood, so each theorem about its value carries the corresponding membership hypothesis. There is deliberately no single global logarithm: beyond a normal neighbourhood the exponential map may lose injectivity or local invertibility, so no canonical smooth global inverse is provided.

Main definitions and results

• TauCeti.Manifold.IsNormalDomain: the predicate defining normal domains.
• TauCeti.Manifold.riemannianLog: the Riemannian logarithm relative to a normal domain.
• TauCeti.Manifold.IsNormalDomain.toPartialDiffeomorph: the exponential map and logarithm as a partial diffeomorphism between a normal domain and its normal neighbourhood.
• TauCeti.Manifold.IsNormalDomain.exists_partialDiffeomorph_riemannianExp_comp: the exponential map precomposed with a linear isomorphism carrying an open set into a normal domain is a partial diffeomorphism with that open set as source.
• TauCeti.Manifold.exists_isNormalDomain_ball: balls of small enough radius are normal domains.
• TauCeti.Manifold.IsNormalDomain.ball: a tangent ball contained in a normal domain is itself a normal domain.
• TauCeti.Manifold.isCompact_riemannianExp_image_closedBall: a closed tangent ball in the exponential domain has compact exponential image.
• TauCeti.Manifold.isCompact_riemannianExp_image_sphere: a tangent sphere in the exponential domain has compact exponential image.
• TauCeti.Manifold.exists_isNormalDomain_ball_with_isCompact_riemannianExp_image_closedBall: a smaller closed tangent ball inside a larger normal ball has compact exponential image.
• TauCeti.Manifold.IsNormalDomain.isOpen_image: a normal neighbourhood is open.
• TauCeti.Manifold.IsNormalDomain.injective_mfderiv_riemannianExp: the differential of the exponential map is injective on a normal domain.
• TauCeti.Manifold.IsNormalDomain.contDiffOn_norm_angular_riemannianExp: the length of the differential of the exponential map along a fixed vector is smooth on a normal domain.
• TauCeti.Manifold.IsNormalDomain.riemannianLog_riemannianExp and TauCeti.Manifold.riemannianExp_riemannianLog: the two inverse identities.
• TauCeti.Manifold.IsNormalDomain.riemannianLog_self: the logarithm vanishes at the base point.
• TauCeti.Manifold.IsNormalDomain.contMDiffOn_riemannianLog: the logarithm is smooth on the normal neighbourhood.
• TauCeti.Manifold.IsNormalDomain.mfderiv_riemannianLog_comp_mfderiv_riemannianExp and TauCeti.Manifold.IsNormalDomain.mfderiv_riemannianExp_comp_mfderiv_riemannianLog: the differentials of the logarithm and the exponential map are mutually inverse.
• TauCeti.Manifold.IsNormalDomain.mem_geodesicInterval: the geodesic towards a vector of a normal domain is defined at least up to time one.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 3, §3.
• J. M. Lee, Introduction to Riemannian Manifolds, Springer, 2018, Ch. 5 and 6.

Normal domains

structure TauCeti.Manifold.IsNormalDomain {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)) : Prop

A normal domain at p is an open star-shaped neighbourhood U of the origin of T_p M, contained in the natural domain of the exponential map, on which exp_p restricts to a diffeomorphism onto its image. The image exp_p '' U is the associated normal neighbourhood of p.

• isOpen : IsOpen U

  A normal domain is open.

• zero_mem : 0 ∈ U

  A normal domain contains the origin.

• starConvex : StarConvex ℝ 0 U

  A normal domain is star-shaped at the origin.

• subset_expDomain : U ⊆ expDomain I M p

  A normal domain lies in the natural domain of the exponential map.

• injOn : Set.InjOn (riemannianExp I M p) U

  The exponential map is injective on a normal domain.

• isLocalDiffeomorphOn : IsLocalDiffeomorphOn (modelWithCornersSelf ℝ (TangentSpace I p)) I (↑⊤) (riemannianExp I M p) U

  The exponential map is a local diffeomorphism at each vector of a normal domain.

theorem TauCeti.Manifold.IsNormalDomain.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] {p : M} {U V : Set (TangentSpace I p)} (h : IsNormalDomain I M p U) (hVU : V ⊆ U) (hV : IsOpen V) (hzero : 0 ∈ V) (hstar : StarConvex ℝ 0 V) : IsNormalDomain I M p V

An open star-shaped neighbourhood of the origin inside a normal domain is a normal domain.

theorem TauCeti.Manifold.IsNormalDomain.ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)} {r : ℝ} (h : IsNormalDomain I M p U) (hU : Metric.ball 0 r ⊆ U) (hr : 0 < r) : IsNormalDomain I M p (Metric.ball 0 r)

A tangent ball contained in a normal domain is itself a normal domain.

theorem TauCeti.Manifold.IsNormalDomain.isOpen_image {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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) : IsOpen (riemannianExp I M p '' U)

A normal neighbourhood is open.

theorem TauCeti.Manifold.IsNormalDomain.injective_mfderiv_riemannianExp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)} {v : TangentSpace I p} (h : IsNormalDomain I M p U) (hv : v ∈ U) : Function.Injective ⇑(mfderiv% (riemannianExp I M p) v)

The differential of the exponential map is injective at every vector of a normal domain.

theorem TauCeti.Manifold.IsNormalDomain.smul_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)} {v : TangentSpace I p} {t : ℝ} (h : IsNormalDomain I M p U) (hv : v ∈ U) (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) : t • v ∈ U

A vector of a normal domain can be shrunk towards the origin inside the normal domain.

theorem TauCeti.Manifold.IsNormalDomain.mem_geodesicInterval {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)} {v : TangentSpace I p} {t : ℝ} (h : IsNormalDomain I M p U) (hv : v ∈ U) (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) : t ∈ geodesicInterval I M p v

The radial geodesic of a normal domain is defined up to time one. The maximal geodesic from p with initial velocity a vector v of a normal domain exists on [0, 1]; by riemannianExp_smul its value at t is the exponential of t • v.

theorem TauCeti.Manifold.IsNormalDomain.self_mem_image {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)} [I.Boundaryless] [T2Space M] (h : IsNormalDomain I M p U) : p ∈ riemannianExp I M p '' U

The base point belongs to every normal neighbourhood.

theorem TauCeti.Manifold.IsNormalDomain.image_mem_nhds {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)} [I.Boundaryless] [T2Space M] (h : IsNormalDomain I M p U) : riemannianExp I M p '' U ∈ nhds p

A normal neighbourhood is a neighbourhood of the base point.

theorem TauCeti.Manifold.IsNormalDomain.contDiffOn_norm_angular_riemannianExp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)} [I.Boundaryless] [T2Space M] {w : TangentSpace I p} (h : IsNormalDomain I M p U) : ContDiffOn ℝ (↑⊤) (fun (z : TangentSpace I p) => ‖(mfderiv% (riemannianExp I M p) z) w‖) U

The Riemannian length of the differential of the exponential map, applied to a fixed tangent vector w, is smooth on any normal domain, where that differential is injective.

Existence of normal balls

theorem TauCeti.Manifold.exists_isNormalDomain_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [I.Boundaryless] [T2Space M] (p : M) : ∃ (r : ℝ), 0 < r ∧ IsNormalDomain I M p (Metric.ball 0 r)

Normal balls exist. There is a positive radius such that the ball of that radius around the origin of T_p M is a normal domain at p; its image is a normal neighbourhood of p.

Compactly contained normal balls

theorem TauCeti.Manifold.isCompact_riemannianExp_image_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [I.Boundaryless] [T2Space M] (p : M) {r : ℝ} (hr : Metric.closedBall 0 r ⊆ expDomain I M p) : IsCompact (riemannianExp I M p '' Metric.closedBall 0 r)

The exponential image of a closed tangent ball contained in the exponential domain is compact.

theorem TauCeti.Manifold.isCompact_riemannianExp_image_sphere {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [I.Boundaryless] [T2Space M] (p : M) {r : ℝ} (hr : Metric.sphere 0 r ⊆ expDomain I M p) : IsCompact (riemannianExp I M p '' Metric.sphere 0 r)

The exponential image of a tangent sphere contained in the exponential domain is compact.

theorem TauCeti.Manifold.exists_isNormalDomain_ball_with_isCompact_riemannianExp_image_closedBall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [I.Boundaryless] [T2Space M] (p : M) : ∃ (r : ℝ) (R : ℝ), 0 < r ∧ r < R ∧ IsNormalDomain I M p (Metric.ball 0 R) ∧ Metric.closedBall 0 r ⊆ Metric.ball 0 R ∧ IsCompact (riemannianExp I M p '' Metric.closedBall 0 r)

Normal balls can be chosen compactly contained in a larger normal ball. More precisely, there are positive radii r < R such that the ball of radius R is a normal domain and the closed ball of radius r is contained in it. The exponential image of that closed ball is compact.

The nested tangent balls and compact exponential image are inputs to the escape estimate for curves leaving a normal neighbourhood.

The Riemannian logarithm

noncomputable def TauCeti.Manifold.riemannianLog {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)) : M → TangentSpace I p

The Riemannian logarithm at p relative to a set U of tangent vectors, defined as the chosen preimage function invFunOn for the restriction of exp_p to U. When U is a normal domain, it inverts exp_p on the normal neighbourhood exp_p '' U; outside that neighbourhood it takes a junk value, so every theorem about its value carries a membership hypothesis.

theorem TauCeti.Manifold.riemannianLog_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)) : riemannianLog I M p U = Function.invFunOn (riemannianExp I M p) U

The Riemannian logarithm relative to U is invFunOn for exp_p restricted to U.

theorem TauCeti.Manifold.riemannianLog_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)} {q : M} (hq : q ∈ riemannianExp I M p '' U) : riemannianLog I M p U q ∈ U

The logarithm of a point of exp_p '' U lies in U.

@[simp]

theorem TauCeti.Manifold.riemannianExp_riemannianLog {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)} {q : M} (hq : q ∈ riemannianExp I M p '' U) : riemannianExp I M p (riemannianLog I M p U q) = q

The exponential map inverts the logarithm on exp_p '' U.

@[simp]

theorem TauCeti.Manifold.IsNormalDomain.riemannianLog_riemannianExp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)} {v : TangentSpace I p} (h : IsNormalDomain I M p U) (hv : v ∈ U) : riemannianLog I M p U (riemannianExp I M p v) = v

The logarithm inverts the exponential map on a normal domain.

theorem TauCeti.Manifold.IsNormalDomain.contMDiffOn_riemannianLog {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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) : ContMDiffOn I (modelWithCornersSelf ℝ (TangentSpace I p)) (↑⊤) (riemannianLog I M p U) (riemannianExp I M p '' U)

The Riemannian logarithm is smooth on the normal neighbourhood it inverts.

theorem TauCeti.Manifold.IsNormalDomain.mdifferentiableAt_riemannianLog {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)} {q : M} (h : IsNormalDomain I M p U) (hq : q ∈ riemannianExp I M p '' U) : MDiffAt (riemannianLog I M p U) q

The Riemannian logarithm is differentiable at every point of the normal neighbourhood.

theorem TauCeti.Manifold.IsNormalDomain.continuousOn_riemannianLog {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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) : ContinuousOn (riemannianLog I M p U) (riemannianExp I M p '' U)

The Riemannian logarithm is continuous on the normal neighbourhood it inverts.

noncomputable def TauCeti.Manifold.IsNormalDomain.toPartialDiffeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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) : PartialDiffeomorph (modelWithCornersSelf ℝ (TangentSpace I p)) I (TangentSpace I p) M ↑⊤

The exponential map and Riemannian logarithm as a partial diffeomorphism from a normal domain to its normal neighbourhood.

@[simp]

theorem TauCeti.Manifold.IsNormalDomain.toPartialDiffeomorph_source {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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) : h.toPartialDiffeomorph.source = U

The source of the normal-domain partial diffeomorphism is the normal domain.

@[simp]

theorem TauCeti.Manifold.IsNormalDomain.toPartialDiffeomorph_target {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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) : h.toPartialDiffeomorph.target = riemannianExp I M p '' U

The target of the normal-domain partial diffeomorphism is the normal neighbourhood.

@[simp]

theorem TauCeti.Manifold.IsNormalDomain.coe_toPartialDiffeomorph {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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) : ↑h.toPartialDiffeomorph.toPartialEquiv = riemannianExp I M p

The forward map of the normal-domain partial diffeomorphism is the exponential map.

@[simp]

theorem TauCeti.Manifold.IsNormalDomain.toPartialDiffeomorph_symm_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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) (q : M) : ↑h.toPartialDiffeomorph.symm q = riemannianLog I M p U q

The inverse map of the normal-domain partial diffeomorphism is the Riemannian logarithm.

theorem TauCeti.Manifold.IsNormalDomain.exists_partialDiffeomorph_riemannianExp_comp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] (h : IsNormalDomain I M p U) (A : F ≃L[ℝ] TangentSpace I p) {s : Set F} (hs : IsOpen s) (hmap : Set.MapsTo (⇑A) s U) : ∃ (Φ : PartialDiffeomorph (modelWithCornersSelf ℝ F) I F M ↑⊤), Φ.source = s ∧ ↑Φ.toPartialEquiv = riemannianExp I M p ∘ ⇑A

The exponential map precomposed with a linear isomorphism that maps an open set into a normal domain is a partial diffeomorphism with that open set as source.

theorem TauCeti.Manifold.IsNormalDomain.mfderiv_riemannianLog_comp_mfderiv_riemannianExp {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)} {v : TangentSpace I p} (h : IsNormalDomain I M p U) (hv : v ∈ U) : mfderiv% (riemannianLog I M p U) (riemannianExp I M p v) ∘SL mfderiv% (riemannianExp I M p) v = ContinuousLinearMap.id ℝ (TangentSpace I p)

The differential of the logarithm at exp_p v is a left inverse of the differential of the exponential map at a vector v of the normal domain.

theorem TauCeti.Manifold.IsNormalDomain.mfderiv_riemannianExp_comp_mfderiv_riemannianLog {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)} {v : TangentSpace I p} (h : IsNormalDomain I M p U) (hv : v ∈ U) : mfderiv% (riemannianExp I M p) v ∘SL mfderiv% (riemannianLog I M p U) (riemannianExp I M p v) = ContinuousLinearMap.id ℝ (TangentSpace I (riemannianExp I M p v))

The differential of the logarithm at exp_p v is a right inverse of the differential of the exponential map at a vector v of the normal domain.

theorem TauCeti.Manifold.IsNormalDomain.isInvertible_mfderiv_riemannianLog {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)} {q : M} (h : IsNormalDomain I M p U) (hq : q ∈ riemannianExp I M p '' U) : (mfderiv% (riemannianLog I M p U) q).IsInvertible

The differential of the logarithm is invertible at every point of the normal neighbourhood.

@[simp]

theorem TauCeti.Manifold.IsNormalDomain.riemannianLog_self {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [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)} [I.Boundaryless] [T2Space M] (h : IsNormalDomain I M p U) : riemannianLog I M p U p = 0

The logarithm vanishes at the base point.