Physlib

PhyslibAlpha.ClassicalFieldTheory.Local.JetPointRegularity

Regularity and support for jet-coordinate maps

i. Overview

This module collects the analytic facts about coordinate-level jet maps that are needed later in the local variational argument.

At this stage, it provides:

  • smoothness of jet-coordinate maps of smooth fields,
  • smoothness of the base-plus-coordinate jet map,
  • and vanishing of jet coordinates outside topological support.

ii. Key results

  • `ClassicalFieldTheory.Local.jetCoordinatesAt_contDiff`
  • `ClassicalFieldTheory.Local.jetBaseCoordinates_contDiff`
  • `ClassicalFieldTheory.Local.jetCoordinatesAt_eq_zero_of_notMem_tsupport`
  • `ClassicalFieldTheory.Local.jetDirectionAt_eq_zero_of_notMem_tsupport`

iii. Table of contents

  • A. Smoothness of jet-coordinate maps
  • B. Support and vanishing lemmas

iv. References

A. Smoothness of jet-coordinate maps

B. Support and vanishing lemmas

4 declarations

theorem

Smoothness of the Jet-Coordinate Map of a Smooth Field

Let g:Space d→Rmg: \text{Space } d \to \mathbb{R}^m be a smooth (C∞C^\infty) field. For any natural number kk, the jet-coordinate map x↦jetCoordinatesAt k g(x)x \mapsto \text{jetCoordinatesAt } k \, g(x) is also smooth (C∞C^\infty). This map associates each point x∈Space dx \in \text{Space } d with the collection of jet coordinates (uIa)∣I∣≤k,0≤a<m(u^a_I)_{|I| \le k, 0 \le a < m}, where each coordinate is defined as the partial derivative uIa=∂Iga(x)u^a_I = \partial^I g_a(x) for a multi-index II of order at most kk and field component aa.

theorem

Smoothness of the Base-plus-Jet Coordinate Map for a C∞C^\infty Field

Let g:Rd→Rmg: \mathbb{R}^d \to \mathbb{R}^m be a field. If gg is C∞C^\infty smooth, then for any k∈Nk \in \mathbb{N}, the map that associates each point x∈Rdx \in \mathbb{R}^d with its base coordinate xx and its jet coordinates (uIa)∣I∣≤k,0≤a<m(u^a_I)_{|I| \le k, 0 \le a < m} at xx, given by x↦(x,(∂Iga(x))∣I∣≤k,0≤a<m) x \mapsto \left(x, \left( \partial^I g_a(x) \right)_{|I| \le k, 0 \le a < m} \right) is also C∞C^\infty smooth. Here II denotes a multi-index of order ∣I∣≤k|I| \le k and gag_a denotes the aa-th component of the field gg.

theorem

Jet coordinates vanish outside supp(g)\text{supp}(g)

Let g:Space d→Rmg : \text{Space } d \to \mathbb{R}^m be a field and k∈Nk \in \mathbb{N} be the maximum derivative order. If a point x∈Space dx \in \text{Space } d is not in the topological support of gg (i.e., x∉supp(g)x \notin \text{supp}(g)), then the jet coordinates of order kk of the field gg at xx are zero: jetCoordinatesAt k g x=0\text{jetCoordinatesAt } k \, g \, x = 0 This implies that for all component indices a∈{0,…,m−1}a \in \{0, \dots, m-1\} and all multi-indices II with ∣I∣≤k|I| \le k, the partial derivatives ∂[I]ga(x)\partial^{[I]} g_a(x) vanish.

theorem

jetDirectionAt k g x=0\text{jetDirectionAt } k \, g \, x = 0 for x∉supp(g)x \notin \text{supp}(g)

Let g:Space d→Rmg : \text{Space } d \to \mathbb{R}^m be a field and k∈Nk \in \mathbb{N} be the jet order. If a point x∈Space dx \in \text{Space } d is not in the topological support of gg (denoted x∉supp(g)x \notin \text{supp}(g)), then the kk-th order jet fiber direction of the field gg at xx is zero: jetDirectionAt k g x=0\text{jetDirectionAt } k \, g \, x = 0 This implies that all partial derivatives of the components of gg up to order kk vanish at the point xx.