1. PhyslibAlpha
  2. ClassicalFieldTheory
  3. Local
  4. Action
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.Lagrangian public import PhyslibAlpha.ClassicalFieldTheory.Local.Variation

Local action functionals

i. Overview

This module defines the local action functional associated with a local Lagrangian, together with the first notions needed to talk about variational criticality.

For the first implementation pass, the action is defined directly as the integral of a local Lagrangian evaluated along jets of a field. The integrability conditions needed for this action and for its variations are kept explicit in the API.

ii. Key results

    ClassicalFieldTheory.Local.actionDensity : the density associated with a field.

    ClassicalFieldTheory.Local.action : the action of a field.

    ClassicalFieldTheory.Local.HasFiniteAction : finiteness of the action integral.

    ClassicalFieldTheory.Local.IsAdmissibleForAction : symmetric admissibility of a lagrangian and field pair for the action functional.

    ClassicalFieldTheory.Local.actionVariation : the action under an admissible variation.

    ClassicalFieldTheory.Local.IsCritical : vanishing first derivative of the varied action.

iii. Table of contents

    A. Action densities and action

    B. Action under variation

    C. Critical fields

iv. References

    J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics, Chapter 5.

@[expose] public section

A. Action densities and action

The integrability condition for the action density of a field.

def HasFiniteAction (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) : Prop := Integrable (actionDensity L f)

Symmetric admissibility predicate for the action functional: the pair (L, f) is admissible when the field is smooth and the corresponding action density is integrable.

def IsAdmissibleForAction (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) : Prop := ContDiff ℝ ∞ f ∧ HasFiniteAction L f
@[simp] lemma actionDensity_apply (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (x : Space d) : actionDensity L f x = L (jetAt k f x) := rfl@[simp] lemma action_eq_integral (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) : action L f = ∫ x, actionDensity L f x := rfl

B. Action under variation

Smoothness of the varied field for smooth f and admissible η.

lemma variedField_contDiff (f : Space d → EuclideanSpace ℝ (Fin m)) (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) (s : ℝ) (hf : ContDiff ℝ ∞ f) : ContDiff ℝ ∞ (variedField f η s) := d:ℕm:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))s:ℝhf:ContDiff ℝ ∞ f⊢ ContDiff ℝ ∞ (variedField f η s) All goals completed! 🐙

Explicit integrability condition for the family of varied action densities.

def HasFiniteActionVariation (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) : Prop := ∀ s : ℝ, Integrable (actionDensity L (variedField f η s))

Locality package for the action density under compactly supported variations: for every variation parameter s, the change in the action density is a continuous compactly supported function. Combined with finiteness of the base action, this implies finiteness of the varied action.

def HasCompactlySupportedActionVariationDifference (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) : Prop := ∀ s : ℝ, Continuous (fun x => actionDensity L (variedField f η s) x - actionDensity L f x) ∧ HasCompactSupport (fun x => actionDensity L (variedField f η s) x - actionDensity L f x)

If the base action is finite and every varied action density differs from the base density by a continuous compactly supported function, then the whole varied family has finite action.

d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hbase:HasFiniteAction L fhdiff:HasCompactlySupportedActionVariationDifference L f ηs:ℝhcont:Continuous fun x => actionDensity L (variedField f η s) x - actionDensity L f xhsupp:HasCompactSupport fun x => actionDensity L (variedField f η s) x - actionDensity L f xhsub:Integrable (fun x => actionDensity L (variedField f η s) x - actionDensity L f x) volumehadd:Integrable (fun x => actionDensity L (variedField f η s) x - actionDensity L f x + actionDensity L f x) volume⊢ Integrable (actionDensity L (variedField f η s)) volume d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hbase:HasFiniteAction L fhdiff:HasCompactlySupportedActionVariationDifference L f ηs:ℝhcont:Continuous fun x => L.toFun (jetAt k (variedField f η s) x) + -L.toFun (jetAt k f x)hsupp:HasCompactSupport fun x => L.toFun (jetAt k (variedField f η s) x) + -L.toFun (jetAt k f x)hsub:Integrable (fun x => L.toFun (jetAt k f x)) volumehadd:Integrable (fun x => L.toFun (jetAt k (variedField f η s) x)) volume⊢ Integrable (actionDensity L (variedField f η s)) volume All goals completed! 🐙
@[simp] lemma variedField_apply (f : Space d → EuclideanSpace ℝ (Fin m)) (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) (s : ℝ) (x : Space d) : variedField f η s x = f x + s • η x := rfl@[simp] lemma actionVariation_apply (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) (s : ℝ) : actionVariation L f η s = action L (variedField f η s) := rfld:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))s:ℝx:Space dhf:ContDiff ℝ ∞ fhx:x ∉ tsupport η.toFunhcoords:jetCoordinatesAt k (variedField f η s) x = jetCoordinatesAt k f x⊢ JetPoint.ofBaseCoordinates x (jetCoordinatesAt k (variedField f η s) x) = JetPoint.ofBaseCoordinates x (jetCoordinatesAt k f x) All goals completed! 🐙lemma actionDensity_variedField_eq_of_notMem_tsupport (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) (s : ℝ) {x : Space d} (hf : ContDiff ℝ ∞ f) (hx : x ∉ tsupport η.toFun) : actionDensity L (variedField f η s) x = actionDensity L f x := d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))s:ℝx:Space dhf:ContDiff ℝ ∞ fhx:x ∉ tsupport η.toFun⊢ actionDensity L (variedField f η s) x = actionDensity L f x All goals completed! 🐙d:ℕm:ℕk:ℕL:Lagrangian d m khcontL:L.ContinuousInCoordinatesf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))s:ℝhbaseCont:Continuous (actionDensity L f)hvarCont:Continuous (actionDensity L (variedField f η s))hsupp:(Function.support fun x => actionDensity L (variedField f η s) x - actionDensity L f x) ⊆ tsupport η.toFun⊢ (tsupport fun x => actionDensity L (variedField f η s) x - actionDensity L f x) ⊆ tsupport η.toFun All goals completed! 🐙

C. Critical fields

A field is critical for a local action if every admissible compactly supported variation has vanishing first derivative at s = 0, under the explicit finite-action hypothesis for the varied family.

def IsCritical (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) : Prop := ∀ η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)), HasFiniteActionVariation L f η → HasDerivAt (actionVariation L f η) 0 0