poisson_bracket_anticomm

theoremverified

For any two scalar functions f and g on the phase space E × E and any phase-space point qp, the Poisson bracket satisfies {f, g}(qp) = -{g, f}(qp).

Statement

theorem poisson_bracket_anticomm {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    (f g : E × E → ℝ) (qp : E × E) :
    poisson_bracket f g qp = - poisson_bracket g f qp

Source

Arnold, Mathematical Methods of Classical Mechanics, §38; Goldstein, Poole & Safko, Classical Mechanics (3rd ed.), §9.4

Verified

11 Sep 2026

Axioms

Classical.choiceQuot.soundpropext

Built on 1

poisson_bracketThe Poisson bracket {f, g} of two scalar functions f, g on the phase space E × E evaluated at (q, p) is defined as the difference of inner…

Read back from the Lean

For every real Hilbert space $E$ (a complete real normed additive commutative group with an inner product space structure over $\mathbb{R}$), for all functions $f, g : E \times E \to \mathbb{R}$, and for every point $qp \in E \times E$, the Poisson bracket of $f$ and $g$ evaluated at $qp$ is the negation of the Poisson bracket of $g$ and $f$ evaluated at $qp$ (i.e., poisson_bracket f g qp = - poisson_bracket g f qp).

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.

Lean source view module on GitHub

/-- The Poisson bracket is anticommutative (skew-symmetric). -/
theorem poisson_bracket_anticomm {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    (f g : E × E → ℝ) (qp : E × E) :
    poisson_bracket f g qp = - poisson_bracket g f qp := by
  dsimp [poisson_bracket]
  rw [real_inner_comm (gradient (fun q => f (q, qp.2)) qp.1)]
  rw [real_inner_comm (gradient (fun p => f (qp.1, p)) qp.2)]
  ring

Discuss this result Challenge it