Hamiltonian vector fields on symplectic vector spaces

For a constant symplectic form on a finite-dimensional real normed space, the Hamiltonian vector field of H is obtained by inverting contraction with the symplectic form. Our sign convention is ω (X_H x) v = dH(x) v. For ω = dq ∧ dp, this gives the Hamilton equations q' = ∂H/∂p, p' = -∂H/∂q.

The characteristic contraction equation determines the field uniquely. Since dH(X_H) = 0, a differentiable Hamiltonian is constant along every integral curve of X_H (TauCeti.SymplecticForm.apply_eq_of_hasDerivWithinAt_hamiltonianVectorField). The linearization of X_H is infinitesimally symplectic when H is twice continuously differentiable; this is the identity used to show that Hamiltonian flows preserve the symplectic form. A Lipschitz bound ‖X_G(z) - X_G(y₀)‖ ≤ L ‖z - y₀‖ on a ball gives the second-order Taylor bound |G(y) - G(y₀) - dG(y₀)(y - y₀)| ≤ ‖ω‖ L ‖y - y₀‖² there (TauCeti.SymplecticForm.abs_sub_sub_fderiv_le_of_norm_hamiltonianVectorField_sub_le). A compactly supported C² Hamiltonian has a globally Lipschitz Hamiltonian vector field (TauCeti.SymplecticForm.exists_lipschitzWith_hamiltonianVectorField), so its flow is defined for all times.

For an almost complex structure J preserving ω, the field J X_H is the gradient of H for the bilinear form g = ω(·, J ·) (TauCeti.SymplecticForm.Invariant.associatedBilinForm_hamiltonianVectorField).

Along a family of Hamiltonians whose derivatives vary continuously, for instance a jointly C¹ family evaluated along a continuous map, the Hamiltonian vector fields vary continuously.

The Poisson bracket {F, G} = ω(X_F, X_G) of two Hamiltonians is the symplectic pairing of their Hamiltonian vector fields. With the contraction convention it is dF(X_G) = -dG(X_F); it is antisymmetric, vanishes when either argument is constant, and is linear in each argument on Hamiltonians differentiable at the point.

See McDuff--Salamon, Introduction to Symplectic Topology, the discussion of Hamiltonian vector fields and their flows. The construction uses SymplecticForm contraction duality.

noncomputable def TauCeti.SymplecticForm.hamiltonianVectorField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (H : V → ℝ) (x : V) : V

The Hamiltonian vector field, with convention ι_X ω = dH. The derivative is totalized as usual: at a nondifferentiability point this field is zero.

theorem TauCeti.SymplecticForm.hamiltonianVectorField_def {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (H : V → ℝ) (x : V) : ω.hamiltonianVectorField H x = (LinearMap.toContinuousBilinearMap ω.toBilinForm).inverse (fderiv ℝ H x)

The Hamiltonian vector field is inverse contraction applied to the derivative.

theorem TauCeti.SymplecticForm.hamiltonianVectorField_congr_of_eventuallyEq {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {H H' : V → ℝ} {x : V} (h : H =ᶠ[nhds x] H') : ω.hamiltonianVectorField H x = ω.hamiltonianVectorField H' x

The Hamiltonian vector field at x depends only on the germ of the Hamiltonian at x.

@[simp]

theorem TauCeti.SymplecticForm.apply_hamiltonianVectorField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (H : V → ℝ) (x v : V) : (fun (v w : V) => (ω.toBilinForm v) w) (ω.hamiltonianVectorField H x) v = (fderiv ℝ H x) v

Contraction of the Hamiltonian field is the derivative of the Hamiltonian.

theorem TauCeti.SymplecticForm.eq_hamiltonianVectorField_iff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (H : V → ℝ) (x u : V) : u = ω.hamiltonianVectorField H x ↔ ∀ (v : V), (fun (v w : V) => (ω.toBilinForm v) w) u v = (fderiv ℝ H x) v

The contraction equation uniquely characterizes the Hamiltonian vector field.

@[simp]

theorem TauCeti.SymplecticForm.hamiltonianVectorField_eq_zero_iff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (H : V → ℝ) (x : V) : ω.hamiltonianVectorField H x = 0 ↔ fderiv ℝ H x = 0

The Hamiltonian vector field vanishes at x exactly when the derivative fderiv ℝ H x does. Where H is differentiable these are the critical points of H; since fderiv is 0 where H is not differentiable, the field also vanishes at every such point.

@[simp]

theorem TauCeti.SymplecticForm.hamiltonianVectorField_const_mul {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (c : ℝ) (H : V → ℝ) (x : V) : ω.hamiltonianVectorField (fun (y : V) => c * H y) x = c • ω.hamiltonianVectorField H x

The Hamiltonian vector field is homogeneous: X_{c H} = c X_H.

@[simp]

theorem TauCeti.SymplecticForm.fderiv_apply_hamiltonianVectorField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (H : V → ℝ) (x : V) : (fderiv ℝ H x) (ω.hamiltonianVectorField H x) = 0

The Hamiltonian has zero derivative in its own Hamiltonian direction.

theorem TauCeti.SymplecticForm.apply_eq_of_hasDerivWithinAt_hamiltonianVectorField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {H : V → ℝ} {γ : ℝ → V} {s : Set ℝ} (hs' : IsPreconnected s) (hγ : ∀ t ∈ s, HasDerivWithinAt γ (ω.hamiltonianVectorField H (γ t)) s t) (hH : ∀ t ∈ s, DifferentiableAt ℝ H (γ t)) {t₀ t : ℝ} (ht₀ : t₀ ∈ s) (ht : t ∈ s) : H (γ t) = H (γ t₀)

Conservation of energy. A Hamiltonian is constant along every integral curve of its Hamiltonian vector field on a preconnected set of times, provided it is differentiable at every point of the curve; the curve need only have its derivative within the set of times.

theorem TauCeti.SymplecticForm.Invariant.associatedBilinForm_hamiltonianVectorField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hJ : ω.Invariant J) (H : V → ℝ) (x w : V) : ((ω.associatedBilinForm J) (J.toLinearMap (ω.hamiltonianVectorField H x))) w = (fderiv ℝ H x) w

For a J-invariant symplectic form, J X_H(x) is the gradient of H at x for the bilinear form g = ω(·, J ·): g(J X_H(x), w) = dH(x) w.

theorem TauCeti.SymplecticForm.contDiff_hamiltonianVectorField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {H : V → ℝ} {n : WithTop ℕ∞} (hH : ContDiff ℝ (n + 1) H) : ContDiff ℝ n (ω.hamiltonianVectorField H)

A C^(n+1) Hamiltonian has a C^n Hamiltonian vector field.

theorem TauCeti.SymplecticForm.exists_lipschitzWith_hamiltonianVectorField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {H : V → ℝ} (hH : ContDiff ℝ 2 H) (hc : HasCompactSupport H) : ∃ (K : NNReal), LipschitzWith K (ω.hamiltonianVectorField H)

A C² Hamiltonian with compact support has a globally Lipschitz Hamiltonian vector field, so its flow TauCeti.SymplecticForm.hamiltonianFlow is defined for all times.

theorem TauCeti.SymplecticForm.apply_fderiv_hamiltonianVectorField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {H : V → ℝ} {x : V} (hH : DifferentiableAt ℝ (fderiv ℝ H) x) (u v : V) : (fun (v w : V) => (ω.toBilinForm v) w) ((fderiv ℝ (ω.hamiltonianVectorField H) x) u) v = ((fderiv ℝ (fderiv ℝ H) x) u) v

Contracting the linearization of the Hamiltonian vector field gives the Hessian.

theorem TauCeti.SymplecticForm.apply_fderiv_hamiltonianVectorField_add {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {H : V → ℝ} {x : V} (hH : ContDiffAt ℝ 2 H x) (u v : V) : (fun (v w : V) => (ω.toBilinForm v) w) ((fderiv ℝ (ω.hamiltonianVectorField H) x) u) v + (fun (v w : V) => (ω.toBilinForm v) w) u ((fderiv ℝ (ω.hamiltonianVectorField H) x) v) = 0

The linearization of a C² Hamiltonian vector field is infinitesimally symplectic.

@[simp]

theorem TauCeti.SymplecticForm.hamiltonianVectorField_const {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (c : ℝ) : (ω.hamiltonianVectorField fun (x : V) => c) = 0

A constant Hamiltonian has zero Hamiltonian vector field.

@[simp]

theorem TauCeti.SymplecticForm.hamiltonianVectorField_apply_left {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (a x : V) : ω.hamiltonianVectorField (fun (y : V) => (fun (v w : V) => (ω.toBilinForm v) w) a y) x = a

The Hamiltonian vector field of the linear function ω(a, ·) is the constant a.

@[simp]

theorem TauCeti.SymplecticForm.hamiltonianVectorField_add_const {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (H : V → ℝ) (c : ℝ) : (ω.hamiltonianVectorField fun (x : V) => H x + c) = ω.hamiltonianVectorField H

Adding a constant to a Hamiltonian does not change its Hamiltonian vector field. No differentiability is needed: H and H + c are differentiable at the same points.

theorem TauCeti.SymplecticForm.hamiltonianVectorField_const_mul_add_const_mul {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {F G : V → ℝ} {x : V} (hF : DifferentiableAt ℝ F x) (hG : DifferentiableAt ℝ G x) (a b : ℝ) : ω.hamiltonianVectorField (fun (y : V) => a * F y + b * G y) x = a • ω.hamiltonianVectorField F x + b • ω.hamiltonianVectorField G x

The Hamiltonian vector field is linear in Hamiltonians differentiable at the point: X_{aF + bG} = a X_F + b X_G.

theorem TauCeti.SymplecticForm.hamiltonianVectorField_fun_sum {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {ι : Type u_2} {s : Finset ι} {F : ι → V → ℝ} {x : V} (hF : ∀ i ∈ s, DifferentiableAt ℝ (F i) x) : ω.hamiltonianVectorField (fun (y : V) => ∑ i ∈ s, F i y) x = ∑ i ∈ s, ω.hamiltonianVectorField (F i) x

The Hamiltonian vector field is additive on finite sums of Hamiltonians differentiable at the point: X_{∑ Fᵢ} = ∑ X_{Fᵢ}.

@[simp]

theorem TauCeti.SymplecticForm.hamiltonianVectorField_neg {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (H : V → ℝ) (x : V) : ω.hamiltonianVectorField (-H) x = -ω.hamiltonianVectorField H x

The Hamiltonian vector field of -H is -X_H.

theorem TauCeti.SymplecticForm.hamiltonianVectorField_sub {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {F G : V → ℝ} {x : V} (hF : DifferentiableAt ℝ F x) (hG : DifferentiableAt ℝ G x) : ω.hamiltonianVectorField (F - G) x = ω.hamiltonianVectorField F x - ω.hamiltonianVectorField G x

The Hamiltonian vector field of a difference of Hamiltonians differentiable at the point: X_{F - G} = X_F - X_G.

theorem TauCeti.SymplecticForm.abs_sub_sub_fderiv_le_of_norm_hamiltonianVectorField_sub_le {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {G : V → ℝ} (hG : Differentiable ℝ G) {y₀ y : V} {L r : ℝ} (hL : 0 ≤ L) (hX : ∀ z ∈ Metric.closedBall y₀ r, ‖ω.hamiltonianVectorField G z - ω.hamiltonianVectorField G y₀‖ ≤ L * ‖z - y₀‖) (hy : ‖y - y₀‖ ≤ r) : |G y - G y₀ - (fderiv ℝ G y₀) (y - y₀)| ≤ ‖LinearMap.toContinuousBilinearMap ω.toBilinForm‖ * L * ‖y - y₀‖ ^ 2

Second-order Taylor bound for a Hamiltonian. If the Hamiltonian vector field of a differentiable function G satisfies ‖X_G(z) - X_G(y₀)‖ ≤ L ‖z - y₀‖ on the closed ball of radius r about y₀, then |G(y) - G(y₀) - dG(y₀)(y - y₀)| ≤ ‖ω‖ L ‖y - y₀‖² for ‖y - y₀‖ ≤ r, where ‖ω‖ is the operator norm of the form.

theorem TauCeti.SymplecticForm.continuousOn_hamiltonianVectorField_comp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {X : Type u_2} [TopologicalSpace X] {K : X → V → ℝ} {u : X → V} {s : Set X} (ω : SymplecticForm V) (h : ContinuousOn (fun (z : X) => fderiv ℝ (K z) (u z)) s) : ContinuousOn (fun (z : X) => ω.hamiltonianVectorField (K z) (u z)) s

Along a family of Hamiltonians K z and points u z whose derivatives dK_z(u z) vary continuously on a set, the Hamiltonian vector fields X_{K z}(u z) vary continuously on it.

theorem TauCeti.SymplecticForm.continuous_hamiltonianVectorField_comp {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {X : Type u_2} [TopologicalSpace X] {K : X → V → ℝ} {u : X → V} (ω : SymplecticForm V) (h : Continuous fun (z : X) => fderiv ℝ (K z) (u z)) : Continuous fun (z : X) => ω.hamiltonianVectorField (K z) (u z)

Along a family of Hamiltonians K z and points u z whose derivatives dK_z(u z) vary continuously, the Hamiltonian vector fields X_{K z}(u z) vary continuously.

theorem TauCeti.SymplecticForm.continuousOn_uncurry_hamiltonianVectorField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] (ω : SymplecticForm V) {K : W → V → ℝ} {U : Set W} (hK : ContDiffOn ℝ 1 (Function.uncurry K) (U ×ˢ Set.univ)) : ContinuousOn (Function.uncurry fun (z : W) => ω.hamiltonianVectorField (K z)) (U ×ˢ Set.univ)

For a family of Hamiltonians K z that is jointly C¹ over a set U of the parameter space, the Hamiltonian vector field X_{K z}(x) is continuous jointly in the parameter z ∈ U and the point x.

theorem TauCeti.SymplecticForm.continuousOn_hamiltonianVectorField_comp_of_contDiffOn {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] (ω : SymplecticForm V) {K : W → V → ℝ} {u : W → V} {U : Set W} (hu : ContinuousOn u U) (hK : ContDiffOn ℝ 1 (Function.uncurry K) (U ×ˢ Set.univ)) : ContinuousOn (fun (z : W) => ω.hamiltonianVectorField (K z) (u z)) U

For a family of Hamiltonians K z that is jointly C¹ over a set U of the parameter space, the Hamiltonian vector fields X_{K z} evaluated along a map continuous on U vary continuously on U.

theorem TauCeti.SymplecticForm.continuous_uncurry_hamiltonianVectorField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] {W : Type u_2} [NormedAddCommGroup W] [NormedSpace ℝ W] (ω : SymplecticForm V) {K : W → V → ℝ} (hK : ContDiff ℝ 1 (Function.uncurry K)) : Continuous (Function.uncurry fun (z : W) => ω.hamiltonianVectorField (K z))

For a jointly C¹ family of Hamiltonians K z, the Hamiltonian vector field X_{K z}(x) is continuous jointly in the parameter z and the point x.

noncomputable def TauCeti.SymplecticForm.poissonBracket {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (F G : V → ℝ) (x : V) : ℝ

The Poisson bracket {F, G}(x) = ω(X_F x, X_G x) of two Hamiltonians.

theorem TauCeti.SymplecticForm.poissonBracket_def {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (F G : V → ℝ) (x : V) : ω.poissonBracket F G x = (fun (v w : V) => (ω.toBilinForm v) w) (ω.hamiltonianVectorField F x) (ω.hamiltonianVectorField G x)

theorem TauCeti.SymplecticForm.poissonBracket_eq_fderiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (F G : V → ℝ) (x : V) : ω.poissonBracket F G x = (fderiv ℝ F x) (ω.hamiltonianVectorField G x)

The Poisson bracket {F, G} is the derivative of F along the Hamiltonian field of G.

theorem TauCeti.SymplecticForm.poissonBracket_eq_neg_fderiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (F G : V → ℝ) (x : V) : ω.poissonBracket F G x = -(fderiv ℝ G x) (ω.hamiltonianVectorField F x)

The Poisson bracket {F, G} is minus the derivative of G along the Hamiltonian field of F.

theorem TauCeti.SymplecticForm.neg_poissonBracket {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (F G : V → ℝ) (x : V) : -ω.poissonBracket G F x = ω.poissonBracket F G x

The Poisson bracket is antisymmetric.

@[simp]

theorem TauCeti.SymplecticForm.poissonBracket_self {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (F : V → ℝ) (x : V) : ω.poissonBracket F F x = 0

@[simp]

theorem TauCeti.SymplecticForm.poissonBracket_const_left {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (c : ℝ) (G : V → ℝ) (x : V) : ω.poissonBracket (fun (x : V) => c) G x = 0

@[simp]

theorem TauCeti.SymplecticForm.poissonBracket_const_right {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (F : V → ℝ) (c : ℝ) (x : V) : ω.poissonBracket F (fun (x : V) => c) x = 0

@[simp]

theorem TauCeti.SymplecticForm.poissonBracket_add_const_left {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (F : V → ℝ) (c : ℝ) (G : V → ℝ) (x : V) : ω.poissonBracket (fun (y : V) => F y + c) G x = ω.poissonBracket F G x

Adding a constant to the first Hamiltonian does not change the Poisson bracket.

@[simp]

theorem TauCeti.SymplecticForm.poissonBracket_add_const_right {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (F G : V → ℝ) (c : ℝ) (x : V) : ω.poissonBracket F (fun (y : V) => G y + c) x = ω.poissonBracket F G x

Adding a constant to the second Hamiltonian does not change the Poisson bracket.

@[simp]

theorem TauCeti.SymplecticForm.poissonBracket_const_mul_left {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (c : ℝ) (F G : V → ℝ) (x : V) : ω.poissonBracket (fun (y : V) => c * F y) G x = c * ω.poissonBracket F G x

The Poisson bracket is homogeneous in its first argument: {c F, G} = c {F, G}.

@[simp]

theorem TauCeti.SymplecticForm.poissonBracket_const_mul_right {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (F : V → ℝ) (c : ℝ) (G : V → ℝ) (x : V) : ω.poissonBracket F (fun (y : V) => c * G y) x = c * ω.poissonBracket F G x

The Poisson bracket is homogeneous in its second argument: {F, c G} = c {F, G}.

@[simp]

theorem TauCeti.SymplecticForm.poissonBracket_neg_left {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (F G : V → ℝ) (x : V) : ω.poissonBracket (-F) G x = -ω.poissonBracket F G x

Negating the first argument negates the Poisson bracket.

@[simp]

theorem TauCeti.SymplecticForm.poissonBracket_neg_right {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (F G : V → ℝ) (x : V) : ω.poissonBracket F (-G) x = -ω.poissonBracket F G x

Negating the second argument negates the Poisson bracket.

theorem TauCeti.SymplecticForm.poissonBracket_sub_left {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {F F' : V → ℝ} (G : V → ℝ) {x : V} (hF : DifferentiableAt ℝ F x) (hF' : DifferentiableAt ℝ F' x) : ω.poissonBracket (F - F') G x = ω.poissonBracket F G x - ω.poissonBracket F' G x

The Poisson bracket is subtractive in its first argument on Hamiltonians differentiable at the point.

theorem TauCeti.SymplecticForm.poissonBracket_sub_right {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (F : V → ℝ) {G G' : V → ℝ} {x : V} (hG : DifferentiableAt ℝ G x) (hG' : DifferentiableAt ℝ G' x) : ω.poissonBracket F (G - G') x = ω.poissonBracket F G x - ω.poissonBracket F G' x

The Poisson bracket is subtractive in its second argument on Hamiltonians differentiable at the point.

theorem TauCeti.SymplecticForm.poissonBracket_fun_sum_left {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {ι : Type u_2} {s : Finset ι} {F : ι → V → ℝ} (G : V → ℝ) {x : V} (hF : ∀ i ∈ s, DifferentiableAt ℝ (F i) x) : ω.poissonBracket (fun (y : V) => ∑ i ∈ s, F i y) G x = ∑ i ∈ s, ω.poissonBracket (F i) G x

The Poisson bracket is additive in its first argument on finite sums of Hamiltonians differentiable at the point: {∑ Fᵢ, G} = ∑ {Fᵢ, G}.

theorem TauCeti.SymplecticForm.poissonBracket_fun_sum_right {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) {ι : Type u_2} {s : Finset ι} (F : V → ℝ) {G : ι → V → ℝ} {x : V} (hG : ∀ i ∈ s, DifferentiableAt ℝ (G i) x) : ω.poissonBracket F (fun (y : V) => ∑ i ∈ s, G i y) x = ∑ i ∈ s, ω.poissonBracket F (G i) x

The Poisson bracket is additive in its second argument on finite sums of Hamiltonians differentiable at the point: {F, ∑ Gᵢ} = ∑ {F, Gᵢ}.

theorem TauCeti.SymplecticForm.poissonBracket_comb {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) (F G : V → ℝ) (a b c d : ℝ) (x : V) : ω.poissonBracket (fun (y : V) => a * F y + b * G y) (fun (y : V) => c * F y + d * G y) x = (a * d - b * c) * ω.poissonBracket F G x

The Poisson bracket of two combinations a F + b G and c F + d G is a d - b c times {F, G}, with no differentiability hypothesis: where a combination is not differentiable its Hamiltonian field is zero, and then {F, G} or the bracket of the combinations vanishes too.