Contact Hamiltonian vector fields #
Let α be a one-form on a manifold M, with Reeb vector field R_α. A vector field X is a
contact Hamiltonian vector field of a function f : M → ℝ when
α(X) = f, ι_X dα = (R_α f) α - df
(TauCeti.SmoothForm.IsContactHamiltonianVectorField). With these sign conventions, Cartan's
formula L_X α = ι_X dα + d(ι_X α) turns the two equations into
L_X α = (R_α f) α
(TauCeti.SmoothForm.IsContactHamiltonianVectorField.mlieDerivForm_eq), with no hypothesis on
α beyond smoothness. This is the infinitesimal form of the statement that the flow of X
rescales α by positive functions, so that it preserves the contact distribution ξ = ker α
together with its coorientation. Accordingly, the bracket of X with any vector field tangent to
ξ is again tangent to ξ
(TauCeti.SmoothForm.IsContactHamiltonianVectorField.mlieBracket_mem_kerDistribution).
Conversely, for a contact form, a differentiable vector field X with L_X α = g α for some
function g is the contact Hamiltonian vector field of α(X)
(TauCeti.SmoothForm.IsContactForm.isContactHamiltonianVectorField_iff_mlieDerivForm,
TauCeti.SmoothForm.IsContactForm.eq_contactHamiltonianVectorField_of_mlieDerivForm_eq_smul); then
necessarily g = R_α(α(X))
(TauCeti.SmoothForm.IsContactForm.eq_mvfderiv_reebVectorField_of_mlieDerivForm_apply_eq_smul).
So contact vector fields are determined by their Hamiltonians.
The two defining equations together say that the contact flat map v ↦ ι_v dα + α(v) α of
TauCeti.SmoothForm.contactFlat sends X to the covector (f + R_α f) α - df. For a contact
form on a finite-dimensional manifold the contact flat maps are invertible, so the contact
Hamiltonian vector field X_f (TauCeti.SmoothForm.contactHamiltonianVectorField), defined as
the inverse contact flat map applied to this covector, is the unique contact Hamiltonian vector
field of f (TauCeti.SmoothForm.IsContactForm.isContactHamiltonianVectorField_iff_eq). The
Hamiltonian of the Reeb vector field is the constant 1: more generally X_c = c R_α for a
constant c (TauCeti.SmoothForm.IsContactForm.contactHamiltonianVectorField_const). The
contact Hamiltonian vector field of a C^(n+1) function is a C^n vector field
(TauCeti.SmoothForm.IsContactForm.contMDiff_contactHamiltonianVectorField), as is its Reeb
derivative R_α f (TauCeti.SmoothForm.IsContactForm.contMDiff_mvfderiv_reebVectorField).
Unlike a symplectic Hamiltonian, a contact Hamiltonian need not be conserved: along X_f it
changes by df(X_f) = (R_α f) f, so it is conserved exactly where (R_α f) f = 0
(TauCeti.SmoothForm.IsContactHamiltonianVectorField.mvfderiv_apply_self).
Since α(X) = f, a contact Hamiltonian vector field X of f is tangent to ξ exactly where f
vanishes (TauCeti.SmoothForm.IsContactHamiltonianVectorField.mem_kerDistribution_iff).
Main declarations #
TauCeti.SmoothForm.IsContactHamiltonianVectorField: the defining equations.TauCeti.SmoothForm.contactHamiltonianVectorField: the contact Hamiltonian vector fieldX_f.TauCeti.SmoothForm.IsContactForm.isContactHamiltonianVectorField_iff_eq: existence and uniqueness.TauCeti.SmoothForm.IsContactHamiltonianVectorField.contMDiff: a contact Hamiltonian vector field of aC^(n+1)function isC^n.TauCeti.SmoothForm.IsContactHamiltonianVectorField.mlieDerivForm_eq:L_X α = (R_α f) α.TauCeti.SmoothForm.IsContactHamiltonianVectorField.mlieBracket_mem_kerDistribution: infinitesimal preservation of the contact distribution.TauCeti.SmoothForm.IsContactForm.isContactHamiltonianVectorField_iff_mlieDerivForm,TauCeti.SmoothForm.IsContactForm.eq_contactHamiltonianVectorField_of_mlieDerivForm_eq_smul: contact vector fields are the contact Hamiltonian vector fields of their Hamiltonians.TauCeti.SmoothForm.IsContactForm.eq_mvfderiv_reebVectorField_of_mlieDerivForm_apply_eq_smul: the multiplierginL_X α = g αisR_α(α(X)).
The construction of X_f, its linearity lemmas and its regularity proof are adapted from
TauCeti.SmoothTwoForm.hamiltonianVectorField in
TauCeti.Geometry.Symplectic.Hamiltonian.Manifold.
References #
- Hansjörg Geiges, An Introduction to Contact Topology, Cambridge Studies in Advanced Mathematics 109 (2008), Section 2.3.
The defining equations #
A vector field X is a contact Hamiltonian vector field of f for the one-form α when
α(X) = f and ι_X dα = (R_α f) α - df, where R_α is the Reeb vector field of α.
Instances For
The defining characterization of a contact Hamiltonian vector field.
A contact Hamiltonian vector field of f takes the value f under α.
The contraction of dα with a contact Hamiltonian vector field of f is (R_α f) α - df.
A contact Hamiltonian vector field of f lies in the contact distribution exactly where f
vanishes.
A contact Hamiltonian need not be conserved: along its contact Hamiltonian vector field it
changes by df(X) = (R_α f) f.
Cartan's formula for a contact Hamiltonian vector field at a point where it is
differentiable: L_X α = (R_α f) α.
The derivative of α(W) along a contact Hamiltonian vector field X of f, from
L_X α = (R_α f) α: X(α(W)) - α([X, W]) = (R_α f) α(W).
Cartan's formula for a contact Hamiltonian vector field: a differentiable contact
Hamiltonian vector field X of f satisfies L_X α = (R_α f) α.
A contact Hamiltonian vector field preserves the contact distribution infinitesimally: its
bracket at x with a vector field tangent to ξ = ker α near x is again tangent to ξ.
The contact Hamiltonian vector field #
The contact Hamiltonian vector field X_f of a function f: the inverse contact flat map
applied to the covector (f + R_α f) α - df. For a contact form on a finite-dimensional manifold
it is the unique contact Hamiltonian vector field of f
(TauCeti.SmoothForm.IsContactForm.isContactHamiltonianVectorField_iff_eq); the inverse is
ContinuousLinearMap.inverse, so the field vanishes at points where the contact flat map is not
invertible.
Instances For
The contact Hamiltonian vector field unfolds as the inverse contact flat map applied to
(f + R_α f) α - df.
The contact Hamiltonian vector field of the zero function vanishes.
The contact Hamiltonian vector field is additive on differentiable functions.
The contact Hamiltonian vector field of -f is the opposite of that of f.
The contact Hamiltonian vector field commutes with multiplication by a real constant.
Contact forms #
A vector field is a contact Hamiltonian vector field of f exactly when the contact flat map
sends it to the covector (f + R_α f) α - df.
The contact flat map sends the contact Hamiltonian vector field of f to
(f + R_α f) α - df.
The contact Hamiltonian vector field of f is a contact Hamiltonian vector field of f.
A contact form takes the value f on the contact Hamiltonian vector field of f.
Contraction of dα with the contact Hamiltonian vector field of f is
(R_α f) α - df.
Existence and uniqueness of contact Hamiltonian vector fields. For a contact form on a
finite-dimensional manifold, X_f is the only contact Hamiltonian vector field of f.
A contact Hamiltonian vector field is characterized by its value under α and its
contraction equation tested only on the contact hyperplanes.
The contact Hamiltonian vector field of a constant c is c R_α.
The Reeb vector field is the contact Hamiltonian vector field of the constant 1.
For a contact form on a finite-dimensional manifold, the derivative R_α f of a C^(n+1)
function along the Reeb vector field is C^n, for n ≤ ∞.
For a contact form on a finite-dimensional manifold, the derivative R_α f of a C² function
along the Reeb vector field is differentiable.
Regularity of contact Hamiltonian vector fields. For a contact form on a
finite-dimensional manifold, the contact Hamiltonian vector field of a C^(n+1) function is a
C^n vector field, for n ≤ ∞.
Regularity of contact Hamiltonian vector fields. For a contact form on a
finite-dimensional manifold, every contact Hamiltonian vector field of a C^(n+1) function is a
C^n vector field, for n ≤ ∞.
The contact Hamiltonian vector field of a C² function is differentiable.
The multiplier of a contact vector field. For a contact form α and a vector field X
differentiable at x with α(X) = f, if L_X α = c α at x, then c = R_α f at x.
Contact vector fields are contact Hamiltonian vector fields. For a contact form α and a
differentiable vector field X, X is a contact Hamiltonian vector field of f exactly when
α(X) = f and the Lie derivative L_X α is a multiple g α of α by some function g. The
multiplier is then g = R_α f
(TauCeti.SmoothForm.IsContactForm.eq_mvfderiv_reebVectorField_of_mlieDerivForm_apply_eq_smul).
A contact vector field is the contact Hamiltonian vector field of its Hamiltonian. For a
contact form α, a differentiable vector field X whose Lie derivative L_X α is a multiple of
α is the contact Hamiltonian vector field of α(X).