Euler-Lagrange equations

In this module we define the Euler-Lagrange operator eulerLagrangeOp, and prove the that the variational derivative of the action functional ∫ L(t, q(t), dₜ q(t)) dt is equal to the Euler-Lagrange operator applied to the trajectory q.

noncomputable def ClassicalMechanics.eulerLagrangeOp {X : Type} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (L : Time → X → X → ℝ) (q : Time → X) : Time → X

The Euler Lagrange operator, for a trajectory q : Time → X, and a lagrangian Time → X → X → ℝ, the Euler-Lagrange operator is ∂L/∂q - dₜ(∂L/∂(dₜ q)).

Equations

• ClassicalMechanics.eulerLagrangeOp L q t = gradient (fun (x : X) => L t x (Time.deriv q t)) (q t) - Time.deriv (fun (t' : Time) => gradient (fun (x : X) => L t' (q t') x) (Time.deriv q t')) t

theorem ClassicalMechanics.eulerLagrangeOp_eq {X : Type} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (L : Time → X → X → ℝ) (q : Time → X) : eulerLagrangeOp L q = fun (t : Time) => gradient (fun (x : X) => L t x (Time.deriv q t)) (q t) - Time.deriv (fun (t' : Time) => gradient (fun (x : X) => L t' (q t') x) (Time.deriv q t')) t

theorem ClassicalMechanics.eulerLagrangeOp_zero {X : Type} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (q : Time → X) : eulerLagrangeOp (fun (x : Time) (x x : X) => 0) q = fun (x : Time) => 0

theorem ClassicalMechanics.euler_lagrange_varGradient {X : Type} [NormedAddCommGroup X] [InnerProductSpace ℝ X] [CompleteSpace X] (L : Time → X → X → ℝ) (q : Time → X) (hq : ContDiff ℝ (↑⊤) q) (hL : ContDiff ℝ ↑⊤ ↿L) : varGradient (fun (q' : Time → X) (t : Time) => L t (q' t) ((fderiv ℝ q' t) 1)) q = eulerLagrangeOp L q