Physlib.SpaceAndTime.Space.Derivatives.Basic
Derivatives on Space
i. Overview
In this module we define derivatives of functions and distributions on space `Space d`, in the standard directions.
ii. Key results
- `deriv` : The derivative of a function on space in a given direction.
- `distDeriv` : The derivative of a distribution on space in a given direction.
iii. Table of contents
- A. Derivatives of functions on `Space d` - A.1. Basic equalities - A.2. Derivative of the constant function - A.3. Derivative distributes over addition - A.4. Derivative distributes over scalar multiplication - A.5. Two spatial derivatives commute - A.6. Derivative of a component - A.7. Derivative of a component squared - A.8. Derivivatives of components - A.9. Derivative of a norm squared - A.9.1. Differentiability of the norm squared function - A.9.2. Derivative of the norm squared function - A.10. Derivative of the inner product - A.10.1. Differentiability of the inner product function - A.10.2. Derivative of the inner product function - A.10.3. Derivative of the inner product on one side - A.11. Differentiability of derivatives - B. Derivatives of distributions on `Space d` - B.1. The definition - B.2. Basic equality - B.3. Commutation of derivatives
iv. References
A. Derivatives of functions on `Space d`
A.1. Basic equalities
A.2. Derivative of the constant function
A.3. Derivative distributes over addition
A.4. Derivative distributes over scalar multiplication
A.5. Two spatial derivatives commute
A.6. Derivative of a component
A.7. Derivative of a component squared
A.8. Derivivatives of components
A.9. Derivative of a norm squared
#### A.9.1. Differentiability of the norm squared function
#### A.9.2. Derivative of the norm squared function
A.10. Derivative of the inner product
#### A.10.1. Differentiability of the inner product function
#### A.10.2. Derivative of the inner product function
#### A.10.3. Derivative of the inner product on one side
A.11. Differentiability of derivatives
B. Derivatives of distributions on `Space d`
B.1. The definition
B.2. Basic equality
B.3. Commutation of derivatives
39 declarations
Spatial derivative in direction
Given a function , where is a real topological vector space, and a basis index , the spatial derivative is the function that maps each point to the Fréchet derivative of at evaluated in the direction of the -th standard basis vector . This definition corresponds to the partial derivative of with respect to the -th coordinate, denoted as or .
Spatial derivative notation
This definition introduces the mathematical notation as a shorthand for the spatial derivative operator `Space.deriv` in the direction of the -th basis vector. Given a function and an index , the expression denotes the partial derivative of with respect to the -th coordinate direction.
Let be a real topological vector space and be a function. For any basis index and any point , the spatial derivative of at in the direction of the -th standard basis vector is equal to the Fréchet derivative of at evaluated at the -th basis vector : where denotes the Fréchet derivative of at , and is the -th vector of the standard orthonormal basis of .
Let be a real topological vector space and be a function. For any index , the spatial derivative is the function that maps each point to the Fréchet derivative of at evaluated in the direction of the -th standard basis vector . Mathematically, , where denotes the Fréchet derivative of at and is the -th standard orthonormal basis vector of .
Let be a real topological vector space and be a function. For any point and any basis index , the spatial derivative of in the direction at , denoted , is equal to the Fréchet derivative of at evaluated at the -th standard basis vector .
Fréchet Derivative as a Sum of Spatial Derivatives:
Let be a real topological vector space and be a function. For any points , the Fréchet derivative of at evaluated in the direction , denoted , is equal to the sum over all basis indices of the -th coordinate of scaled by the spatial derivative of at in the -th direction: where is the -th component of and is the partial derivative of at with respect to the -th standard basis vector.
Let be a real normed space and be a function. For any point and any basis index , the spatial derivative of in the direction at , denoted , is equal to the manifold derivative of at (with respect to the standard model spaces and ) evaluated at the -th standard basis vector .
Equivalence of Manifold and Fréchet Differentiability on
Let be a dimension and be a real normed vector space. For a function and a point , is manifold-differentiable at with respect to the specific manifold structure `manifoldStructure d` on the domain and the canonical manifold structure on the codomain if and only if is Fréchet differentiable at in the standard sense of real normed spaces.
equals the manifold derivative of under `manifoldStructure`
Let be a real normed space and be a function. For any point and any coordinate index , the spatial derivative of at in the direction is equal to the manifold Fréchet derivative of at applied to the -th standard basis vector . This derivative is taken with respect to the specific manifold structure `Space.manifoldStructure d` on the domain and the canonical manifold structure on the codomain. Mathematically: where is the manifold derivative at , and is the vector in the Euclidean space with at the -th coordinate and elsewhere.
Let be a real normed space and be a natural number representing the dimension of the domain . For any constant value and any basis index , let be the constant function . The spatial derivative of in the direction of the -th basis vector at any point is zero, denoted as .
Let be a real normed space and be a natural number. Let be two functions that are differentiable on . For any basis index , the spatial derivative of the sum of the functions is equal to the sum of their individual spatial derivatives: where denotes the partial derivative with respect to the -th coordinate (the Fréchet derivative evaluated in the direction of the -th standard basis vector).
Let be two differentiable functions. For any basis index of the domain and any coordinate index of the codomain , the spatial derivative of the sum of the -th components of and is equal to the sum of the spatial derivatives of the individual -th components: where denotes the -th component of the vector .
Product rule for spatial derivatives:
Let be a real normed space and be a normed algebra over . For functions and that are differentiable at a point , the spatial derivative in direction of their scalar product satisfies the Leibniz rule: where denotes the partial derivative with respect to the -th standard basis vector.
Let be a real normed space and be a semiring acting on (such that the action commutes with the real scalar multiplication and constant scalar multiplication is continuous). Let be a differentiable function and be a constant. For any index , the spatial derivative in direction (denoted by ) satisfies: where is the derivative of in the direction of the -th standard orthonormal basis vector of .
Let be a differentiable function and be a scalar constant. For any point , coordinate index , and basis index , the spatial derivative in direction (denoted by ) of the -th component of scaled by satisfies: where denotes the -th coordinate of the vector .
Commutativity of spatial derivatives: for functions
Let be a real normed space and be a function. If is twice continuously differentiable (of class ), then for any indices , the spatial derivatives in those directions commute: where denotes the derivative of in the direction of the -th standard orthonormal basis vector of .
For any dimension , given an index and a point in the space , the spatial derivative of the -th coordinate function in the direction of the -th standard basis vector is equal to 1: where denotes the -th component of the vector .
for in
For a given dimension , let and be distinct indices in (i.e., ). For any point in , the spatial derivative of the -th coordinate function with respect to the -th direction is zero: where denotes the -th component of , and denotes the derivative in the direction of the -th standard orthonormal basis vector .
For a given dimension , let and be indices in . For any point in , the spatial derivative of the -th coordinate function with respect to the -th direction is given by: where denotes the -th component of the vector , and denotes the derivative in the direction of the -th standard basis vector.
In a -dimensional space , let and be indices in . For any point , the spatial derivative of the square of the -th coordinate function in the direction of the -th standard basis vector is given by: where denotes the -th component of the vector , and denotes the derivative evaluated in the direction of the -th standard basis vector .
for Euclidean-valued functions
Let be a differentiable function, where the codomain is the -dimensional Euclidean space. For any point , any domain basis index , and any codomain component index , the spatial derivative of the -th component of in the direction is equal to the -th component of the spatial derivative of in the direction . That is,
for Lorentz-valued functions
Let be a differentiable function. For any spatial coordinate index and any Lorentz vector component index , the spatial derivative of the -th component of at a point is equal to the -th component of the spatial derivative of at . Mathematically, where denotes the derivative with respect to the -th standard basis vector of .
is differentiable on
In the -dimensional real vector space , the function mapping each element to the square of its Euclidean norm, , is differentiable over .
In the -dimensional real inner product space , for any point and any basis index , the spatial derivative of the squared Euclidean norm function in the direction of the -th basis vector at is equal to . Mathematically, where denotes the -th component of the vector , and denotes the spatial derivative in the direction of the -th standard basis vector .
is Differentiable on
For any dimension , the function mapping an element of the -dimensional real inner product space to its inner product with itself is differentiable over the real numbers .
is Differentiable at
For any dimension and any element of the -dimensional real inner product space , the function mapping to the inner product is differentiable at over the real numbers .
Differentiability of at
Let be a real normed space and be a natural number. Suppose are functions. If and are differentiable at a point , then the scalar-valued function mapping to the inner product is differentiable at .
The inner product of differentiable functions on Space is differentiable
Let be a real normed space and be a natural number. If the functions and are differentiable, then the function mapping each to the inner product is also differentiable.
The function is on
For any dimension and any , the function on the -dimensional space that maps a vector to its inner product with itself, , is -times continuously differentiable () over the real numbers .
The inner product of two functions is
Let be a real normed vector space and be a natural number. Let denote the -dimensional real inner product space where the inner product of two vectors is given by . If and are -times continuously differentiable functions (of class ) for , then the mapping is also an -times continuously differentiable function from to .
In the -dimensional real inner product space , for any point and any basis index , the spatial derivative of the function in the direction of the -th standard basis vector at is equal to . Mathematically, where denotes the real inner product and denotes the -th component of the vector .
For any dimension , let and be vectors in the -dimensional real inner product space . For any basis index , the spatial derivative of the function in the direction of the -th standard basis vector, evaluated at the point , is equal to the -th component of :
Let be a -dimensional real inner product space. For any vectors and any basis index , let be the function defined by . The spatial derivative of in the direction of the -th standard basis vector at the point is equal to the -th component of :
The Partial Derivative of a Function is Differentiable
Let be a real normed space and be a function. If is twice continuously differentiable (), then for any index , the spatial derivative is differentiable. Here, denotes the partial derivative of in the direction of the -th standard basis vector of .
If is , then is
Let be a function. If is continuously differentiable of order (), then the function that maps each point to the collection of its spatial partial derivatives is continuously differentiable of order (). Here, is a -dimensional real inner product space, and denotes the derivative of in the direction of the -th vector of the standard orthonormal basis.
Distributional partial derivative on
Let be a -dimensional real inner product space and be a real normed vector space. Given an index , the operator is an -linear map that sends a distribution to its partial derivative in the direction of the -th standard basis vector . This derivative is defined by composing the distributional Fréchet derivative with the evaluation map at , representing the directional derivative .
for distributions
Let be a -dimensional real inner product space and be a real normed vector space. Let be the standard orthonormal basis of . For a distribution , an index , and a Schwartz test function , the evaluation of the distributional partial derivative at is equal to the distributional Fréchet derivative evaluated at and applied to the basis vector :
for Schwartz Functions
For a Schwartz function on a -dimensional real inner product space, let be the standard orthonormal basis of . For any point and any indices , the mixed partial derivatives of commute: where denotes the directional derivative in the direction of the -th basis vector .
Commutativity of Distributional Partial Derivatives
Let be a -dimensional real inner product space and be a real normed vector space. For any -valued distribution and any indices , the distributional partial derivatives with respect to the standard basis vectors commute: where denotes the operator `distDeriv i` acting on the space of distributions.
