Variations of Hamiltonian vector fields

For a constant symplectic form, taking the Hamiltonian vector field commutes with parameter variation: δX_H = X_(δH). Joint C² regularity of the Hamiltonians justifies exchanging the parameter and target derivatives. We also record joint regularity of the vector fields, with one derivative lost. These are the coefficient calculus needed to differentiate inhomogeneous Cauchy–Riemann equations in local coordinates.

The contraction convention is ω(X_H, ·) = dH. See McDuff–Salamon, Introduction to Symplectic Topology, the discussion of Hamiltonian vector fields. Mixed derivatives use TauCeti.hasFDerivAt_spatialFDeriv.

theorem TauCeti.SymplecticForm.contDiffAt_hamiltonianVectorField_uncurry {P : Type u_1} {V : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {K : P → V → ℝ} {p : P} {x : V} {n : WithTop ℕ∞} (hK : ContDiffAt ℝ (n + 1) (Function.uncurry K) (p, x)) : ContDiffAt ℝ n (fun (w : P × V) => ω.hamiltonianVectorField (K w.1) w.2) (p, x)

A jointly C^(n+1) Hamiltonian family has jointly C^n Hamiltonian vector fields.

theorem TauCeti.SymplecticForm.contDiff_hamiltonianVectorField_uncurry {P : Type u_1} {V : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {K : P → V → ℝ} {n : WithTop ℕ∞} (hK : ContDiff ℝ (n + 1) (Function.uncurry K)) : ContDiff ℝ n fun (w : P × V) => ω.hamiltonianVectorField (K w.1) w.2

A jointly C^(n+1) Hamiltonian family has jointly C^n Hamiltonian vector fields. This is the global form of contDiffAt_hamiltonianVectorField_uncurry.

theorem TauCeti.SymplecticForm.continuous_fderiv_hamiltonianVectorField_comp {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {H : ℝ → V → ℝ} (hH : ContDiff ℝ 2 (Function.uncurry H)) {x : ℝ → V} (hx : Continuous x) : Continuous fun (t : ℝ) => fderiv ℝ (ω.hamiltonianVectorField (H t)) (x t)

Along a continuous path x, the linearized Hamiltonian vector fields S_t = dX_{H_t}(x(t)) of a jointly C² Hamiltonian depend continuously on t.

theorem TauCeti.SymplecticForm.fderiv_hamiltonianVectorField_parameter_apply {P : Type u_1} {V : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {K : P → V → ℝ} {p : P} {x : V} (hK : ContDiffAt ℝ 2 (Function.uncurry K) (p, x)) (h : P) : (fderiv ℝ (fun (q : P) => ω.hamiltonianVectorField (K q) x) p) h = ω.hamiltonianVectorField (fun (y : V) => (fderiv ℝ (fun (q : P) => K q y) p) h) x

Differentiating a Hamiltonian vector field in a parameter direction gives the Hamiltonian vector field of the actual parameter derivative of the Hamiltonian.

theorem TauCeti.SymplecticForm.fderiv_hamiltonianVectorField_comp_apply {P : Type u_1} {V : Type u_2} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {K : P → V → ℝ} {u : P → V} {p : P} (hK : ContDiffAt ℝ 2 (Function.uncurry K) (p, u p)) (hu : DifferentiableAt ℝ u p) (h : P) : (fderiv ℝ (fun (q : P) => ω.hamiltonianVectorField (K q) (u q)) p) h = (fderiv ℝ (ω.hamiltonianVectorField (K p)) (u p)) ((fderiv ℝ u p) h) + ω.hamiltonianVectorField (fun (y : V) => (fderiv ℝ (fun (q : P) => K q y) p) h) (u p)

Along a varying target point, the variation is the spatial linearization plus the Hamiltonian vector field of the parameter variation.