Imports
/-
Copyright (c) 2026 Juan Jose Fernandez Morales. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Juan Jose Fernandez Morales
-/
module
public import PhyslibAlpha.ClassicalFieldTheory.Local.TotalDivergenceLagrangian equivalence up to total divergences
i. Overview
This module adds the local coordinate API for lagrangians that differ by a total divergence.
In the current Alpha stack, local lagrangians carry their jet-coordinate derivatives explicitly. Consequently, this module does not construct the modified lagrangian by adding a current divergence syntactically. Instead, it packages the data needed by later equivalence results:
two local lagrangians of the same order,
a total-divergence lagrangian witnessing the density difference,
and equality of the corresponding Euler-Lagrange operators.
This is the field-theory analogue of the classical fact that adding a total derivative or total divergence does not change the variational equations, while keeping the current API honest about which facts are data and which facts are proved.
ii. Key results
ClassicalFieldTheory.Local.HasTotalDivergenceDifference
ClassicalFieldTheory.Local.IsEulerLagrangeEquivalent
ClassicalFieldTheory.Local.IsEulerLagrangeEquivalent.eulerLagrangeOp_eq_zero_iff
ClassicalFieldTheory.Local.IsEulerLagrangeEquivalent.isCritical_iff
ClassicalFieldTheory.Local.TotalDivergenceEquivalence
ClassicalFieldTheory.Local.TotalDivergenceEquivalence.isCritical_iff
iii. Table of contents
A. Equivalence predicates
B. Euler-Lagrange equivalence API
C. Packaged total-divergence equivalences
iv. References
J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics, arXiv:1612.03100v2, Chapter 5.
@[expose] public sectionA. Equivalence predicates
A lagrangian target differs from source by the density of a packaged total divergence.
The total divergence has current order k, hence its associated lagrangian and both compared
lagrangians have order k + 1.
def HasTotalDivergenceDifference (source target : Lagrangian d m (k + 1))
(T : TotalDivergence d m k) : Prop :=
∀ f : Space d → EuclideanSpace ℝ (Fin m),
actionDensity target f =
fun x => actionDensity source f x + actionDensity T.lagrangian f xTwo local lagrangians are Euler-Lagrange equivalent when they determine the same local Euler-Lagrange operator along every field.
def IsEulerLagrangeEquivalent (source target : Lagrangian d m k) : Prop :=
∀ f : Space d → EuclideanSpace ℝ (Fin m),
eulerLagrangeOp target f = eulerLagrangeOp source fB. Euler-Lagrange equivalence API
lemma refl (L : Lagrangian d m k) : IsEulerLagrangeEquivalent L L := d:ℕm:ℕk:ℕL:Lagrangian d m k⊢ IsEulerLagrangeEquivalent L L
d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)⊢ eulerLagrangeOp L f = eulerLagrangeOp L f
All goals completed! 🐙lemma symm {L1 L2 : Lagrangian d m k} (h : IsEulerLagrangeEquivalent L1 L2) :
IsEulerLagrangeEquivalent L2 L1 := d:ℕm:ℕk:ℕL1:Lagrangian d m kL2:Lagrangian d m kh:IsEulerLagrangeEquivalent L1 L2⊢ IsEulerLagrangeEquivalent L2 L1
d:ℕm:ℕk:ℕL1:Lagrangian d m kL2:Lagrangian d m kh:IsEulerLagrangeEquivalent L1 L2f:Space d → EuclideanSpace ℝ (Fin m)⊢ eulerLagrangeOp L1 f = eulerLagrangeOp L2 f
All goals completed! 🐙lemma trans {L1 L2 L3 : Lagrangian d m k}
(h12 : IsEulerLagrangeEquivalent L1 L2) (h23 : IsEulerLagrangeEquivalent L2 L3) :
IsEulerLagrangeEquivalent L1 L3 := d:ℕm:ℕk:ℕL1:Lagrangian d m kL2:Lagrangian d m kL3:Lagrangian d m kh12:IsEulerLagrangeEquivalent L1 L2h23:IsEulerLagrangeEquivalent L2 L3⊢ IsEulerLagrangeEquivalent L1 L3
d:ℕm:ℕk:ℕL1:Lagrangian d m kL2:Lagrangian d m kL3:Lagrangian d m kh12:IsEulerLagrangeEquivalent L1 L2h23:IsEulerLagrangeEquivalent L2 L3f:Space d → EuclideanSpace ℝ (Fin m)⊢ eulerLagrangeOp L3 f = eulerLagrangeOp L1 f
All goals completed! 🐙lemma eulerLagrangeOp_eq {source target : Lagrangian d m k}
(h : IsEulerLagrangeEquivalent source target)
(f : Space d → EuclideanSpace ℝ (Fin m)) :
eulerLagrangeOp target f = eulerLagrangeOp source f :=
h fAll goals completed! 🐙All goals completed! 🐙lemma isCritical_target_of_source {source target : Lagrangian d m k}
(h : IsEulerLagrangeEquivalent source target)
(f : Space d → EuclideanSpace ℝ (Fin m))
(hsourcef : IsAdmissibleForAction source f)
(htargetf : IsAdmissibleForAction target f)
(hsource : Lagrangian.SmoothInCoordinates source)
(htarget : Lagrangian.SmoothInCoordinates target)
(hcrit : IsCritical source f) :
IsCritical target f :=
(h.isCritical_iff f hsourcef htargetf hsource htarget).2 hcritlemma isCritical_source_of_target {source target : Lagrangian d m k}
(h : IsEulerLagrangeEquivalent source target)
(f : Space d → EuclideanSpace ℝ (Fin m))
(hsourcef : IsAdmissibleForAction source f)
(htargetf : IsAdmissibleForAction target f)
(hsource : Lagrangian.SmoothInCoordinates source)
(htarget : Lagrangian.SmoothInCoordinates target)
(hcrit : IsCritical target f) :
IsCritical source f :=
(h.isCritical_iff f hsourcef htargetf hsource htarget).1 hcritC. Packaged total-divergence equivalences
A packaged equivalence between two local lagrangians whose densities differ by a total divergence.
The field sameEulerLagrangeOp records the variational consequence in the current Alpha API. It
will become a theorem once the stack has enough symbolic calculus for coordinate derivatives of
total divergences.
The original local lagrangian.
The modified local lagrangian.
The total divergence giving the density difference.
The target density is the source density plus the total-divergence density.
The two lagrangians have the same Euler-Lagrange operator.
structure TotalDivergenceEquivalence (d m k : ℕ) where source : Lagrangian d m (k + 1) target : Lagrangian d m (k + 1) divergence : TotalDivergence d m k hasTotalDivergenceDifference :
HasTotalDivergenceDifference source target divergence sameEulerLagrangeOp : IsEulerLagrangeEquivalent source target@[simp]
lemma actionDensity_eq (E : TotalDivergenceEquivalence d m k)
(f : Space d → EuclideanSpace ℝ (Fin m)) :
actionDensity E.target f =
fun x => actionDensity E.source f x + actionDensity E.divergence.lagrangian f x :=
E.hasTotalDivergenceDifference flemma eulerLagrangeOp_eq (E : TotalDivergenceEquivalence d m k)
(f : Space d → EuclideanSpace ℝ (Fin m)) :
eulerLagrangeOp E.target f = eulerLagrangeOp E.source f :=
E.sameEulerLagrangeOp flemma eulerLagrangeOp_eq_zero_iff (E : TotalDivergenceEquivalence d m k)
(f : Space d → EuclideanSpace ℝ (Fin m)) :
eulerLagrangeOp E.target f = 0 ↔ eulerLagrangeOp E.source f = 0 :=
E.sameEulerLagrangeOp.eulerLagrangeOp_eq_zero_iff flemma isCritical_iff (E : TotalDivergenceEquivalence d m k)
(f : Space d → EuclideanSpace ℝ (Fin m))
(hsourcef : IsAdmissibleForAction E.source f)
(htargetf : IsAdmissibleForAction E.target f)
(hsource : Lagrangian.SmoothInCoordinates E.source)
(htarget : Lagrangian.SmoothInCoordinates E.target) :
IsCritical E.target f ↔ IsCritical E.source f := d:ℕm:ℕk:ℕE:TotalDivergenceEquivalence d m kf:Space d → EuclideanSpace ℝ (Fin m)hsourcef:IsAdmissibleForAction E.source fhtargetf:IsAdmissibleForAction E.target fhsource:E.source.SmoothInCoordinateshtarget:E.target.SmoothInCoordinates⊢ IsCritical E.target f ↔ IsCritical E.source f
All goals completed! 🐙lemma isCritical_target_of_source (E : TotalDivergenceEquivalence d m k)
(f : Space d → EuclideanSpace ℝ (Fin m))
(hsourcef : IsAdmissibleForAction E.source f)
(htargetf : IsAdmissibleForAction E.target f)
(hsource : Lagrangian.SmoothInCoordinates E.source)
(htarget : Lagrangian.SmoothInCoordinates E.target)
(hcrit : IsCritical E.source f) :
IsCritical E.target f :=
E.sameEulerLagrangeOp.isCritical_target_of_source f hsourcef htargetf hsource htarget hcritlemma isCritical_source_of_target (E : TotalDivergenceEquivalence d m k)
(f : Space d → EuclideanSpace ℝ (Fin m))
(hsourcef : IsAdmissibleForAction E.source f)
(htargetf : IsAdmissibleForAction E.target f)
(hsource : Lagrangian.SmoothInCoordinates E.source)
(htarget : Lagrangian.SmoothInCoordinates E.target)
(hcrit : IsCritical E.target f) :
IsCritical E.source f :=
E.sameEulerLagrangeOp.isCritical_source_of_target f hsourcef htargetf hsource htarget hcrit