Documentation

TauCeti.Geometry.Symplectic.Cotangent.Bundle.Cogeodesic

The Reeb flow of the unit cosphere bundle is the cogeodesic flow #

Let M be a Riemannian manifold without boundary, with cotangent bundle T*M, Liouville form λ = p dq and canonical symplectic form ω = -dλ. The kinetic energy of a covector is K(q, p) = ‖p‖² / 2 (TauCeti.CotangentBundle.kineticEnergy), where ‖p‖ is the norm of p for the metric. Its Hamiltonian vector field X_K, with ι_(X_K) ω = dK, generates the cogeodesic flow: in canonical coordinates it reads dq/dt = p♯, dp/dt = -∂_q K.

The unit cosphere bundle S*M = {‖p‖ = 1} is the level K = 1/2. It carries the two contact forms α_g = λ|S*M and α_b = -λ|S*M, which define opposite coorientations of the same contact distribution. This file identifies their Reeb vector fields with the cogeodesic field:

The proof applies TauCeti.SmoothTwoForm.IsNondegenerate.mfderiv_reebVectorField_mpullback to θ = λ and the energy K. Two facts about K enter. Its differential is ‖p‖ d‖p‖ (TauCeti.CotangentBundle.mvfderiv_kineticEnergy), so on S*M its kernel is the tangent space of S*M. And K is homogeneous of degree two in the fibres, so the Euler field Z = p ∂_p satisfies dK(Z) = 2K = ‖p‖² (TauCeti.CotangentBundle.mvfderiv_kineticEnergy_vectorBundleEulerField). Since ι_Z ω = -λ, this gives λ(X_K) = ω(X_K, Z) = dK(Z) = ‖p‖² (TauCeti.CotangentBundle.liouvilleForm_hamiltonianVectorField_kineticEnergy), which is 1 on S*M: the Reeb normalization α_g(R) = 1 holds for X_K itself, with no rescaling.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.CotangentBundle.kineticEnergy {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (z : CotangentBundle I M) :
ℝ

The kinetic energy K(q, p) = ‖p‖² / 2 of a covector, for the norm of covectors induced by the Riemannian metric. Its Hamiltonian flow for the canonical symplectic form is the cogeodesic flow.

Instances For
    source
    @[simp]
    theorem TauCeti.CotangentBundle.kineticEnergy_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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (z : CotangentBundle I M) :
    kineticEnergy I M z = ‖z.snd‖ ^ 2 / 2
    source
    theorem TauCeti.CotangentBundle.contMDiff_kineticEnergy {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] {n : WithTop ℕ∞} [IsManifold I 1 M] [IsManifold I (n + 1) M] [IsContMDiffRiemannianBundle I n E fun (x : M) => TangentSpace I x] :
    ContMDiff (I.prod (modelWithCornersSelf ℝ (E →L[ℝ] ℝ))) (modelWithCornersSelf ℝ ℝ) n (kineticEnergy I M)

    The kinetic energy is as smooth as the metric.

    source
    theorem TauCeti.CotangentBundle.mvfderiv_kineticEnergy {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] {z : CotangentBundle I M} (hz : z.snd ≠ 0) :
    d% (kineticEnergy I M) z = ‖z.snd‖ • (d% fun (z : CotangentBundle I M) => ‖z.snd‖) z

    The differential of the kinetic energy. Off the zero section, dK = ‖p‖ d‖p‖.

    source
    theorem TauCeti.CotangentBundle.mvfderiv_kineticEnergy_vectorBundleEulerField {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I 2 M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (z : CotangentBundle I M) :
    (d% (kineticEnergy I M) z) (vectorBundleEulerField I z) = ‖z.snd‖ ^ 2

    Euler's identity for the kinetic energy. The kinetic energy is homogeneous of degree two in the fibres, so the Euler vector field Z = p ∂_p satisfies dK(Z) = 2K = ‖p‖².

    source
    theorem TauCeti.CotangentBundle.liouvilleForm_hamiltonianVectorField_kineticEnergy {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I 1 E fun (x : M) => TangentSpace I x] (z : CotangentBundle I M) :
    (↑(liouvilleForm I M) z) ![(symplecticForm I M).hamiltonianVectorField (kineticEnergy I M) z] = ‖z.snd‖ ^ 2

    The Liouville form on the cogeodesic field. The Liouville form takes the value λ(X_K) = ‖p‖² = 2K on the Hamiltonian vector field of the kinetic energy: in coordinates, p(dq/dt) = p(p♯) = ‖p‖².

    source
    theorem TauCeti.CotangentBundle.mfderiv_coe_reebVectorField_cosphereBundle {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [I.Boundaryless] (z : ↑(cosphereBundle I M)) :
    (mfderiv% Subtype.val z) (((SmoothForm.mpullback Subtype.val ⋯) (liouvilleForm I M)).reebVectorField z) = (symplecticForm I M).hamiltonianVectorField (kineticEnergy I M) ↑z

    The Reeb field of λ|S*M is the cogeodesic field. The differential of the inclusion of the unit cosphere bundle sends the Reeb vector field of the contact form α_g = λ|S*M to the Hamiltonian vector field of the kinetic energy.

    source
    theorem TauCeti.CotangentBundle.mfderiv_coe_reebVectorField_neg_cosphereBundle {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [I.Boundaryless] (z : ↑(cosphereBundle I M)) :
    (mfderiv% Subtype.val z) (((SmoothForm.mpullback Subtype.val ⋯) (-liouvilleForm I M)).reebVectorField z) = -(symplecticForm I M).hamiltonianVectorField (kineticEnergy I M) ↑z

    The Reeb field of -λ|S*M is the reversed cogeodesic field. The differential of the inclusion of the unit cosphere bundle sends the Reeb vector field of the contact form α_b = -λ|S*M to minus the Hamiltonian vector field of the kinetic energy.

    source
    theorem TauCeti.CotangentBundle.coe_flowOf_reebVectorField_cosphereBundle {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] [IsContMDiffRiemannianBundle I (↑⊤) E fun (x : M) => TangentSpace I x] [I.Boundaryless] [T2Space M] {t : ℝ} {z : ↑(cosphereBundle I M)} (ht : (t, z) ∈ flowDomain ((SmoothForm.mpullback Subtype.val ⋯) (liouvilleForm I M)).reebVectorField) :
    ↑(flowOf ((SmoothForm.mpullback Subtype.val ⋯) (liouvilleForm I M)).reebVectorField t z) = flowOf ((symplecticForm I M).hamiltonianVectorField (kineticEnergy I M)) t ↑z

    The Reeb flow of λ|S*M is the cogeodesic flow. Wherever the Reeb flow of the contact form α_g = λ|S*M is defined, the inclusion of the unit cosphere bundle carries it to the Hamiltonian flow of the kinetic energy.