Imports
/-
Copyright (c) 2025 Tomas Skrivan. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Tomas Skrivan, Joseph Tooby-Smith
-/
module
public import Physlib.Mathematics.VariationalCalculus.HasVarGradient
public import Physlib.SpaceAndTime.Time.DerivativesHamilton's equations
In this module, given a Hamiltonian function H : Time → X → X → ℝ,
we define the operator hamiltonEqOp
which when equals zero implies hamilton's equations.
We show that the variational derivative of the action functional
∫ ⟪p, dq/dt⟫ - H(t, p, q) dt is equal to the hamiltonEqOp
applied to (p, q).
References
G. J. Sussman and J. Wisdom, "Structure and Interpretation of Classical Mechanics", Section 3.1.2. https://groups.csail.mit.edu/mac/users/gjs/6946/sicm-html/book-Z-H-36.html#%_sec_3.1.2
@[expose] public sectionlemma hamiltonEqOp_eq (H : Time → X → X → ℝ) (p : Time → X) (q : Time → X) :
hamiltonEqOp H p q = fun t => (∂ₜ q t + -gradient (fun x => H t x (q t)) (p t),
- ∂ₜ p t + -gradient (fun x => H t (p t) x) (q t)) := X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XH:Time → X → X → ℝp:Time → Xq:Time → X⊢ hamiltonEqOp H p q = fun t =>
(∂ₜ q t + -gradient (fun x => H t x (q t)) (p t), -∂ₜ p t + -gradient (fun x => H t (p t) x) (q t))
All goals completed! 🐙lemma hamiltonEqOp_eq_zero_iff_hamiltons_equations (H : Time → X → X → ℝ)
(p : Time → X) (q : Time → X) :
hamiltonEqOp H p q = 0 ↔
(∀ t, ∂ₜ q t = gradient (fun x => H t x (q t)) (p t)) ∧
(∀ t, ∂ₜ p t = -gradient (fun x => H t (p t) x) (q t)) := X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XH:Time → X → X → ℝp:Time → Xq:Time → X⊢ hamiltonEqOp H p q = 0 ↔
(∀ (t : Time), ∂ₜ q t = gradient (fun x => H t x (q t)) (p t)) ∧
∀ (t : Time), ∂ₜ p t = -gradient (fun x => H t (p t) x) (q t)
All goals completed! 🐙X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XH:Time → X → X → ℝpq:Time → X × Xhp:ContDiff ℝ ∞ pqhL:ContDiff ℝ ∞ ↿Hx:Time⊢ hamiltonEqOp H (fun t => (pq t).1) (fun t => (pq t).2) x =
((fderiv ℝ (Prod.snd ∘ pq) x) 1 + -gradient (fun x_1 => H x x_1 (pq x).2) (pq x).1,
-(fderiv ℝ (fun x => (pq x).1) x) 1 + -gradient (fun x_1 => H x (pq x).1 x_1) (pq x).2)X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XH:Time → X → X → ℝpq:Time → X × Xhp:ContDiff ℝ ∞ pqhL:ContDiff ℝ ∞ ↿Hx:Time⊢ DifferentiableAt ℝ (fun x_1 => H x (pq x).1 x_1) (pq x).2X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XH:Time → X → X → ℝpq:Time → X × Xhp:ContDiff ℝ ∞ pqhL:ContDiff ℝ ∞ ↿Hx:Time⊢ DifferentiableAt ℝ (fun x_1 => H x x_1 (pq x).2) (pq x).1
X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XH:Time → X → X → ℝpq:Time → X × Xhp:ContDiff ℝ ∞ pqhL:ContDiff ℝ ∞ ↿Hx:Time⊢ DifferentiableAt ℝ (fun x_1 => H x (pq x).1 x_1) (pq x).2X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XH:Time → X → X → ℝpq:Time → X × Xhp:ContDiff ℝ ∞ pqhL:ContDiff ℝ ∞ ↿Hx:Time⊢ DifferentiableAt ℝ (fun x_1 => H x x_1 (pq x).2) (pq x).1
all_goals exact ((X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XH:Time → X → X → ℝpq:Time → X × Xhp:ContDiff ℝ ∞ pqhL:ContDiff ℝ ∞ ↿Hx:Time⊢ ContDiff ℝ ∞ fun x_1 => H x x_1 (pq x).2 All goals completed! 🐙 : ContDiff ℝ ∞ _).differentiable (X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XH:Time → X → X → ℝpq:Time → X × Xhp:ContDiff ℝ ∞ pqhL:ContDiff ℝ ∞ ↿Hx:Time⊢ ∞ ≠ 0 All goals completed! 🐙)).differentiableAt