poisson_bracket
def
The 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 products ⟪∇_q f, ∇_p g⟫ - ⟪∇_p f, ∇_q g⟫.
Statement
noncomputable def poisson_bracket {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f g : E × E → ℝ) (qp : E × E) : ℝ
- Source
- Arnold, Mathematical Methods of Classical Mechanics, §38; Goldstein, Poole & Safko, Classical Mechanics (3rd ed.), §9.4
- Verified
- 11 Sep 2026
- Axioms
- none listed
- Used by 1
- poisson_bracket_anticommFor 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) =…
Read back from the Lean
Given a complete real inner product space E (a real Hilbert space), two functions f, g : E × E → ℝ, and a point qp = (q, p) : E × E, poisson_bracket f g qp is the real number defined by:
⟨∇(q ↦ f(q, qp.2))(qp.1), ∇(p ↦ g(qp.1, p))(qp.2)⟩ - ⟨∇(p ↦ f(qp.1, p))(qp.2), ∇(q ↦ g(q, qp.2))(qp.1)⟩
where ⟨·, ·⟩ denotes the inner product on E and ∇ denotes the Fréchet gradient (the Riesz representer of the Fréchet derivative) with respect to E.
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 of two observables on the phase space of a classical mechanical system. -/ noncomputable def poisson_bracket {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f g : E × E → ℝ) (qp : E × E) : ℝ := @inner ℝ E _ (gradient (𝕜 := ℝ) (F := E) (fun q => f (q, qp.2)) qp.1) (gradient (𝕜 := ℝ) (F := E) (fun p => g (qp.1, p)) qp.2) - @inner ℝ E _ (gradient (𝕜 := ℝ) (F := E) (fun p => f (qp.1, p)) qp.2) (gradient (𝕜 := ℝ) (F := E) (fun q => g (q, qp.2)) qp.1)