PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.Support
First variation support lemmas
i. Overview
This module collects the reusable support lemmas used by the analytic part of the local first-variation proof: basic identities for varied fields, iterated derivative regularity for test functions, and continuity of the varied local-jet coordinate map.
ii. Key results
- `ClassicalFieldTheory.Local.variedField_zero`
- `ClassicalFieldTheory.Local.variedField_variedField`
iii. Table of contents
- A. Varied fields
- B. Iterated derivative support lemmas
- C. Varied local-jet coordinates
iv. References
- J. Cortés and A. Haupt, *Lecture Notes on Mathematical Methods of Classical Physics*, Chapter 5, Theorem 5.2.
A. Varied fields
B. Iterated derivative support lemmas
C. Varied local-jet coordinates
10 declarations
Let be a field and be an admissible variation. Then the varied field evaluated at the parameter is equal to the original field .
Additivity of variation parameters and in varied fields
Let be a field and be an admissible variation. For any real parameters , applying a variation with parameter to a field that has already been varied by is equivalent to applying a single variation with parameter to the original field. That is: In terms of the varied field function, this is expressed as:
If is , then is
Let be a function. If is infinitely differentiable (), then for any index , its partial derivative (the spatial derivative in the direction of the -th standard basis vector) is also infinitely differentiable ().
The spatial derivative of a test function is a test function
Let be a test function. For any basis index , the spatial derivative is also a test function.
Iterated Partial Derivatives of a Function are
Let be an infinitely differentiable function (of class ). For any finite sequence of indices where each , the iterated partial derivative is also infinitely differentiable.
Iterated partial derivatives of a test function are test functions
Let be a test function. For any finite list of coordinate indices where each , the iterated partial derivative is also a test function.
Commutes with Iterated Partial Derivatives for Smooth Functions
For any smooth function (where ), any coordinate index , and any list of indices , the partial derivative commutes with the iterated partial derivatives defined by . Specifically: where denotes the spatial derivative in the direction of the -th standard basis vector.
Iterated partial derivatives of the components of an admissible variation are test functions
Let be an admissible variation. For any multi-index of dimension with order and any component index , the function mapping a point to the iterated partial derivative is a test function.
Continuity of implies integrability of the first-variation density term
Let be a Lagrangian of order for fields mapping to . Let be a field configuration and be an admissible variation. For any multi-index with and any component index , if the mapping is continuous, then the first-variation density term is integrable over . Here, denotes the -jet of the field at point , and is the iterated partial derivative of the -th component of the variation .
Joint continuity of the jet and base coordinates in
Let . For a smooth () field and an admissible variation , the map from to the space of base-jet coordinates is continuous. Here is the variation parameter, is the spatial point, and denotes the jet coordinates of the varied field at .
