Hamilton's equations

In this module, given a Hamiltonian function H : Time → X → X → ℝ, we define the operator hamiltonEqOp whichn 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).

noncomputable def ClassicalMechanics.hamiltonEqOp {X : Type} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (H : Time → X → X → ℝ) (p q : Time → X) : Time → X × X

Given a hamiltonian H : Time → X → X → ℝ the operator which when set to zero implies the Hamilton equations.

Equations

• ClassicalMechanics.hamiltonEqOp H p q t = (Time.deriv q t + -gradient (fun (x : X) => H t x (q t)) (p t), -Time.deriv p t + -gradient (fun (x : X) => H t (p t) x) (q t))

theorem ClassicalMechanics.hamiltonEqOp_eq {X : Type} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (H : Time → X → X → ℝ) (p q : Time → X) : hamiltonEqOp H p q = fun (t : Time) => (Time.deriv q t + -gradient (fun (x : X) => H t x (q t)) (p t), -Time.deriv p t + -gradient (fun (x : X) => H t (p t) x) (q t))

theorem ClassicalMechanics.hamiltonEqOp_eq_zero_iff_hamiltons_equations {X : Type} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (H : Time → X → X → ℝ) (p q : Time → X) : hamiltonEqOp H p q = 0 ↔ (∀ (t : Time), Time.deriv q t = gradient (fun (x : X) => H t x (q t)) (p t)) ∧ ∀ (t : Time), Time.deriv p t = -gradient (fun (x : X) => H t (p t) x) (q t)

theorem ClassicalMechanics.hamiltons_equations_varGradient {X : Type} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (H : Time → X → X → ℝ) (pq : Time → X × X) (hp : ContDiff ℝ (↑⊤) pq) (hL : ContDiff ℝ ↑⊤ ↿H) : varGradient (fun (pq' : Time → X × X) (t : Time) => inner ℝ (pq' t).1 (Time.deriv (Prod.snd ∘ pq') t) - H t (pq' t).1 (pq' t).2) pq = fun (t : Time) => hamiltonEqOp H (fun (t : Time) => (pq t).1) (fun (t : Time) => (pq t).2) t