The Liouville flow rescales the form and its primitive

Let Z be a complete C² Liouville vector field of a two-form σ, L_Z σ = σ, with flow ψ. Then ψₜ^* σ = e^t σ for every time t (TauCeti.IsLiouvilleVectorField.mpullback_globalFlow_eq_exp_smul): the flow rescales σ, and is conformally symplectic when σ is symplectic. If moreover α is a primitive of σ whose Liouville field is Z, dα = σ and ι_Z σ = α, then also ψₜ^* α = e^t α (TauCeti.mpullback_globalFlow_eq_exp_smul_of_interior_eq): the flow rescales the primitive, so that it is an exact conformal symplectomorphism when σ is symplectic.

Near a hypersurface Σ of contact type, such as the boundary of a Liouville domain, the flow sweeps out a family of hypersurfaces ψₜ(Σ) whose characteristic foliations are conjugate under ψₜ, because ψₜ multiplies the symplectic form by a constant; this is how almost existence of closed characteristics near Σ yields closed characteristics on Σ itself. On the cylindrical end of the completion of a Liouville domain, swept out from the boundary by the flow, the identity ψₜ^* α = e^t α says that α has the form e^t α|_Σ of a symplectization.

Without completeness the same identities hold wherever the maximal flow φ of Z is defined: (φₜ^* σ)ₓ = e^t σₓ and (φₜ^* α)ₓ = e^t αₓ whenever φₜ(x) is defined (TauCeti.IsLiouvilleVectorField.mpullback_flowOf_apply_eq_exp_smul, TauCeti.mpullback_flowOf_apply_eq_exp_smul_of_interior_eq). These describe the Liouville flow near a hypersurface of contact type when the Liouville field is not complete.

The local identities integrate infinitesimal ones along the flow (TauCeti.mpullback_flowOf_apply_eq_exp_integral_smul): L_Z σ = σ by definition, and L_Z α = α by Cartan's formula (TauCeti.mlieDerivForm_eq_self_of_interior_eq). The identities for a complete field are the case where the maximal flow is defined everywhere.

Main results

• TauCeti.IsLiouvilleVectorField.mpullback_globalFlow_eq_exp_smul: ψₜ^* σ = e^t σ.
• TauCeti.mpullback_globalFlow_eq_exp_smul_of_interior_eq: ψₜ^* α = e^t α.
• TauCeti.IsLiouvilleVectorField.mpullback_flowOf_apply_eq_exp_smul, TauCeti.mpullback_flowOf_apply_eq_exp_smul_of_interior_eq: the same along the maximal flow, wherever it is defined.

References

• D. McDuff, D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 3.5 (Liouville vector fields and hypersurfaces of contact type).
• K. Cieliebak, Y. Eliashberg, From Stein to Weinstein and Back, AMS Colloquium Publications 59, 2012, Section 11.1 (Liouville domains and their completions).

theorem TauCeti.IsLiouvilleVectorField.mpullback_flowOf_apply_eq_exp_smul {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] {Z : (x : M) → TangentSpace I x} [FiniteDimensional ℝ E] [I.Boundaryless] [T2Space M] (hZ : ContMDiff I I.tangent 2 fun (y : M) => ⟨y, Z y⟩) {σ : RoughForm I M ℝ 2} (hσ : MDiff fun (y : M) => ⟨y, σ y⟩) (hZσ : IsLiouvilleVectorField σ Z) {t : ℝ} {x : M} (hx : (t, x) ∈ flowDomain Z) : mpullback I I (flowOf Z t) σ x = Real.exp t • σ x

The local Liouville flow rescales the two-form. Wherever the maximal flow φ of a C² Liouville vector field Z of a differentiable two-form σ, L_Z σ = σ, is defined at (t, x), (φₜ^* σ)ₓ = e^t σₓ. No completeness of Z is needed.

theorem TauCeti.mpullback_flowOf_apply_eq_exp_smul_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] {Z : (x : M) → TangentSpace I x} [FiniteDimensional ℝ E] [I.Boundaryless] [T2Space M] (hZ : ContMDiff I I.tangent 2 fun (y : M) => ⟨y, Z y⟩) {α : RoughForm I M ℝ 1} {σ : RoughForm I M ℝ 2} (hα : MDiff fun (y : M) => ⟨y, α y⟩) (hdα : mextDeriv α = σ) (hZα : RoughForm.interior Z σ = α) {t : ℝ} {x : M} (hx : (t, x) ∈ flowDomain Z) : mpullback I I (flowOf Z t) α x = Real.exp t • α x

The local Liouville flow rescales the primitive. If α is a differentiable primitive of the two-form σ, and the C² vector field Z is its Liouville field, ι_Z σ = α, then wherever the maximal flow φ of Z is defined at (t, x), (φₜ^* α)ₓ = e^t αₓ. No completeness of Z is needed.

theorem TauCeti.IsLiouvilleVectorField.mpullback_globalFlow_eq_exp_smul {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] {Z : (x : M) → TangentSpace I x} [FiniteDimensional ℝ E] [I.Boundaryless] [T2Space M] (hc : IsCompleteVectorField Z) (hZ : ContMDiff I I.tangent 2 fun (y : M) => ⟨y, Z y⟩) {σ : RoughForm I M ℝ 2} (hσ : MDiff fun (y : M) => ⟨y, σ y⟩) (hZσ : IsLiouvilleVectorField σ Z) (t : ℝ) : mpullback I I ((globalFlow Z ⋯ hc).toFun t) σ = Real.exp t • σ

The Liouville flow rescales the two-form. The flow ψ of a complete C² Liouville vector field Z of a differentiable two-form σ, L_Z σ = σ, satisfies ψₜ^* σ = e^t σ; when σ is symplectic, the flow is conformally symplectic.

theorem TauCeti.mpullback_globalFlow_eq_exp_smul_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] {Z : (x : M) → TangentSpace I x} [FiniteDimensional ℝ E] [I.Boundaryless] [T2Space M] (hc : IsCompleteVectorField Z) (hZ : ContMDiff I I.tangent 2 fun (y : M) => ⟨y, Z y⟩) {α : RoughForm I M ℝ 1} {σ : RoughForm I M ℝ 2} (hα : MDiff fun (y : M) => ⟨y, α y⟩) (hdα : mextDeriv α = σ) (hZα : RoughForm.interior Z σ = α) (t : ℝ) : mpullback I I ((globalFlow Z ⋯ hc).toFun t) α = Real.exp t • α

The Liouville flow rescales the primitive. If α is a differentiable primitive of the two-form σ, and the complete C² vector field Z is its Liouville field, ι_Z σ = α, then the flow ψ of Z satisfies ψₜ^* α = e^t α; when σ is symplectic, the flow is exact conformally symplectic.