Physlib.SpaceAndTime.Space.Derivatives.Iterated
Iterated derivatives on `Space d`
i. Overview
This module defines iterated coordinate derivatives on `Space d` indexed by multi-indices.
The implementation is intentionally modest. A multi-index is first expanded into a canonical list of coordinate directions, and the iterated derivative is then defined by repeated application of `Space.deriv` along that list.
ii. Key results
- `Space.iteratedDeriv` : iterated coordinate derivatives on `Space d`. - `∂^[I] f` : notation for the iterated derivative indexed by the multi-index `I`. - `Space.iteratedDeriv_add`, `Space.iteratedDeriv_const_smul` : algebraic compatibility for smooth scalar-valued functions. - `Space.iteratedDeriv_contDiff` : smooth scalar-valued functions remain smooth after iterated coordinate differentiation. - `Space.tsupport_iteratedDeriv_subset` : the support of an iterated spatial derivative is contained in that of the original function.
iii. Table of contents
- A. Iterated derivatives on `Space d`
- B. Algebraic and regularity lemmas
- C. Support lemmas
iv. References
A. Iterated derivatives on `Space d`
12 declarations
Iterated coordinate derivative
Given a natural number , a multi-index , and a function mapping into a real topological vector space , the iterated coordinate derivative is the function obtained by repeatedly applying the partial derivative operator (defined as `Space.deriv`) for each coordinate index in the canonical list associated with . This corresponds to the standard partial derivative of of order indexed by the multi-index , denoted as:
Notation for the iterated derivative
The notation denotes the iterated coordinate derivative operator indexed by a multi-index . For a function , where is a module over , represents the repeated application of the coordinate derivative `Space.deriv` along the directions specified by the multi-index .
Let be a real topological vector space and be a natural number. For any function , the iterated coordinate derivative with respect to the zero multi-index is the function itself:
Let be a real topological vector space and be a function. For any multi-index , the iterated coordinate derivative of indexed by the multi-index incremented at the -th coordinate is given by: where denotes the multi-index , is the iterated coordinate derivative of with respect to , and is the partial derivative with respect to the -th coordinate.
Let be a function mapping into a real topological vector space , and let be a coordinate index. Let denote the unit multi-index with at the -th position and elsewhere (defined as the increment of the zero multi-index at ). Then the iterated coordinate derivative is equal to the spatial derivative in the -th direction .
Let be a natural number and be a multi-index of dimension . For any two infinitely differentiable (smooth) functions , the iterated coordinate derivative of their sum is equal to the sum of their individual iterated coordinate derivatives:
for smooth functions
Let be a natural number and be a multi-index. For any real constant and any smooth function (i.e., ), the iterated coordinate derivative of the scalar multiple satisfies: where denotes the partial derivative operator .
Iterated derivatives of smooth functions are smooth
Let be a natural number and be the -dimensional real inner product space. For any multi-index and any smooth scalar-valued function (i.e., is ), the iterated coordinate derivative is also a smooth function.
Let be a function and be a coordinate index. Let denote the spatial derivative of in the -th coordinate direction. Then the topological support of the spatial derivative is contained in the topological support of the original function:
and commute for smooth functions
Let be an infinitely differentiable (smooth) scalar-valued function. For any coordinate index and any multi-index , the spatial derivative commutes with the iterated multi-index derivative . That is, where is the partial derivative with respect to the -th coordinate and is the iterated coordinate derivative defined by the multi-index .
Let be a natural number and be a multi-index. For any real-valued function , the topological support of its iterated coordinate derivative , defined as is a subset of the topological support of . That is,
for
Let be a natural number and be a multi-index. For any real-valued function and any point , if is not in the topological support of (denoted ), then the iterated coordinate derivative vanishes at : where is defined as:
