Physlib

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

theorem

variedField(f,η,0)=f\text{variedField}(f, \eta, 0) = f

Let f ⁣:Space dRmf \colon \text{Space } d \to \mathbb{R}^m be a field and η\eta be an admissible variation. Then the varied field variedField(f,η,s)\text{variedField}(f, \eta, s) evaluated at the parameter s=0s = 0 is equal to the original field ff.

theorem

Additivity of variation parameters ss and tt in varied fields

Let f:Space dRmf : \text{Space } d \to \mathbb{R}^m be a field and η:Space dRm\eta : \text{Space } d \to \mathbb{R}^m be an admissible variation. For any real parameters s,tRs, t \in \mathbb{R}, applying a variation with parameter tt to a field that has already been varied by ss is equivalent to applying a single variation with parameter s+ts + t to the original field. That is: (f+sη)+tη=f+(s+t)η (f + s\eta) + t\eta = f + (s + t)\eta In terms of the varied field function, this is expressed as: variedField(variedField(f,η,s),η,t)=variedField(f,η,s+t) \text{variedField}(\text{variedField}(f, \eta, s), \eta, t) = \text{variedField}(f, \eta, s + t)

theorem

If gg is CC^\infty, then ig\partial_i g is CC^\infty

Let g:Space dRg: \text{Space } d \to \mathbb{R} be a function. If gg is infinitely differentiable (CC^\infty), then for any index i{0,,d1}i \in \{0, \dots, d-1\}, its partial derivative ig\partial_i g (the spatial derivative in the direction of the ii-th standard basis vector) is also infinitely differentiable (CC^\infty).

theorem

The spatial derivative of a test function is a test function

Let g:Space dRg: \text{Space } d \to \mathbb{R} be a test function. For any basis index i{0,,d1}i \in \{0, \dots, d-1\}, the spatial derivative ig\partial_i g is also a test function.

theorem

Iterated Partial Derivatives of a CC^\infty Function are CC^\infty

Let g:Space dRg: \text{Space } d \to \mathbb{R} be an infinitely differentiable function (of class CC^\infty). For any finite sequence of indices L=[i1,i2,,in]L = [i_1, i_2, \dots, i_n] where each ij{0,,d1}i_j \in \{0, \dots, d-1\}, the iterated partial derivative i1i2ing \partial_{i_1} \partial_{i_2} \dots \partial_{i_n} g is also infinitely differentiable.

theorem

Iterated partial derivatives of a test function are test functions

Let g:Space dRg: \text{Space } d \to \mathbb{R} be a test function. For any finite list of coordinate indices L=[i1,i2,,ik]L = [i_1, i_2, \dots, i_k] where each ij{0,,d1}i_j \in \{0, \dots, d-1\}, the iterated partial derivative i1i2ikg\partial_{i_1} \partial_{i_2} \dots \partial_{i_k} g is also a test function.

theorem

i\partial_i Commutes with Iterated Partial Derivatives for Smooth Functions

For any smooth function g:Space dRg : \text{Space } d \to \mathbb{R} (where gCg \in C^\infty), any coordinate index i{0,,d1}i \in \{0, \dots, d-1\}, and any list of indices L=[j1,j2,,jn]L = [j_1, j_2, \dots, j_n], the partial derivative i\partial_i commutes with the iterated partial derivatives defined by LL. Specifically: j1j2jn(ig)=i(j1j2jng) \partial_{j_1} \partial_{j_2} \cdots \partial_{j_n} (\partial_i g) = \partial_i (\partial_{j_1} \partial_{j_2} \cdots \partial_{j_n} g) where μ\partial_\mu denotes the spatial derivative in the direction of the μ\mu-th standard basis vector.

theorem

Iterated partial derivatives of the components of an admissible variation are test functions

Let η:Space dRm\eta: \text{Space } d \to \mathbb{R}^m be an admissible variation. For any multi-index II of dimension dd with order Ik|I| \le k and any component index a{0,,m1}a \in \{0, \dots, m-1\}, the function mapping a point xSpace dx \in \text{Space } d to the iterated partial derivative [I]ηa(x)\partial^{[I]} \eta_a(x) is a test function.

theorem

Continuity of LuIa\frac{\partial \mathcal{L}}{\partial u^a_I} implies integrability of the first-variation density term LuIaIηa\frac{\partial \mathcal{L}}{\partial u^a_I} \partial^I \eta^a

Let L\mathcal{L} be a Lagrangian of order kk for fields mapping Rd\mathbb{R}^d to Rm\mathbb{R}^m. Let f:RdRmf: \mathbb{R}^d \to \mathbb{R}^m be a field configuration and η:RdRm\eta: \mathbb{R}^d \to \mathbb{R}^m be an admissible variation. For any multi-index II with Ik|I| \le k and any component index a{0,,m1}a \in \{0, \dots, m-1\}, if the mapping xLuIa(jkf(x))x \mapsto \frac{\partial \mathcal{L}}{\partial u^a_I}(j^k f(x)) is continuous, then the first-variation density term xLuIa(jkf(x))Iηa(x)x \mapsto \frac{\partial \mathcal{L}}{\partial u^a_I}(j^k f(x)) \cdot \partial^I \eta^a(x) is integrable over Rd\mathbb{R}^d. Here, jkf(x)j^k f(x) denotes the kk-jet of the field ff at point xx, and Iηa(x)\partial^I \eta^a(x) is the iterated partial derivative of the aa-th component of the variation η\eta.

theorem

Joint continuity of the jet and base coordinates (x,jk(f+sη)(x))(x, j^k(f + s\eta)(x)) in (s,x)(s, x)

Let d,m,kNd, m, k \in \mathbb{N}. For a smooth (CC^\infty) field f:RdRmf: \mathbb{R}^d \to \mathbb{R}^m and an admissible variation η:RdRm\eta: \mathbb{R}^d \to \mathbb{R}^m, the map (s,x)(x,jk(f+sη)(x))(s, x) \mapsto (x, j^k(f + s\eta)(x)) from R×Rd\mathbb{R} \times \mathbb{R}^d to the space of base-jet coordinates Rd×JetCoordinates(d,m,k)\mathbb{R}^d \times \text{JetCoordinates}(d, m, k) is continuous. Here sRs \in \mathbb{R} is the variation parameter, xRdx \in \mathbb{R}^d is the spatial point, and jk(f+sη)(x)j^k(f + s\eta)(x) denotes the jet coordinates ([I](fa+sηa)(x))Ik,0a<m(\partial^{[I]} (f_a + s\eta_a)(x))_{|I| \le k, 0 \le a < m} of the varied field at xx.