The escape estimate for normal neighbourhoods

This module provides the escape estimate for normal neighbourhoods: a path that starts at the centre and leaves the exponential image of the domain has length at least the radius of a smaller tangent ball contained in that domain. It also provides a strict comparison with the radial segment to a point in the smaller ball when the path leaves the larger domain.

References

• The Apache-2.0 frenzymath/Poincare-Conjecture formalization, revision 24f32e4d600878bfaac6bc2f2f9324175571c321, especially DoCarmoLib/Riemannian/Exponential/NormalBallEDist.lean and DoCarmoLib/Riemannian/Exponential/MinimizingPathPiecewise.lean.
• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 3, §3, Proposition 3.6.
• J. M. Lee, Introduction to Riemannian Manifolds, Springer, 2018, Ch. 6, Prop. 6.11.

theorem TauCeti.Manifold.IsNormalDomain.pathELength_escape {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)} {r : ℝ} (h : IsNormalDomain I M p U) (hr : 0 < r) (hclosed : Metric.closedBall 0 r ⊆ U) {γ : ℝ → M} (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc 0 1)) (hγ0 : γ 0 = p) (hex : ∃ t ∈ Set.Icc 0 1, γ t ∉ riemannianExp I M p '' U) : ENNReal.ofReal r ≤ Manifold.pathELength I γ 0 1

The escape estimate for a normal neighbourhood. If a C¹ path starts at the centre p of a normal domain U and meets the complement of riemannianExp p '' U, then its length is at least ENNReal.ofReal r whenever 0 < r and Metric.closedBall 0 r ⊆ U.

theorem TauCeti.Manifold.IsNormalDomain.pathELength_riemannianExp_smul_lt_of_not_mapsTo {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)} {r : ℝ} {v : TangentSpace I p} (h : IsNormalDomain I M p U) (hclosed : Metric.closedBall 0 r ⊆ U) (hv : v ∈ Metric.ball 0 r) {γ : ℝ → M} (hγ : ContMDiffOn (modelWithCornersSelf ℝ ℝ) I 1 γ (Set.Icc 0 1)) (hγ0 : γ 0 = p) (hleave : ¬Set.MapsTo γ (Set.Icc 0 1) (riemannianExp I M p '' U)) : Manifold.pathELength I (fun (t : ℝ) => riemannianExp I M p (t • v)) 0 1 < Manifold.pathELength I γ 0 1

A C¹ competitor that starts at the centre and leaves the larger normal domain is strictly longer than the radial segment to a point in a smaller normal ball.