Geodesics, the exponential map, and the Hopf–Rinow theorem

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremThe Hopf–Rinow theorem#

For a point p of a Riemannian manifold M whose distance is the Riemannian distance, the following are equivalent: the exponential map at p is defined on all of T_p M; M is proper; M is complete; every maximal geodesic of M is defined for all time; and M has an increasing exhaustion by compact sets K n such that dist p (q n) → ∞ whenever q n ∉ K n for every n.

TauCeti.Manifold.tfae_expDomain_eq_univ.{u_1, u_2, u_3} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3}
  [MetricSpace M] [ChartedSpace H M] [FiniteDimensional ℝ E] [I.Boundaryless]
  [Bundle.RiemannianBundle fun x => TangentSpace I x] [IsManifold I (↑⊤) M]
  [IsContMDiffRiemannianBundle I (↑⊤) E fun x => TangentSpace I x] [IsRiemannianManifold I M]
  (p : M) :
  [TauCeti.Manifold.expDomain I M p = Set.univ, ProperSpace M, CompleteSpace M,
      ∀ (q : M), TauCeti.Manifold.IsGeodesicallyCompleteAt I M q,
      ∃ K,
        (∀ (n : ℕ), IsCompact (K n)) ∧
          Monotone K ∧
            ⋃ n, K n = Set.univ ∧
              ∀ (q : ℕ → M),
                (∀ (n : ℕ), q n ∉ K n) →
                  Filter.Tendsto (fun n => dist p (q n)) Filter.atTop Filter.atTop].TFAE

Lean

Formalized in Tau Ceti as TauCeti.Manifold.tfae_expDomain_eq_univ.

Sources

• Tau Ceti documentation: TauCeti.Manifold.tfae_expDomain_eq_univ
• Source of TauCeti.Manifold.tfae_expDomain_eq_univ in TauCeti/Geometry/Manifold/Riemannian/Geodesic/HopfRinow.lean
• Tau Ceti roadmap status: Geodesics, the exponential map, and the Hopf–Rinow theorem

LeanTauCeti.Manifold.tfae_expDomain_eq_univ

Uses 4

Proof usesThe Gauss lemma · The inverse function theorem for manifolds · The Koszul formula · TauCeti.Manifold.riemannianExp

TheoremA compact Riemannian manifold is geodesically complete#

every maximal geodesic leaving a point p is defined for all time. This is do Carmo's corollary to the Hopf–Rinow theorem.

TauCeti.Manifold.isGeodesicallyCompleteAt_of_compactSpace.{u_1, u_2, u_3} {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] [I.Boundaryless] [Bundle.RiemannianBundle fun x => TangentSpace I x]
  [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun x => TangentSpace I x] [T2Space M]
  [CompactSpace M] (p : M) : TauCeti.Manifold.IsGeodesicallyCompleteAt I M p

Lean

Formalized in Tau Ceti as TauCeti.Manifold.isGeodesicallyCompleteAt_of_compactSpace.

Sources

• Tau Ceti documentation: TauCeti.Manifold.isGeodesicallyCompleteAt_of_compactSpace
• Source of TauCeti.Manifold.isGeodesicallyCompleteAt_of_compactSpace in TauCeti/Geometry/Manifold/Riemannian/Geodesic/Compact.lean
• Tau Ceti roadmap status: Geodesics, the exponential map, and the Hopf–Rinow theorem

LeanTauCeti.Manifold.isGeodesicallyCompleteAt_of_compactSpace

Uses 1

Proof usesThe Koszul formula

TheoremThe Gauss lemma#

The differential of the Riemannian exponential map preserves the inner product with the radial direction at every vector in its natural domain.

TauCeti.Manifold.inner_mfderiv_riemannianExp_radial.{u_1, u_2, u_3} {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 => TangentSpace I x] [IsManifold I (↑⊤) M]
  [IsContMDiffRiemannianBundle I (↑⊤) E fun x => TangentSpace I x] [I.Boundaryless] [T2Space M]
  {p : M} {v w : TangentSpace I p} (hv : v ∈ TauCeti.Manifold.expDomain I M p) :
  inner ℝ ((mfderiv% (TauCeti.Manifold.riemannianExp I M p) v) v)
      ((mfderiv% (TauCeti.Manifold.riemannianExp I M p) v) w) =
    inner ℝ v w

Lean

Formalized in Tau Ceti as TauCeti.Manifold.inner_mfderiv_riemannianExp_radial.

Other forms

The Gauss lemma in an inner-product space. Formalized in Tau Ceti as TauCeti.Manifold.inner_mfderiv_riemannianExp_model_space.

TauCeti.Manifold.inner_mfderiv_riemannianExp_model_space.{u_1} {F : Type u_1} [NormedAddCommGroup F]
  [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] (p : F)
  (v w₁ w₂ : TangentSpace (modelWithCornersSelf ℝ F) p) :
  inner ℝ ((mfderiv% (TauCeti.Manifold.riemannianExp (modelWithCornersSelf ℝ F) F p) v) w₁)
      ((mfderiv% (TauCeti.Manifold.riemannianExp (modelWithCornersSelf ℝ F) F p) v) w₂) =
    inner ℝ w₁ w₂

Sources

• Tau Ceti documentation: TauCeti.Manifold.inner_mfderiv_riemannianExp_radial
• Source of TauCeti.Manifold.inner_mfderiv_riemannianExp_radial in TauCeti/Geometry/Manifold/Riemannian/Geodesic/Gauss/Basic.lean
• Tau Ceti roadmap status: Geodesics, the exponential map, and the Hopf–Rinow theorem

LeanTauCeti.Manifold.inner_mfderiv_riemannianExp_radial · TauCeti.Manifold.inner_mfderiv_riemannianExp_model_space

Uses 2 · Used by 1

Statement usesTauCeti.Manifold.riemannianExp

Proof usesThe Koszul formula

Used byThe Hopf–Rinow theorem

TheoremThe variational characterization of geodesics#

On a boundaryless C^n manifold with 2 ≤ n ≤ ∞, a curve which is C^n near every point of [a, b] is a critical point of the energy between a and b among C^n variations with fixed endpoints exactly when it is a geodesic on the open interval between a and b. For n = ∞: a smooth curve is critical among smooth variations exactly when it is a geodesic.

TauCeti.Manifold.isEnergyCritical_iff_isGeodesicCurveOn.{u_1, u_2, u_3} {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] {γ : ℝ → M}
  {a b : ℝ} {n : ℕ∞} [I.Boundaryless] [IsManifold I 2 M]
  [Bundle.RiemannianBundle fun x => TangentSpace I x] [FiniteDimensional ℝ E]
  [ContMDiffVectorBundle 1 E (TangentSpace I) I]
  [IsContMDiffRiemannianBundle I 1 E fun x => TangentSpace I x] [IsManifold I (↑n) M] (hn : 2 ≤ n)
  (hγ : ∀ t ∈ Set.uIcc a b, ContMDiffAt (modelWithCornersSelf ℝ ℝ) I (↑n) γ t) :
  TauCeti.Manifold.IsEnergyCritical I (↑n) γ a b ↔
    TauCeti.Manifold.IsGeodesicCurveOn I γ (Set.uIoo a b)

Lean

Formalized in Tau Ceti as TauCeti.Manifold.isEnergyCritical_iff_isGeodesicCurveOn.

Sources

• Tau Ceti documentation: TauCeti.Manifold.isEnergyCritical_iff_isGeodesicCurveOn
• Source of TauCeti.Manifold.isEnergyCritical_iff_isGeodesicCurveOn in TauCeti/Geometry/Manifold/Riemannian/Geodesic/FirstVariation.lean
• Tau Ceti roadmap status: Geodesics, the exponential map, and the Hopf–Rinow theorem

LeanTauCeti.Manifold.isEnergyCritical_iff_isGeodesicCurveOn

TheoremThe first variation of the Levi-Civita connection#

Let g_s be a family of smooth nondegenerate metrics, jointly C² in (s, y) at (t, x), with parameter derivative h = ∂ₛ g_s at s = t, and let ∇ˢ be a Levi-Civita connection of g_s for every s. Then for every vector field Y which is differentiable at x and all v, w ∈ T_x M,

2 g_t((∂ₜ∇)_v Y, w) = (∇ᵗ_v h)(Y, w) + (∇ᵗ_Y h)(v, w) - (∇ᵗ_w h)(v, Y),

where (∂ₜ∇)_v Y is the derivative at t of s ↦ ∇ˢ_v Y and ∇ᵗh is the covariant derivative CovariantDerivative.derivBilinearTensor of h along ∇ᵗ.

TauCeti.Manifold.two_mul_apply_deriv_eq_derivBilinearTensor_of_isLeviCivitaConnection.{u_1, u_2,
    u_3}
  {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]
  {h : (x : M) → TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ} {t : ℝ} {x : M}
  [IsManifold I (↑⊤) M] [FiniteDimensional ℝ E]
  {g : ℝ → TauCeti.Manifold.ContMDiffNondegenerateMetric}
  {cov : ℝ → CovariantDerivative I E fun x => TangentSpace I x} {Y : (x : M) → TangentSpace I x}
  (hcov : ∀ (s : ℝ), (g s).IsLeviCivitaConnection (cov s))
  (hg :
    ContMDiffAt ((modelWithCornersSelf ℝ ℝ).prod I)
      (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] E →L[ℝ] ℝ))) 2
      (fun q => ⟨q.2, (g q.1).toContMDiffSection q.2⟩) (t, x))
  (hh :
    ∀ (y : M) (v w : TangentSpace I y),
      HasDerivAt (fun s => (((g s).toContMDiffSection y) v) w) (((h y) v) w) t)
  (hY : (MDiffAt fun x => ⟨x, Y x⟩) x) (v w : TangentSpace I x) :
  2 * (((g t).toContMDiffSection x) (deriv (fun s => (↑(cov s) Y x) v) t)) w =
    ((((cov t).derivBilinearTensor h x) (Y x)) w) v +
        ((((cov t).derivBilinearTensor h x) v) w) (Y x) -
      ((((cov t).derivBilinearTensor h x) v) (Y x)) w

Lean

Formalized in Tau Ceti as TauCeti.Manifold.two_mul_apply_deriv_eq_derivBilinearTensor_of_isLeviCivitaConnection.

Sources

• Tau Ceti documentation: TauCeti.Manifold.two_mul_apply_deriv_eq_derivBilinearTensor_of_isLeviCivitaConnection
• Source of TauCeti.Manifold.two_mul_apply_deriv_eq_derivBilinearTensor_of_isLeviCivitaConnection in TauCeti/Geometry/Manifold/VectorBundle/CovariantDerivative/LeviCivita/Nondegenerate/Variation.lean
• Tau Ceti roadmap status: Geodesics, the exponential map, and the Hopf–Rinow theorem

LeanTauCeti.Manifold.two_mul_apply_deriv_eq_derivBilinearTensor_of_isLeviCivitaConnection

Uses 1

Proof usesThe Koszul formula

DefinitionTauCeti.Manifold.ContMDiffNondegenerateMetric.leviCivitaConnection#

The Levi-Civita connection of a smooth symmetric nondegenerate metric. It is chosen to vanish on vector fields that are not differentiable at the evaluation point.

TauCeti.Manifold.ContMDiffNondegenerateMetric.leviCivitaConnection.{u_1, u_2, u_3} {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]
  [IsManifold I (↑⊤) M] (g : TauCeti.Manifold.ContMDiffNondegenerateMetric)
  [FiniteDimensional ℝ E] : CovariantDerivative I E fun x => TangentSpace I x

Lean

Formalized in Tau Ceti as TauCeti.Manifold.ContMDiffNondegenerateMetric.leviCivitaConnection.

Sources

• Tau Ceti documentation: TauCeti.Manifold.ContMDiffNondegenerateMetric.leviCivitaConnection
• Source of TauCeti.Manifold.ContMDiffNondegenerateMetric.leviCivitaConnection in TauCeti/Geometry/Manifold/VectorBundle/CovariantDerivative/LeviCivita/Nondegenerate/Existence.lean
• Tau Ceti roadmap status: Geodesics, the exponential map, and the Hopf–Rinow theorem

LeanTauCeti.Manifold.ContMDiffNondegenerateMetric.leviCivitaConnection

DefinitionTauCeti.Manifold.riemannianExp#

The Riemannian exponential map at p: the value at time 1 of the maximal geodesic from p with initial velocity v. Outside expDomain I M p it takes the junk value p.

TauCeti.Manifold.riemannianExp.{u_1, u_2, u_3} {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 => TangentSpace I x] [IsManifold I (↑⊤) M]
  [IsContMDiffRiemannianBundle I (↑⊤) E fun x => TangentSpace I x] (p : M) (v : TangentSpace I p) :
  M

Lean

Formalized in Tau Ceti as TauCeti.Manifold.riemannianExp.

Sources

• Tau Ceti documentation: TauCeti.Manifold.riemannianExp
• Source of TauCeti.Manifold.riemannianExp in TauCeti/Geometry/Manifold/Riemannian/Geodesic/Exponential.lean
• Tau Ceti roadmap status: Geodesics, the exponential map, and the Hopf–Rinow theorem

LeanTauCeti.Manifold.riemannianExp

Used by 5

Used byThe Gauss lemma · The Hopf–Rinow theorem · TauCeti.Nil.semidirectProductIsomMulEquiv · Closed normal disc theorem for a closed smooth submanifold · Smooth Riemannian tubular neighbourhood theorem

StructureTauCeti.Manifold.ContMDiffNondegenerateMetricFamily#

A smooth family, parametrized by P, of symmetric nondegenerate real bilinear forms on the tangent bundle of M.

The family is a native smooth section over P × M of the pullback of the tangent bilinear-form bundle of M along the projection P × M → M; its value at (p, x) is a bilinear form on T_x M. As for a single metric, no positivity or signature is imposed.

TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.{u_1, u_2, u_3, u_4, u_5, u_6} {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]
  [IsManifold I (↑⊤) M] {EP : Type u_4} [NormedAddCommGroup EP] [NormedSpace ℝ EP] {HP : Type u_5}
  [TopologicalSpace HP] (IP : ModelWithCorners ℝ EP HP) (P : Type u_6) [TopologicalSpace P]
  [ChartedSpace HP P] : Type (max (max u_1 u_3) u_6)

Lean

Formalized in Tau Ceti as TauCeti.Manifold.ContMDiffNondegenerateMetricFamily.

Sources

• Tau Ceti documentation: TauCeti.Manifold.ContMDiffNondegenerateMetricFamily
• Source of TauCeti.Manifold.ContMDiffNondegenerateMetricFamily in TauCeti/Geometry/Manifold/VectorBundle/NondegenerateMetric/Family.lean
• Tau Ceti roadmap status: Geodesics, the exponential map, and the Hopf–Rinow theorem

LeanTauCeti.Manifold.ContMDiffNondegenerateMetricFamily

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.