The action of a Lagrangian and the principle of stationary action

Let E be a real normed space, the configuration space of a mechanical system, and let L : ℝ → E × E → ℝ be a possibly time-dependent Lagrangian, a function L t (q, v) of time, positions and velocities. The action of a curve q : ℝ → E between the times a and b is

S(q) = ∫_a^b L(t, q(t), q'(t)) dt (TauCeti.lagrangianAction).

A variation of q is a two-parameter family Q s t with Q 0 = q, and its variation field is η(t) = ∂_s Q(0, t). This file computes the derivative of the action along a variation. When the uncurried family (s, t) ↦ Q s t is C² and L is C¹ along q, differentiation under the integral sign and the symmetry of the mixed partial derivatives of Q give

d/ds S(Q s)|₀ = ∫_a^b DL_t(q, q')(η, η') dt (TauCeti.hasDerivAt_lagrangianAction),

the integral of the derivative of L along the first prolongation (η, η') of the variation field. Along a C¹ curve q, the force ∂_q L(t, q, q') is continuous (TauCeti.continuousAt_force). When L is moreover C², the momentum p(t) = ∂_v L(t, q, q') is C¹ (TauCeti.contDiffAt_momentum), and an integration by parts produces the first variation formula with its endpoint boundary term

d/ds S(Q s)|₀ = p(b)(η(b)) - p(a)(η(a)) + ∫_a^b (∂_q L(t, q, q') - p'(t))(η(t)) dt

(TauCeti.hasDerivAt_lagrangianAction_of_contDiffAt_two). For a variation with fixed endpoints (TauCeti.Manifold.IsFixedEndpointVariation, in the normed space E) the variation field vanishes at a and b, so only the integral of the Euler–Lagrange expression ∂_q L - p' remains (TauCeti.Manifold.IsFixedEndpointVariation.hasDerivAt_lagrangianAction).

A curve is a stationary point of the action among C^n variations (TauCeti.IsActionStationary) when it is C^n on [a, b] and the action of every C^n variation with fixed endpoints has derivative zero at s = 0. Hamilton's principle of stationary action says that, for 2 ≤ n ≤ ∞, a C^n curve along which L is C² is stationary exactly when it solves the Euler–Lagrange equations

d/dt ∂_v L(t, q, q') = ∂_q L(t, q, q')

on the open interval between a and b (TauCeti.isActionStationary_iff_eulerLagrange). The forward direction tests the first variation formula against the variations q + s ψ e, with ψ a smooth function supported in the open interval and e ∈ E, and applies the fundamental lemma of the calculus of variations (IsOpen.ae_eq_zero_of_integral_contDiff_smul_eq_zero). The Euler–Lagrange equations are stated in the form of the hypothesis of Noether's theorem TauCeti.hasDerivAt_noetherCharge, with the velocity deriv q, so stationary curves feed it directly.

No finite dimensionality of E is needed, and the endpoints a and b may come in either order. When a = b every curve that is C^n at a is stationary and the open interval is empty.

The structure of the variation computation, and of the stationarity predicate carrying the regularity of the curve as a field, follows the Riemannian first variation of energy TauCeti.Manifold.hasDerivAt_energy and TauCeti.Manifold.IsEnergyCritical in TauCeti.Geometry.Manifold.Riemannian.FirstVariation.

Main definitions

• TauCeti.lagrangianAction L q a b: the action ∫_a^b L(t, q(t), q'(t)) dt.
• TauCeti.IsActionStationary n L q a b: q is a stationary point of the action among C^n variations with fixed endpoints.

Main results

• TauCeti.contDiffAt_momentum, TauCeti.continuousAt_force: regularity of the momentum along a C² curve and of the force along a C¹ curve.
• TauCeti.hasDerivAt_lagrangianAction: the derivative of the action along a variation.
• TauCeti.hasDerivAt_lagrangianAction_of_contDiffAt_two: the first variation formula with the endpoint boundary term.
• TauCeti.Manifold.IsFixedEndpointVariation.hasDerivAt_lagrangianAction: the first variation formula for a variation with fixed endpoints.
• TauCeti.isActionStationary_iff_eulerLagrange: Hamilton's principle of stationary action.

References

• V. I. Arnold, Mathematical Methods of Classical Mechanics, 2nd ed., Graduate Texts in Mathematics 60, Springer, 1989, Section 12.
• I. M. Gelfand, S. V. Fomin, Calculus of Variations, Prentice–Hall, 1963, Sections 3 and 4.
• J. E. Marsden, T. S. Ratiu, Introduction to Mechanics and Symmetry, 2nd ed., Texts in Applied Mathematics 17, Springer, 1999, Section 8.1.

The action

noncomputable def TauCeti.lagrangianAction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : ℝ → E × E → ℝ) (q : ℝ → E) (a b : ℝ) : ℝ

The action of a time-dependent Lagrangian L along a curve q between the times a and b: the integral ∫_a^b L(t, q(t), q'(t)) dt.

theorem TauCeti.lagrangianAction_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : ℝ → E × E → ℝ) (q : ℝ → E) (a b : ℝ) : lagrangianAction L q a b = ∫ (t : ℝ) in a..b, L t (q t, deriv q t)

@[simp]

theorem TauCeti.lagrangianAction_same {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : ℝ → E × E → ℝ) (q : ℝ → E) (a : ℝ) : lagrangianAction L q a a = 0

theorem TauCeti.lagrangianAction_symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : ℝ → E × E → ℝ) (q : ℝ → E) (a b : ℝ) : lagrangianAction L q b a = -lagrangianAction L q a b

theorem TauCeti.lagrangianAction_add_lagrangianAction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : ℝ → E × E → ℝ} {q : ℝ → E} {a b c : ℝ} (hab : IntervalIntegrable (fun (t : ℝ) => L t (q t, deriv q t)) MeasureTheory.volume a b) (hbc : IntervalIntegrable (fun (t : ℝ) => L t (q t, deriv q t)) MeasureTheory.volume b c) : lagrangianAction L q a b + lagrangianAction L q b c = lagrangianAction L q a c

The action is additive over consecutive time intervals.

The momentum and the force along a curve

theorem TauCeti.contDiffAt_momentum {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : ℝ → E × E → ℝ} {q : ℝ → E} {t : ℝ} (hq : ContDiffAt ℝ 2 q t) (hL : ContDiffAt ℝ 2 (Function.uncurry L) (t, q t, deriv q t)) : ContDiffAt ℝ 1 (fun (r : ℝ) => fderiv ℝ (fun (u : E) => L r (q r, u)) (deriv q r)) t

Along a C² curve, where L is C², the momentum t ↦ ∂_v L(t, q, q') is C¹.

theorem TauCeti.continuousAt_force {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : ℝ → E × E → ℝ} {q : ℝ → E} {t : ℝ} (hq : ContDiffAt ℝ 1 q t) (hL : ContDiffAt ℝ 1 (Function.uncurry L) (t, q t, deriv q t)) : ContinuousAt (fun (r : ℝ) => fderiv ℝ (fun (y : E) => L r (y, deriv q r)) (q r)) t

Along a C¹ curve, where L is C¹, the force t ↦ ∂_q L(t, q, q') is continuous.

The first variation of the action

theorem TauCeti.hasDerivAt_lagrangianAction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : ℝ → E × E → ℝ} {Q : ℝ → ℝ → E} {a b : ℝ} (hQ : ∀ t ∈ Set.uIcc a b, ContDiffAt ℝ 2 (Function.uncurry Q) (0, t)) (hL : ∀ t ∈ Set.uIcc a b, ContDiffAt ℝ 1 (Function.uncurry L) (t, Q 0 t, deriv (Q 0) t)) : HasDerivAt (fun (s : ℝ) => lagrangianAction L (Q s) a b) (∫ (t : ℝ) in a..b, (fderiv ℝ (L t) (Q 0 t, deriv (Q 0) t)) (deriv (fun (s : ℝ) => Q s t) 0, deriv (fun (r : ℝ) => deriv (fun (s : ℝ) => Q s r) 0) t)) 0

The derivative of the action along a variation. Let the uncurried family (s, t) ↦ Q s t be C² at every point of {0} × [a, b], and let L be jointly C¹ in time, position and velocity along the central curve Q 0. Then the action of Q s between a and b is differentiable at s = 0, with derivative the integral of the derivative of L along the first prolongation (η, η') of the variation field η(t) = ∂_s Q(0, t).

theorem TauCeti.hasDerivAt_lagrangianAction_of_contDiffAt_two {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : ℝ → E × E → ℝ} {Q : ℝ → ℝ → E} {a b : ℝ} (hQ : ∀ t ∈ Set.uIcc a b, ContDiffAt ℝ 2 (Function.uncurry Q) (0, t)) (hL : ∀ t ∈ Set.uIcc a b, ContDiffAt ℝ 2 (Function.uncurry L) (t, Q 0 t, deriv (Q 0) t)) : HasDerivAt (fun (s : ℝ) => lagrangianAction L (Q s) a b) ((fderiv ℝ (fun (u : E) => L b (Q 0 b, u)) (deriv (Q 0) b)) (deriv (fun (s : ℝ) => Q s b) 0) - (fderiv ℝ (fun (u : E) => L a (Q 0 a, u)) (deriv (Q 0) a)) (deriv (fun (s : ℝ) => Q s a) 0) + ∫ (t : ℝ) in a..b, (fderiv ℝ (fun (y : E) => L t (y, deriv (Q 0) t)) (Q 0 t) - deriv (fun (r : ℝ) => fderiv ℝ (fun (u : E) => L r (Q 0 r, u)) (deriv (Q 0) r)) t) (deriv (fun (s : ℝ) => Q s t) 0)) 0

The first variation formula, with the endpoint boundary term. Let the uncurried family (s, t) ↦ Q s t be C² at every point of {0} × [a, b], and let L be jointly C² along the central curve q = Q 0. Then the action of Q s between a and b is differentiable at s = 0, with derivative

p(b)(η(b)) - p(a)(η(a)) + ∫_a^b (∂_q L(t, q, q') - p'(t))(η(t)) dt,

where η(t) = ∂_s Q(0, t) is the variation field and p(t) = ∂_v L(t, q, q') the momentum.

theorem TauCeti.Manifold.IsFixedEndpointVariation.hasDerivAt_lagrangianAction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : ℝ → E × E → ℝ} {Q : ℝ → ℝ → E} {a b : ℝ} (hQ : IsFixedEndpointVariation (modelWithCornersSelf ℝ E) 2 Q a b) (hL : ∀ t ∈ Set.uIcc a b, ContDiffAt ℝ 2 (Function.uncurry L) (t, Q 0 t, deriv (Q 0) t)) : HasDerivAt (fun (s : ℝ) => lagrangianAction L (Q s) a b) (∫ (t : ℝ) in a..b, (fderiv ℝ (fun (y : E) => L t (y, deriv (Q 0) t)) (Q 0 t) - deriv (fun (r : ℝ) => fderiv ℝ (fun (u : E) => L r (Q 0 r, u)) (deriv (Q 0) r)) t) (deriv (fun (s : ℝ) => Q s t) 0)) 0

The first variation formula for a variation with fixed endpoints. For a C² variation Q of q = Q 0 with fixed endpoints between a and b, along which L is C², the derivative at s = 0 of the action of Q s is the integral of the Euler–Lagrange expression ∂_q L(t, q, q') - d/dt ∂_v L(t, q, q') against the variation field η(t) = ∂_s Q(0, t).

Hamilton's principle of stationary action

structure TauCeti.IsActionStationary {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (n : WithTop ℕ∞) (L : ℝ → E × E → ℝ) (q : ℝ → E) (a b : ℝ) : Prop

A curve q is a stationary point of the action of L among C^n variations between the times a and b when it is C^n at every point of [a, b] and every C^n variation of q with fixed endpoints (TauCeti.Manifold.IsFixedEndpointVariation, in the normed space E) leaves the action stationary to first order: the action of Q s has derivative 0 at s = 0. The regularity of q is part of the definition, since a curve which is not C^n admits no C^n variation.

• contDiffAt (t : ℝ) : t ∈ Set.uIcc a b → ContDiffAt ℝ n q t

  A stationary point of the action among C^n variations is C^n on [a, b].

• hasDerivAt {Q : ℝ → ℝ → E} : Q 0 = q → Manifold.IsFixedEndpointVariation (modelWithCornersSelf ℝ E) n Q a b → HasDerivAt (fun (s : ℝ) => lagrangianAction L (Q s) a b) 0 0

  The action of a C^n fixed-endpoint variation of a stationary point has derivative 0 at s = 0.

theorem TauCeti.isActionStationary_iff_eulerLagrange {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : ℝ → E × E → ℝ} {a b : ℝ} {n : WithTop ℕ∞} {q : ℝ → E} (hn : 2 ≤ n) (hn' : n ≤ ↑⊤) (hq : ∀ t ∈ Set.uIcc a b, ContDiffAt ℝ n q t) (hL : ∀ t ∈ Set.uIcc a b, ContDiffAt ℝ 2 (Function.uncurry L) (t, q t, deriv q t)) : IsActionStationary n L q a b ↔ ∀ t ∈ Set.uIoo a b, HasDerivAt (fun (s : ℝ) => fderiv ℝ (fun (u : E) => L s (q s, u)) (deriv q s)) (fderiv ℝ (fun (y : E) => L t (y, deriv q t)) (q t)) t

Hamilton's principle of stationary action. For 2 ≤ n ≤ ∞, let q be C^n at every point of [a, b] and let L be jointly C² along q. Then q is a stationary point of the action of L among C^n variations with fixed endpoints between a and b exactly when it solves the Euler–Lagrange equations d/dt ∂_v L(t, q, q') = ∂_q L(t, q, q') at every time strictly between a and b.