Imports
/-
Copyright (c) 2025 Rein Zustand. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rein Zustand
-/
module
public import Physlib.Mathematics.InnerProductSpace.Basic
public import Mathlib.Analysis.InnerProductSpace.Dual
public import Physlib.SpaceAndTime.Time.Derivatives
public import Mathlib.Analysis.Calculus.ContDiff.CPolynomial
public import Physlib.Mathematics.VariationalCalculus.HasVarGradient
public import Physlib.ClassicalMechanics.EulerLagrangeEquivalent Lagrangians under Total Derivatives
i. Overview
Two Lagrangians are physically equivalent if they differ by a total time derivative d/dt F(q, t). This is because the Euler-Lagrange equations depend only on extremizing the action integral, and total derivatives don't affect which paths are extremal.
This module defines the key concept of a function being a total time derivative, which is essential for analyzing symmetries like Galilean invariance.
Note: Some authors call this "gauge equivalence" by analogy with gauge transformations in field theory, but we avoid that terminology here since no gauge fields are involved.
ii. Key insight
A general function δL(t, q, dₜ q) is a total time derivative if there exists a function F(t, q) (independent of velocity) such that: δL(t, q, dₜ q) = d/dt F(t, q) = fderiv ℝ F (t q) (v, 1)
By the chain rule, this expands to: δL(t, q, dₜ q) = ∂F/∂t + ⟨∇ᵣF, dₜ q⟩
For the special case where δL depends only on velocity dₜ q (not position or time), this implies a strong constraint: δL(dₜ q) = ⟨g, dₜ q⟩ for some constant vector g
This is because:
d/dt F(t, q) = ∂F/∂t + ⟨∇F, dₜ q⟩
For δL to be q-independent, ∇F must be q-independent
For δL to be t-independent, the time-dependent part must vanish
The result is δL = ⟨g, dₜ q⟩ for constant g
iii. Key definitions
IsTotalTimeDerivative: General case for δL(t, q, dₜ q)
IsTotalTimeDerivativeVelocity: Velocity-only case, equivalent to δL(dₜ q) = ⟨g, dₜ q⟩
iv. References
Landau & Lifshitz, "Mechanics", §2 (The principle of least action)
Landau & Lifshitz, "Mechanics", §4 (The Lagrangian for a free particle)
@[expose] public sectionA. General Total Time Derivative
A function δL(t, q, dₜ q) is a total time derivative if it can be written as d/dt F(r, t) for some function F that depends on position and time but not velocity,
δL(t, q, dₜ q) = (d/dt) F(t, q)
This is the most general form of Lagrangian equivalence under total derivatives. The key point is that F must be independent of velocity.
def IsTotalTimeDerivative
(δL : Time → X → X → ℝ) : Prop :=
∃ (F : Time → X → ℝ) (_ : ContDiff ℝ ∞ ↿F),
∀ t (q : Time → X), (ContDiff ℝ ∞ q) → δL t (q t) (∂ₜ q t) = ∂ₜ (fun t' => F t' (q t')) tExplicit reformulation (by the chain rule): δL(t, q, dₜ q) = ∂F/∂t(t, q) + ⟨∇ᵣF(t, q), dₜ q⟩
or
δL(t, q, dₜ q) = fderiv ℝ F (t, q) (1, dₜ q)
X:Typeinst✝¹:NormedAddCommGroup Xinst✝:InnerProductSpace ℝ XδL:Time → X → X → ℝtq:(Time → X) → Time → Time × X := fun q t => (t, q t)h_tq_contDiff:∀ (q : Time → X), ContDiff ℝ ∞ q → ContDiff ℝ ∞ (tq q)h_tq_der:∀ (q : Time → X) (t : Time), ContDiff ℝ ∞ q → ∂ₜ (tq q) t = (1, ∂ₜ q t)h_F_tq_der:∀ (q : Time → X) (F : Time → X → ℝ) (t : Time),
ContDiff ℝ ∞ ↿F → ContDiff ℝ ∞ q → ∂ₜ (fun t' => ↿F (t', q t')) t = (fderiv ℝ ↿F (t, q t)) (1, ∂ₜ q t)F:Time → X → ℝhFdif:ContDiff ℝ ∞ ↿FhFder:∀ (t : Time) (q v : X), δL t q v = (fderiv ℝ ↿F (t, q)) (1, v)t:Timeq:Time → Xhq_ContDiff:ContDiff ℝ ∞ q⊢ ∂ₜ (fun t' => ↿F (t', q t')) t = ∂ₜ (fun t' => F t' (q t')) tX:Typeinst✝¹:NormedAddCommGroup Xinst✝:InnerProductSpace ℝ XδL:Time → X → X → ℝtq:(Time → X) → Time → Time × X := fun q t => (t, q t)h_tq_contDiff:∀ (q : Time → X), ContDiff ℝ ∞ q → ContDiff ℝ ∞ (tq q)h_tq_der:∀ (q : Time → X) (t : Time), ContDiff ℝ ∞ q → ∂ₜ (tq q) t = (1, ∂ₜ q t)h_F_tq_der:∀ (q : Time → X) (F : Time → X → ℝ) (t : Time),
ContDiff ℝ ∞ ↿F → ContDiff ℝ ∞ q → ∂ₜ (fun t' => ↿F (t', q t')) t = (fderiv ℝ ↿F (t, q t)) (1, ∂ₜ q t)F:Time → X → ℝhFdif:ContDiff ℝ ∞ ↿FhFder:∀ (t : Time) (q v : X), δL t q v = (fderiv ℝ ↿F (t, q)) (1, v)t:Timeq:Time → Xhq_ContDiff:ContDiff ℝ ∞ q⊢ ContDiff ℝ ∞ ↿FX:Typeinst✝¹:NormedAddCommGroup Xinst✝:InnerProductSpace ℝ XδL:Time → X → X → ℝtq:(Time → X) → Time → Time × X := fun q t => (t, q t)h_tq_contDiff:∀ (q : Time → X), ContDiff ℝ ∞ q → ContDiff ℝ ∞ (tq q)h_tq_der:∀ (q : Time → X) (t : Time), ContDiff ℝ ∞ q → ∂ₜ (tq q) t = (1, ∂ₜ q t)h_F_tq_der:∀ (q : Time → X) (F : Time → X → ℝ) (t : Time),
ContDiff ℝ ∞ ↿F → ContDiff ℝ ∞ q → ∂ₜ (fun t' => ↿F (t', q t')) t = (fderiv ℝ ↿F (t, q t)) (1, ∂ₜ q t)F:Time → X → ℝhFdif:ContDiff ℝ ∞ ↿FhFder:∀ (t : Time) (q v : X), δL t q v = (fderiv ℝ ↿F (t, q)) (1, v)t:Timeq:Time → Xhq_ContDiff:ContDiff ℝ ∞ q⊢ ContDiff ℝ ∞ q
X:Typeinst✝¹:NormedAddCommGroup Xinst✝:InnerProductSpace ℝ XδL:Time → X → X → ℝtq:(Time → X) → Time → Time × X := fun q t => (t, q t)h_tq_contDiff:∀ (q : Time → X), ContDiff ℝ ∞ q → ContDiff ℝ ∞ (tq q)h_tq_der:∀ (q : Time → X) (t : Time), ContDiff ℝ ∞ q → ∂ₜ (tq q) t = (1, ∂ₜ q t)h_F_tq_der:∀ (q : Time → X) (F : Time → X → ℝ) (t : Time),
ContDiff ℝ ∞ ↿F → ContDiff ℝ ∞ q → ∂ₜ (fun t' => ↿F (t', q t')) t = (fderiv ℝ ↿F (t, q t)) (1, ∂ₜ q t)F:Time → X → ℝhFdif:ContDiff ℝ ∞ ↿FhFder:∀ (t : Time) (q v : X), δL t q v = (fderiv ℝ ↿F (t, q)) (1, v)t:Timeq:Time → Xhq_ContDiff:ContDiff ℝ ∞ q⊢ ∂ₜ (fun t' => ↿F (t', q t')) t = ∂ₜ (fun t' => F t' (q t')) t All goals completed! 🐙
X:Typeinst✝¹:NormedAddCommGroup Xinst✝:InnerProductSpace ℝ XδL:Time → X → X → ℝtq:(Time → X) → Time → Time × X := fun q t => (t, q t)h_tq_contDiff:∀ (q : Time → X), ContDiff ℝ ∞ q → ContDiff ℝ ∞ (tq q)h_tq_der:∀ (q : Time → X) (t : Time), ContDiff ℝ ∞ q → ∂ₜ (tq q) t = (1, ∂ₜ q t)h_F_tq_der:∀ (q : Time → X) (F : Time → X → ℝ) (t : Time),
ContDiff ℝ ∞ ↿F → ContDiff ℝ ∞ q → ∂ₜ (fun t' => ↿F (t', q t')) t = (fderiv ℝ ↿F (t, q t)) (1, ∂ₜ q t)F:Time → X → ℝhFdif:ContDiff ℝ ∞ ↿FhFder:∀ (t : Time) (q v : X), δL t q v = (fderiv ℝ ↿F (t, q)) (1, v)t:Timeq:Time → Xhq_ContDiff:ContDiff ℝ ∞ q⊢ ContDiff ℝ ∞ ↿F All goals completed! 🐙
X:Typeinst✝¹:NormedAddCommGroup Xinst✝:InnerProductSpace ℝ XδL:Time → X → X → ℝtq:(Time → X) → Time → Time × X := fun q t => (t, q t)h_tq_contDiff:∀ (q : Time → X), ContDiff ℝ ∞ q → ContDiff ℝ ∞ (tq q)h_tq_der:∀ (q : Time → X) (t : Time), ContDiff ℝ ∞ q → ∂ₜ (tq q) t = (1, ∂ₜ q t)h_F_tq_der:∀ (q : Time → X) (F : Time → X → ℝ) (t : Time),
ContDiff ℝ ∞ ↿F → ContDiff ℝ ∞ q → ∂ₜ (fun t' => ↿F (t', q t')) t = (fderiv ℝ ↿F (t, q t)) (1, ∂ₜ q t)F:Time → X → ℝhFdif:ContDiff ℝ ∞ ↿FhFder:∀ (t : Time) (q v : X), δL t q v = (fderiv ℝ ↿F (t, q)) (1, v)t:Timeq:Time → Xhq_ContDiff:ContDiff ℝ ∞ q⊢ ContDiff ℝ ∞ q All goals completed! 🐙Elementary fact: if δL is a time derivative, then so is -δL.
X:Typeinst✝¹:NormedAddCommGroup Xinst✝:InnerProductSpace ℝ XδL:Time → X → X → ℝF:Time → X → ℝh_ContDiff:ContDiff ℝ ∞ ↿FhF:∀ (t : Time) (q : Time → X), ContDiff ℝ ∞ q → δL t (q t) (∂ₜ q t) = ∂ₜ (fun t' => F t' (q t')) tF_neg:Time → X → ℝ := fun t q => -F t qh_neg_F_ContDiff:ContDiff ℝ ∞ ↿F_negt:Timeq:Time → Xhq:ContDiff ℝ ∞ q⊢ -∂ₜ (fun t' => F t' (q t')) t = ∂ₜ (fun t' => F_neg t' (q t')) t
X:Typeinst✝¹:NormedAddCommGroup Xinst✝:InnerProductSpace ℝ XδL:Time → X → X → ℝF:Time → X → ℝh_ContDiff:ContDiff ℝ ∞ ↿FhF:∀ (t : Time) (q : Time → X), ContDiff ℝ ∞ q → δL t (q t) (∂ₜ q t) = ∂ₜ (fun t' => F t' (q t')) tF_neg:Time → X → ℝ := fun t q => -F t qh_neg_F_ContDiff:ContDiff ℝ ∞ ↿F_negt:Timeq:Time → Xhq:ContDiff ℝ ∞ q⊢ -∂ₜ (fun t' => F t' (q t')) t = ∂ₜ (fun t' => -F t' (q t')) t
X:Typeinst✝¹:NormedAddCommGroup Xinst✝:InnerProductSpace ℝ XδL:Time → X → X → ℝF:Time → X → ℝh_ContDiff:ContDiff ℝ ∞ ↿FhF:∀ (t : Time) (q : Time → X), ContDiff ℝ ∞ q → δL t (q t) (∂ₜ q t) = ∂ₜ (fun t' => F t' (q t')) tF_neg:Time → X → ℝ := fun t q => -F t qh_neg_F_ContDiff:ContDiff ℝ ∞ ↿F_negt:Timeq:Time → Xhq:ContDiff ℝ ∞ q⊢ -(fderiv ℝ (fun t' => F t' (q t')) t) 1 = (fderiv ℝ (fun t' => -F t' (q t')) t) 1
All goals completed! 🐙If δL is a total time derivative (of a smooth function), then it is smooth
X:Typeinst✝¹:NormedAddCommGroup Xinst✝:InnerProductSpace ℝ XδL:Time → X → X → ℝh:IsTotalTimeDerivative δLF:Time → X → ℝhContDiff:ContDiff ℝ ∞ ↿Fheq:∀ (t : Time) (q v : X), δL t q v = (fderiv ℝ ↿F (t, q)) (1, v)Fder_v:(Time × X) × X → (Time × X →L[ℝ] ℝ) × X := Prod.map (fderiv ℝ ↿fun t q => F t q) fun v => vregroup:Time × X × X → (Time × X) × X := ↿fun t q v => ((t, q), v)appv:(Time × X →L[ℝ] ℝ) × X → ℝ := fun FV => FV.1 (1, FV.2)hδL:↿δL = appv ∘ Fder_v ∘ regroup⊢ ContDiff ℝ ∞ (appv ∘ Fder_v ∘ regroup)
X:Typeinst✝¹:NormedAddCommGroup Xinst✝:InnerProductSpace ℝ XδL:Time → X → X → ℝh:IsTotalTimeDerivative δLF:Time → X → ℝhContDiff:ContDiff ℝ ∞ ↿Fheq:∀ (t : Time) (q v : X), δL t q v = (fderiv ℝ ↿F (t, q)) (1, v)Fder_v:(Time × X) × X → (Time × X →L[ℝ] ℝ) × X := Prod.map (fderiv ℝ ↿fun t q => F t q) fun v => vregroup:Time × X × X → (Time × X) × X := ↿fun t q v => ((t, q), v)appv:(Time × X →L[ℝ] ℝ) × X → ℝ := fun FV => FV.1 (1, FV.2)hδL:↿δL = appv ∘ Fder_v ∘ regroup⊢ ContDiff ℝ ∞ ((fun FV => FV.1 (1, FV.2)) ∘ Fder_v ∘ regroup)
X:Typeinst✝¹:NormedAddCommGroup Xinst✝:InnerProductSpace ℝ XδL:Time → X → X → ℝh:IsTotalTimeDerivative δLF:Time → X → ℝhContDiff:ContDiff ℝ ∞ ↿Fheq:∀ (t : Time) (q v : X), δL t q v = (fderiv ℝ ↿F (t, q)) (1, v)Fder_v:(Time × X) × X → (Time × X →L[ℝ] ℝ) × X := Prod.map (fderiv ℝ ↿fun t q => F t q) fun v => vregroup:Time × X × X → (Time × X) × X := ↿fun t q v => ((t, q), v)appv:(Time × X →L[ℝ] ℝ) × X → ℝ := fun FV => FV.1 (1, FV.2)hδL:↿δL = appv ∘ Fder_v ∘ regroup⊢ ContDiff ℝ ∞ ((fun FV => FV.1 (1, FV.2)) ∘ (Prod.map (fderiv ℝ ↿fun t q => F t q) fun v => v) ∘ regroup)
X:Typeinst✝¹:NormedAddCommGroup Xinst✝:InnerProductSpace ℝ XδL:Time → X → X → ℝh:IsTotalTimeDerivative δLF:Time → X → ℝhContDiff:ContDiff ℝ ∞ ↿Fheq:∀ (t : Time) (q v : X), δL t q v = (fderiv ℝ ↿F (t, q)) (1, v)Fder_v:(Time × X) × X → (Time × X →L[ℝ] ℝ) × X := Prod.map (fderiv ℝ ↿fun t q => F t q) fun v => vregroup:Time × X × X → (Time × X) × X := ↿fun t q v => ((t, q), v)appv:(Time × X →L[ℝ] ℝ) × X → ℝ := fun FV => FV.1 (1, FV.2)hδL:↿δL = appv ∘ Fder_v ∘ regroup⊢ ContDiff ℝ ∞
((fun FV => FV.1 (1, FV.2)) ∘ (Prod.map (fderiv ℝ ↿fun t q => F t q) fun v => v) ∘ ↿fun t q v => ((t, q), v))
All goals completed! 🐙B. Total time derivative do not affect the physical content
The total time derivative does not affect the Euler-Lagrange equations, because its variational derivative is zero: ∫d/dt F(t, q)= F(t₁,q₁) - F(t₀,q₀) is fixed by the boundary conditions.
Total time derivative has a variational derivative, which is zero
X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XδL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qF:Time → X → ℝhF_contDiff:ContDiff ℝ ∞ ↿FhF:∀ (t : Time) (q : Time → X), ContDiff ℝ ∞ q → δL t (q t) (∂ₜ q t) = ∂ₜ (fun t' => F t' (q t')) ttraj_deriv:(Time → ℝ) → Time → ℝ := fun G t => (fderiv ℝ G t) 1F_traj:(Time → X) → Time → ℝ := fun q t => F t (q t)q':Time → Xhq':ContDiff ℝ ∞ q't':Time⊢ traj_deriv (F_traj q') t' = ∂ₜ (fun t' => F t' (q' t')) t'
All goals completed! 🐙
X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XδL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qF:Time → X → ℝhF_contDiff:ContDiff ℝ ∞ ↿FhF:∀ (t : Time) (q : Time → X), ContDiff ℝ ∞ q → δL t (q t) (∂ₜ q t) = ∂ₜ (fun t' => F t' (q t')) ttraj_deriv:(Time → ℝ) → Time → ℝ := fun G t => (fderiv ℝ G t) 1F_traj:(Time → X) → Time → ℝ := fun q t => F t (q t)t:Time⊢ 0 = adjFDeriv ℝ (F t) (q t) ((fun x => -(fderiv ℝ (fun x => 1) x) 1) t)
X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XδL:Time → X → X → ℝq:Time → Xhq:ContDiff ℝ ∞ qF:Time → X → ℝhF_contDiff:ContDiff ℝ ∞ ↿FhF:∀ (t : Time) (q : Time → X), ContDiff ℝ ∞ q → δL t (q t) (∂ₜ q t) = ∂ₜ (fun t' => F t' (q t')) ttraj_deriv:(Time → ℝ) → Time → ℝ := fun G t => (fderiv ℝ G t) 1F_traj:(Time → X) → Time → ℝ := fun q t => F t (q t)t:Time⊢ 0 = adjoint ℝ (⇑(fderiv ℝ (F t) (q t))) ((fun x => -(fderiv ℝ (fun x => 1) x) 1) t)
All goals completed! 🐙If two lagrangians, L and L', differ by a total time derivative, and L has a variational derivative grad, then so does L'.
X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝδL:Time → X → X → ℝhδL:IsTotalTimeDerivative δLq:Time → Xhq:ContDiff ℝ ∞ qgrad:Time → Xhgrad:HasVarGradientAt (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) grad qh_add_zero:grad = grad + fun x => 0⊢ HasVarGradientAt (fun q' t => (L + δL) t (q' t) ((fderiv ℝ q' t) 1)) (grad + fun x => 0) q
X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝδL:Time → X → X → ℝhδL:IsTotalTimeDerivative δLq:Time → Xhq:ContDiff ℝ ∞ qgrad:Time → Xhgrad:HasVarGradientAt (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) grad qh_add_zero:grad = grad + fun x => 0⊢ HasVarGradientAt (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) grad qX:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝδL:Time → X → X → ℝhδL:IsTotalTimeDerivative δLq:Time → Xhq:ContDiff ℝ ∞ qgrad:Time → Xhgrad:HasVarGradientAt (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) grad qh_add_zero:grad = grad + fun x => 0⊢ HasVarGradientAt (fun q' t => δL t (q' t) ((fderiv ℝ q' t) 1)) (fun x => 0) q
X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝδL:Time → X → X → ℝhδL:IsTotalTimeDerivative δLq:Time → Xhq:ContDiff ℝ ∞ qgrad:Time → Xhgrad:HasVarGradientAt (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) grad qh_add_zero:grad = grad + fun x => 0⊢ HasVarGradientAt (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) grad q All goals completed! 🐙
X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝδL:Time → X → X → ℝhδL:IsTotalTimeDerivative δLq:Time → Xhq:ContDiff ℝ ∞ qgrad:Time → Xhgrad:HasVarGradientAt (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) grad qh_add_zero:grad = grad + fun x => 0⊢ HasVarGradientAt (fun q' t => δL t (q' t) ((fderiv ℝ q' t) 1)) (fun x => 0) q All goals completed! 🐙X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝL':Time → X → X → ℝhtot:IsTotalTimeDerivative (L' - L)q:Time → Xhq:ContDiff ℝ ∞ qδL:Time → X → X → ℝ := fun t q v => L' t q v - L t q vhL:¬∃ grad, HasVarGradientAt (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) grad qh_triv:L = L' + -(L' - L)grad:Time → Xhgrad:HasVarGradientAt (fun q' t => L' t (q' t) ((fderiv ℝ q' t) 1)) grad q⊢ HasVarGradientAt (fun q' t => L' t (q' t) ((fderiv ℝ q' t) 1)) grad q
All goals completed! 🐙
X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝL':Time → X → X → ℝhtot:IsTotalTimeDerivative (L' - L)q:Time → Xhq:ContDiff ℝ ∞ qδL:Time → X → X → ℝ := fun t q v => L' t q v - L t q vhL:¬∃ grad, HasVarGradientAt (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) grad qhL':¬∃ grad, HasVarGradientAt (fun q' t => L' t (q' t) ((fderiv ℝ q' t) 1)) grad q⊢ varGradient (fun q' t => L' t (q' t) ((fderiv ℝ q' t) 1)) q = varGradient (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) q X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝL':Time → X → X → ℝhtot:IsTotalTimeDerivative (L' - L)q:Time → Xhq:ContDiff ℝ ∞ qδL:Time → X → X → ℝ := fun t q v => L' t q v - L t q vhL:¬∃ grad, HasVarGradientAt (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) grad qhL':¬∃ grad, HasVarGradientAt (fun q' t => L' t (q' t) ((fderiv ℝ q' t) 1)) grad q⊢ (if h : ∃ grad, HasVarGradientAt (fun q' t => L' t (q' t) ((fderiv ℝ q' t) 1)) grad q then Classical.choose h else 0) =
if h : ∃ grad, HasVarGradientAt (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) grad q then Classical.choose h else 0
All goals completed! 🐙Corollary: If L and L' differ by a total time derivative, then the corresponding Euler-Lagrange operators coincide
X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝL':Time → X → X → ℝhtot:IsTotalTimeDerivative (L' - L)hContDiff:ContDiff ℝ ∞ ↿L ∨ ContDiff ℝ ∞ ↿L'q:Time → Xhq:ContDiff ℝ ∞ qF:Time → X → ℝhFContDiff:ContDiff ℝ ∞ ↿FhEq:∀ (t : Time) (q v : X), (L' - L) t q v = (fderiv ℝ ↿F (t, q)) (1, v)hContDiff_both:ContDiff ℝ ∞ ↿L ∧ ContDiff ℝ ∞ ↿L'⊢ varGradient (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) q = varGradient (fun q' t => L' t (q' t) ((fderiv ℝ q' t) 1)) q
X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝL':Time → X → X → ℝhtot:IsTotalTimeDerivative (L' - L)hContDiff:ContDiff ℝ ∞ ↿L ∨ ContDiff ℝ ∞ ↿L'q:Time → Xhq:ContDiff ℝ ∞ qF:Time → X → ℝhFContDiff:ContDiff ℝ ∞ ↿FhEq:∀ (t : Time) (q v : X), (L' - L) t q v = (fderiv ℝ ↿F (t, q)) (1, v)hContDiff_both:ContDiff ℝ ∞ ↿L ∧ ContDiff ℝ ∞ ↿L'⊢ varGradient (fun q' t => L' t (q' t) ((fderiv ℝ q' t) 1)) q = varGradient (fun q' t => L t (q' t) ((fderiv ℝ q' t) 1)) q
X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝL':Time → X → X → ℝhtot:IsTotalTimeDerivative (L' - L)hContDiff:ContDiff ℝ ∞ ↿L ∨ ContDiff ℝ ∞ ↿L'q:Time → Xhq:ContDiff ℝ ∞ qF:Time → X → ℝhFContDiff:ContDiff ℝ ∞ ↿FhEq:∀ (t : Time) (q v : X), (L' - L) t q v = (fderiv ℝ ↿F (t, q)) (1, v)hContDiff_both:ContDiff ℝ ∞ ↿L ∧ ContDiff ℝ ∞ ↿L'⊢ IsTotalTimeDerivative (L' - L)X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝL':Time → X → X → ℝhtot:IsTotalTimeDerivative (L' - L)hContDiff:ContDiff ℝ ∞ ↿L ∨ ContDiff ℝ ∞ ↿L'q:Time → Xhq:ContDiff ℝ ∞ qF:Time → X → ℝhFContDiff:ContDiff ℝ ∞ ↿FhEq:∀ (t : Time) (q v : X), (L' - L) t q v = (fderiv ℝ ↿F (t, q)) (1, v)hContDiff_both:ContDiff ℝ ∞ ↿L ∧ ContDiff ℝ ∞ ↿L'⊢ ContDiff ℝ ∞ q
X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝL':Time → X → X → ℝhtot:IsTotalTimeDerivative (L' - L)hContDiff:ContDiff ℝ ∞ ↿L ∨ ContDiff ℝ ∞ ↿L'q:Time → Xhq:ContDiff ℝ ∞ qF:Time → X → ℝhFContDiff:ContDiff ℝ ∞ ↿FhEq:∀ (t : Time) (q v : X), (L' - L) t q v = (fderiv ℝ ↿F (t, q)) (1, v)hContDiff_both:ContDiff ℝ ∞ ↿L ∧ ContDiff ℝ ∞ ↿L'⊢ IsTotalTimeDerivative (L' - L) All goals completed! 🐙
X:Typeinst✝²:NormedAddCommGroup Xinst✝¹:InnerProductSpace ℝ Xinst✝:CompleteSpace XL:Time → X → X → ℝL':Time → X → X → ℝhtot:IsTotalTimeDerivative (L' - L)hContDiff:ContDiff ℝ ∞ ↿L ∨ ContDiff ℝ ∞ ↿L'q:Time → Xhq:ContDiff ℝ ∞ qF:Time → X → ℝhFContDiff:ContDiff ℝ ∞ ↿FhEq:∀ (t : Time) (q v : X), (L' - L) t q v = (fderiv ℝ ↿F (t, q)) (1, v)hContDiff_both:ContDiff ℝ ∞ ↿L ∧ ContDiff ℝ ∞ ↿L'⊢ ContDiff ℝ ∞ q All goals completed! 🐙C. Velocity-Only Total Time Derivative
When δL depends only on velocity (the free particle case), the condition simplifies.
A velocity-only function that is a total time derivative must be linear in velocity.
If δL depends only on velocity and equals d/dt F(t, q) for some F, then δL(dₜ q) = ⟨g, dₜ q⟩ for some constant vector g.
This characterization comes from the requirement that:
d/dt F(t, q) = ∂F/∂t + ⟨∇F, dₜ q⟩ = ∂F/∂t + ⟨∇F, dₜ q⟩
For the result to be independent of q and t, we need ∇F = g (constant) and ∂F/∂t = 0
Thus δL(dₜ q) = ⟨g, dₜ q⟩
WLOG, we assume δL 0 = 0 since constants are total derivatives (c = d/dt(c·t))
and can be absorbed without affecting the equations of motion.
All goals completed! 🐙