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.FirstVariationFirst-order local field theory
i. Overview
This module provides a thin usability layer for first-order local field theory, i.e. the
specialization of the local CFT stack to k = 1.
The definitions here do not introduce a new theory. They are aliases and projections for the existing coordinate-readout stack:
first-order jet points are JetPoint d m 1,
first-order lagrangians are Lagrangian d m 1,
field values are still the zero-order jet coordinates,
first derivatives are the coordinates indexed by MultiIndex.increment 0 i.
This keeps the general finite-order API as the source of truth while making the common first-order case easier to state in examples and later mechanics bridges.
ii. Key results
ClassicalFieldTheory.Local.FirstOrderJetPoint
ClassicalFieldTheory.Local.FirstOrderLagrangian
ClassicalFieldTheory.Local.firstDerivativeIndex
ClassicalFieldTheory.Local.JetPoint.firstDerivCoord
ClassicalFieldTheory.Local.firstOrderJetAt
iii. Table of contents
A. First-order aliases
B. First derivative indices
C. First-order jet projections
D. First-order evaluation and variational API
iv. References
J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics, arXiv:1612.03100v2, Chapter 5.
@[expose] public sectionA. First-order aliases
Coordinate data for first-order local jet points.
abbrev FirstOrderJetCoordinates (d m : ℕ) := JetCoordinates d m 1Coordinate-level first-order jet points.
abbrev FirstOrderJetPoint (d m : ℕ) := JetPoint d m 1Fiber-direction data for first-order jet points.
abbrev FirstOrderJetFiberData (d m : ℕ) := JetFiberData d m 1First-order local lagrangians.
abbrev FirstOrderLagrangian (d m : ℕ) := Lagrangian d m 1B. First derivative indices
The first-derivative coordinate index in the source direction i.
def firstDerivativeIndex (d : ℕ) (i : Fin d) : DerivativeIndex d 1 :=
⟨Physlib.MultiIndex.increment 0 i, d:ℕi:Fin d⊢ (MultiIndex.increment 0 i).order ≤ 1 All goals completed! 🐙⟩@[simp]
lemma firstDerivativeIndex_coe (d : ℕ) (i : Fin d) :
((firstDerivativeIndex d i : DerivativeIndex d 1) : MultiIndex d) =
Physlib.MultiIndex.increment 0 i := rfllemma firstDerivativeIndex_order (d : ℕ) (i : Fin d) :
((firstDerivativeIndex d i : DerivativeIndex d 1) : MultiIndex d).order = 1 := d:ℕi:Fin d⊢ (↑(firstDerivativeIndex d i)).order = 1
All goals completed! 🐙C. First-order jet projections
The first derivative coordinate u^a_i of a first-order jet point.
def firstDerivCoord (J : FirstOrderJetPoint d m) (i : Fin d) (a : Fin m) : ℝ :=
J.coord (firstDerivativeIndex d i) a
The bundled target vector of first derivative coordinates in the source direction i.
def firstDerivVector (J : FirstOrderJetPoint d m) (i : Fin d) : EuclideanSpace ℝ (Fin m) :=
WithLp.toLp 2 fun a => J.firstDerivCoord i a@[simp]
lemma firstDerivVector_apply (J : FirstOrderJetPoint d m) (i : Fin d) (a : Fin m) :
J.firstDerivVector i a = J.firstDerivCoord i a := d:ℕm:ℕJ:FirstOrderJetPoint d mi:Fin da:Fin m⊢ (firstDerivVector J i).ofLp a = firstDerivCoord J i a
All goals completed! 🐙@[simp]
lemma firstDerivCoord_ofBaseCoordinates (x : Space d) (u : FirstOrderJetCoordinates d m)
(i : Fin d) (a : Fin m) :
(JetPoint.ofBaseCoordinates x u).firstDerivCoord i a = u (firstDerivativeIndex d i) a := rflD. First-order evaluation and variational API
@[simp]
lemma firstOrderJetAt_base (f : Space d → EuclideanSpace ℝ (Fin m)) (x : Space d) :
(firstOrderJetAt f x).base = x := rfllemma firstOrderJetAt_value (f : Space d → EuclideanSpace ℝ (Fin m)) (x : Space d) :
(firstOrderJetAt f x).value = f x := d:ℕm:ℕf:Space d → EuclideanSpace ℝ (Fin m)x:Space d⊢ JetPoint.value (firstOrderJetAt f x) = f x
All goals completed! 🐙@[simp]
lemma firstOrderJetAt_firstDerivCoord (f : Space d → EuclideanSpace ℝ (Fin m))
(x : Space d) (i : Fin d) (a : Fin m) :
(firstOrderJetAt f x).firstDerivCoord i a =
∂^[Physlib.MultiIndex.increment 0 i] (fun y => (f y) a) x := rfltheorem firstOrder_isCritical_iff_eulerLagrange_zero
(L : FirstOrderLagrangian d m) (f : Space d → EuclideanSpace ℝ (Fin m))
(hLf : IsAdmissibleForAction L f)
(hL : Lagrangian.SmoothInCoordinates L) :
IsCritical L f ↔ firstOrderEulerLagrangeOp L f = 0 := d:ℕm:ℕL:FirstOrderLagrangian d mf:Space d → EuclideanSpace ℝ (Fin m)hLf:IsAdmissibleForAction L fhL:Lagrangian.SmoothInCoordinates L⊢ IsCritical L f ↔ firstOrderEulerLagrangeOp L f = 0
All goals completed! 🐙