Documentation

TauCeti.Geometry.Symplectic.Hamiltonian.Flow

Autonomous Hamiltonian flows #

A globally Lipschitz Hamiltonian vector field on a finite-dimensional symplectic vector space has a canonical global flow. This applies in particular to every C² Hamiltonian with compact support (TauCeti.SymplecticForm.exists_lipschitzWith_hamiltonianVectorField). The Hamiltonian is constant along each orbit. For a C² Hamiltonian, every time map preserves the symplectic form on tangent vectors: differentiating the pairing of two variations and using symmetry of the Hessian gives zero.

The construction and variational equation reuse TauCeti.flowOfLipschitz. See McDuff--Salamon, Introduction to Symplectic Topology, Hamiltonian flows.

source
noncomputable def TauCeti.SymplecticForm.hamiltonianFlow {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (H : V → ℝ) {K : NNReal} (hX : LipschitzWith K (ω.hamiltonianVectorField H)) :
Flow ℝ V

The autonomous Hamiltonian flow, defined for all real times when its vector field is globally Lipschitz.

Instances For
    source
    theorem TauCeti.SymplecticForm.hamiltonianFlow_eq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (H : V → ℝ) {K : NNReal} (hX : LipschitzWith K (ω.hamiltonianVectorField H)) :
    ω.hamiltonianFlow H hX = flowOfLipschitz (ω.hamiltonianVectorField H) hX

    The Hamiltonian flow is the canonical Lipschitz flow of its Hamiltonian vector field.

    source
    theorem TauCeti.SymplecticForm.hasDerivAt_hamiltonianFlow {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (H : V → ℝ) {K : NNReal} (hX : LipschitzWith K (ω.hamiltonianVectorField H)) (x : V) (t : ℝ) :
    HasDerivAt (fun (s : ℝ) => (ω.hamiltonianFlow H hX).toFun s x) (ω.hamiltonianVectorField H ((ω.hamiltonianFlow H hX).toFun t x)) t

    Hamiltonian orbits solve Hamilton's differential equation.

    source
    theorem TauCeti.SymplecticForm.hamiltonianFlow_conserves {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (H : V → ℝ) {K : NNReal} (hX : LipschitzWith K (ω.hamiltonianVectorField H)) (hH : Differentiable ℝ H) (t : ℝ) (x : V) :
    H ((ω.hamiltonianFlow H hX).toFun t x) = H x

    An autonomous differentiable Hamiltonian is conserved by its flow.

    source
    theorem TauCeti.SymplecticForm.contDiff_hamiltonianFlow_apply {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (H : V → ℝ) {K : NNReal} (n : ℕ) (hX : LipschitzWith K (ω.hamiltonianVectorField H)) (hH : ContDiff ℝ (↑n + 2) H) (t : ℝ) :
    ContDiff ℝ (↑n + 1) ((ω.hamiltonianFlow H hX).toFun t)

    The time maps of a globally Lipschitz Hamiltonian flow are C^(n+1) when the Hamiltonian is C^(n+2).

    source
    @[simp]
    theorem TauCeti.SymplecticForm.apply_fderiv_hamiltonianFlow {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (H : V → ℝ) {K : NNReal} (hX : LipschitzWith K (ω.hamiltonianVectorField H)) (hH : ContDiff ℝ 2 H) (t : ℝ) (x u v : V) :
    (fun (v w : V) => (ω.toBilinForm v) w) ((fderiv ℝ ((ω.hamiltonianFlow H hX).toFun t) x) u) ((fderiv ℝ ((ω.hamiltonianFlow H hX).toFun t) x) v) = (fun (v w : V) => (ω.toBilinForm v) w) u v

    Each time map of a C² Hamiltonian flow preserves the symplectic form on tangent vectors. No nondegeneracy of the Hessian is required.