is_hamiltonian_trajectory_zero
theoremverified
The constant zero trajectory is a Hamiltonian trajectory for the zero Hamiltonian.
Statement
theorem is_hamiltonian_trajectory_zero {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : IsHamiltonianTrajectory (E := E) (fun _ => 0) (fun _ => (0, 0))
- Verified
- 11 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Built on 1
- IsHamiltonianTrajectoryA path γ : ℝ → E × E is a Hamiltonian trajectory for the Hamiltonian H : E × E → ℝ if for all times t, the time derivative of the position…
Lean source view module on GitHub
/-- The constant zero trajectory is a Hamiltonian trajectory for the zero Hamiltonian. -/ theorem is_hamiltonian_trajectory_zero {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] : IsHamiltonianTrajectory (E := E) (fun _ => 0) (fun _ => (0, 0)) := by simp [IsHamiltonianTrajectory]