IsHamiltonianTrajectory
A path γ : ℝ → E × E is a Hamiltonian trajectory for the Hamiltonian H : E × E → ℝ if for all times t, the time derivative of the position component equals the momentum gradient of H at γ(t) and the time derivative of the momentum component equals the negative position gradient of H at γ(t).
Statement
def IsHamiltonianTrajectory {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (H : E × E → ℝ) (γ : ℝ → E × E) : Prop
- Source
- Arnold, Mathematical Methods of Classical Mechanics, §15; Goldstein, Poole & Safko, Classical Mechanics (3rd ed.), §8.1
- Verified
- 11 Sep 2026
- Axioms
- none listed
- Used by 1
- is_hamiltonian_trajectory_zeroThe constant zero trajectory is a Hamiltonian trajectory for the zero Hamiltonian.
Read back from the Lean
Given a complete real inner product space $E$ (a real Hilbert space), a Hamiltonian function $H : E \times E \to \mathbb{R}$, and a trajectory $\gamma : \mathbb{R} \to E \times E$, IsHamiltonianTrajectory H γ asserts that for every $t \in \mathbb{R}$:
1. The derivative at $t$ of the first component function $s \mapsto (\gamma(s))_1$ equals the gradient (over $\mathbb{R}$ on $E$) of $p \mapsto H((\gamma(t))_1, p)$ evaluated at $(\gamma(t))_2$; and
2. The derivative at $t$ of the second component function $s \mapsto (\gamma(s))_2$ equals the negation of the gradient (over $\mathbb{R}$ on $E$) of $q \mapsto H(q, (\gamma(t))_2)$ evaluated at $(\gamma(t))_1$.
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
/-- A trajectory in phase space satisfies Hamilton's canonical equations of motion with Hamiltonian H. -/ def IsHamiltonianTrajectory {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (H : E × E → ℝ) (γ : ℝ → E × E) : Prop := ∀ t : ℝ, deriv (fun s => (γ s).1) t = gradient (𝕜 := ℝ) (F := E) (fun p => H ((γ t).1, p)) (γ t).2 ∧ deriv (fun s => (γ s).2) t = - gradient (𝕜 := ℝ) (F := E) (fun q => H (q, (γ t).2)) (γ t).1