Liouville vector fields

A vector field Z on a manifold carrying a two-form ω is a Liouville vector field when L_Z ω = ω. For a closed form, Cartan's formula L_Z ω = ι_Z dω + d (ι_Z ω) shows that this holds exactly when ι_Z ω is a primitive of ω (TauCeti.isLiouvilleVectorField_iff_mextDeriv_interior_eq). In particular, if λ is a primitive of ω and ι_Z ω = λ, then Z is a Liouville vector field (TauCeti.isLiouvilleVectorField_mextDeriv_of_interior_eq). This is the Liouville field of the primitive λ, the kind of vector field used to define Liouville domains and hypersurfaces of contact type. On a normed space the same characterization is stated with the flat exterior derivative (TauCeti.isLiouvilleVectorField_extDeriv_iff).

The converse fails for a fixed primitive: a Liouville vector field Z only determines its own primitive ι_Z ω, which need not be the given one. On the plane, with λ = x dy and ω = dλ = dx ∧ dy, the field Z = x ∂_x + ∂_y is a Liouville vector field, but ι_Z ω = λ - dx (Prod.isLiouvilleVectorField_extDeriv_realPlaneXDy, Prod.curryLeft_extDeriv_realPlaneXDy). In cotangent notation, with (x, y) = (p, q), this is λ = p dq and Z = p ∂_p + ∂_q.

On the linear cotangent space, with the tautological form λ = p dq and the canonical symplectic form -dλ, the radial field p ∂_p is the Liouville field of the primitive -λ (TauCeti.isLiouvilleVectorField_cotangentLiouvilleField).

Main declarations

• TauCeti.IsLiouvilleVectorField: the property L_Z ω = ω.
• TauCeti.isLiouvilleVectorField_iff_mextDeriv_interior_eq: for a closed form, Z is a Liouville vector field exactly when d (ι_Z ω) = ω.
• TauCeti.isLiouvilleVectorField_mextDeriv_of_interior_eq: ι_Z dλ = λ implies L_Z dλ = dλ.
• TauCeti.mlieDerivForm_eq_self_of_interior_eq: ι_Z dλ = λ implies L_Z λ = λ.
• TauCeti.isLiouvilleVectorField_extDeriv_iff: the characterization on a normed space.
• TauCeti.isLiouvilleVectorField_cotangentLiouvilleField: the radial field of the linear cotangent space.
• Prod.isLiouvilleVectorField_extDeriv_realPlaneXDy, Prod.curryLeft_extDeriv_realPlaneXDy_ne: a Liouville vector field of d(x dy) that is not the Liouville field of x dy.

References

• D. McDuff, D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Chapter 3 (Liouville vector fields and hypersurfaces of contact type).
• J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Floer homology with DG coefficients. Applications to cotangent bundles, arXiv:2404.07953, §1.2.

def TauCeti.IsLiouvilleVectorField {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] (ω : RoughForm I M ℝ 2) (Z : (x : M) → TangentSpace I x) : Prop

A vector field Z is a Liouville vector field for a two-form ω when the Lie derivative of ω along Z is ω itself, L_Z ω = ω.

theorem TauCeti.isLiouvilleVectorField_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] {ω : RoughForm I M ℝ 2} {Z : (x : M) → TangentSpace I x} : IsLiouvilleVectorField ω Z ↔ mlieDerivForm Z ω = ω

The defining characterization of a Liouville vector field.

theorem TauCeti.isLiouvilleVectorField_iff_mextDeriv_interior_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {ω : RoughForm I M ℝ 2} {Z : (x : M) → TangentSpace I x} (hω : MDiff fun (y : M) => ⟨y, ω y⟩) (hZ : MDiff fun (y : M) => ⟨y, Z y⟩) (hdω : mextDeriv ω = 0) : IsLiouvilleVectorField ω Z ↔ mextDeriv (RoughForm.interior Z ω) = ω

For a differentiable closed two-form ω and a differentiable vector field Z, Z is a Liouville vector field exactly when ι_Z ω is a primitive of ω.

theorem TauCeti.isLiouvilleVectorField_mextDeriv_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] {α : RoughForm I M ℝ 1} {Z : (x : M) → TangentSpace I x} (hα : IsSmoothForm I 2 α) (hZ : MDiff fun (y : M) => ⟨y, Z y⟩) : IsLiouvilleVectorField (mextDeriv α) Z ↔ mextDeriv (RoughForm.interior Z (mextDeriv α)) = mextDeriv α

For a C² one-form α and a differentiable vector field Z, Z is a Liouville vector field of dα exactly when ι_Z dα is again a primitive of dα.

theorem TauCeti.isLiouvilleVectorField_mextDeriv_of_interior_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 2 M] {α : RoughForm I M ℝ 1} {Z : (x : M) → TangentSpace I x} (hα : IsSmoothForm I 2 α) (hZ : MDiff fun (y : M) => ⟨y, Z y⟩) (h : RoughForm.interior Z (mextDeriv α) = α) : IsLiouvilleVectorField (mextDeriv α) Z

The Liouville field of a primitive. If α is a C² one-form and the differentiable vector field Z satisfies ι_Z dα = α, then Z is a Liouville vector field of dα.

theorem TauCeti.mlieDerivForm_eq_self_of_interior_eq {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] {α : RoughForm I M ℝ 1} {Z : (x : M) → TangentSpace I x} (hα : MDiff fun (y : M) => ⟨y, α y⟩) (hZ : MDiff fun (y : M) => ⟨y, Z y⟩) (h : RoughForm.interior Z (mextDeriv α) = α) : mlieDerivForm Z α = α

A primitive has Lie derivative equal to itself along its Liouville field. If the differentiable vector field Z satisfies ι_Z dλ = λ for a differentiable one-form λ, then L_Z λ = λ: by Cartan's formula L_Z λ = ι_Z dλ + d (ι_Z λ), and ι_Z λ = dλ (Z, Z) = 0.

Normed spaces

theorem TauCeti.isLiouvilleVectorField_extDeriv_iff {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {α : E → E [⋀^Fin 1]→L[ℝ] ℝ} {Z : E → E} (hα : ContDiff ℝ 2 α) (hZ : Differentiable ℝ Z) : IsLiouvilleVectorField (extDeriv α) Z ↔ (extDeriv fun (x : E) => (extDeriv α x).curryLeft (Z x)) = extDeriv α

On a normed space, for a C² one-form α and a differentiable vector field Z, Z is a Liouville vector field of dα exactly when the one-form x ↦ ι_{Z x} dα_x is again a primitive of dα.

The radial field of the linear cotangent space

theorem TauCeti.isLiouvilleVectorField_cotangentLiouvilleField {V : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] : IsLiouvilleVectorField (extDeriv (-cotangentLiouvilleForm)) ⇑cotangentLiouvilleField

On the linear cotangent space, the radial field p ∂_p is a Liouville vector field of the canonical symplectic form d(-λ) = -dλ, as the Liouville field of its primitive -λ.

A Liouville vector field that is not the Liouville field of a given primitive

theorem Prod.isLiouvilleVectorField_extDeriv_realPlaneXDy : TauCeti.IsLiouvilleVectorField (extDeriv realPlaneXDy) fun (p : ℝ × ℝ) => (p.1, 1)

On the plane, the vector field Z = x ∂_x + ∂_y is a Liouville vector field of d(x dy) = dx ∧ dy, although it is not the Liouville field of the primitive x dy (Prod.curryLeft_extDeriv_realPlaneXDy_ne): it is the Liouville field of the primitive x dy - dx.