Physlib.SpaceAndTime.Space.Derivatives.Curl
Curl on Space
i. Overview
In this module we define the curl of functions and distributions on 3-dimensional space `Space 3`.
We also prove some basic vector-identities involving of the curl operator.
ii. Key results
- `curl` : The curl operator on functions from `Space 3` to `EuclideanSpace ℝ (Fin 3)`.
- `distCurl` : The curl operator on distributions from `Space 3` to `EuclideanSpace ℝ (Fin 3)`.
- `div_of_curl_eq_zero` : The divergence of the curl of a function is zero.
- `distCurl_distGrad_eq_zero` : The curl of the gradient of a distribution is zero.
iii. Table of contents
- A. The curl on functions - A.1. The curl on the zero function - A.2. The curl on a constant function - A.3. Basic operations on curl - A.4. The curl of a linear map is a linear map - A.5. Preliminary lemmas about second derivatives - A.6. The div of a curl is zero - A.7. The curl of a grad is zero - A.8. The curl of a curl - B. The curl on distributions - B.1. The components of the curl - B.2. Basic equalities - B.3. The curl of a grad is zero
iv. References
A. The curl on functions
A.1. The curl on the zero function
A.2. The curl on a constant function
A.3. Basic operations on curl
A.4. The curl of a linear map is a linear map
A.5. Preliminary lemmas about second derivatives
A.6. The div of a curl is zero
A.7. The curl of a grad is zero
A.8. The curl of a curl
B. The curl on distributions
B.1. The components of the curl
B.2. Basic equalities
B.3. The curl of a grad is zero
20 declarations
Curl operator
For a vector field , the curl operator is defined as the function mapping each point to a vector in whose components are: where denotes the -th component of the vector field , and denotes the partial derivative with respect to the -th coordinate (using 0-based indexing for ).
Notation for the curl operator
The notation is defined to represent the curl of a function , where denotes the curl operator `curl`.
The curl of the zero vector field , where for all , is equal to the zero vector field. This is denoted as .
The curl of a constant vector field is zero
For any constant vector , let be the constant vector field defined by for all . Then the curl of is zero, denoted as .
Let be two differentiable vector fields. The curl of the sum of these vector fields is equal to the sum of their individual curls:
for constant
Let be a differentiable vector field and be a scalar constant. The curl of the vector field scaled by is equal to times the curl of : where denotes the curl operator and is the scalar multiplication of the vector field.
Let be a differentiable vector field. The curl of the negative of the vector field is equal to the negative of the curl of : where denotes the curl operator.
Let be two differentiable vector fields. The curl of the difference of these vector fields is equal to the difference of their individual curls: where denotes the curl operator.
The curl of a linear map is a linear map
Let be a vector space over . Suppose is a linear map such that for every , the vector field is differentiable. Then the mapping , which assigns each to the curl of the vector field , is also a linear map over .
Distributivity of Second-Order Partial Derivatives over Addition of Component Derivatives
Let be a twice continuously differentiable () function. Let denote the -th component of the function and denote the partial derivative with respect to the -th coordinate. For any indices , the second-order partial derivatives distribute over the sum of the coordinate-wise derivatives:
Let be a twice continuously differentiable () vector field. For any coordinate indices , the partial derivative with respect to the -th coordinate of the difference between the partial derivatives and is equal to the difference of the second-order partial derivatives: where denotes the spatial derivative in the direction of the -th standard basis vector and denotes the -th component of the vector field . This identity demonstrates that second-order partial derivatives distribute coordinate-wise over the subtraction of terms typically found in the components of a curl.
for vector fields
For any twice continuously differentiable () vector field , the divergence of its curl is identically zero, i.e., .
The curl of a gradient is zero:
Let be a scalar field that is twice continuously differentiable (). The curl of its gradient is the zero vector field: where denotes the gradient of and denotes the curl operator.
Vector identity
Let be a twice continuously differentiable () vector field. The curl of the curl of is equal to the gradient of the divergence of minus the vector Laplacian of : where denotes the curl operator, denotes the divergence, denotes the gradient operator, and denotes the vector Laplacian.
Curl operator for distributions on
The linear map `distCurl` computes the curl of a distribution . It is defined as the composition of the distributional Fréchet derivative with a linear operator that extracts the curl components. For a distribution mapping the 3-dimensional Euclidean space to , the components of the resulting distribution are given by: \begin{align*} (\nabla \times f)_0 &= \partial_2 f_1 - \partial_1 f_2 \\ (\nabla \times f)_1 &= \partial_0 f_2 - \partial_2 f_0 \\ (\nabla \times f)_2 &= \partial_1 f_0 - \partial_0 f_1 \end{align*} where denotes the distributional partial derivative with respect to the -th coordinate of .
Evaluation of the -th Component of Distributional Curl
Let be an -valued distribution on the 3-dimensional Euclidean space , and let be a Schwartz test function. Let be the standard orthonormal basis of . The evaluation of the -th component (index 0) of the distributional curl at the test function is given by where denotes the directional derivative of the test function in the direction of the basis vector , and represents the -th component of the vector obtained by applying the distribution to a test function .
Evaluation of the -st Component of Distributional Curl
Let be an -valued distribution on and be a Schwartz test function. The evaluation of the -st component (index 1) of the distributional curl at is given by where denotes the partial derivative of with respect to the -th coordinate, and represents the -th component of the vector result obtained by applying the distribution to a test function .
Third component of the distributional curl:
Let be a distribution on the 3-dimensional Euclidean space and be a Schwartz test function. Let be the standard orthonormal basis of . The third component (index 2) of the distributional curl applied to the test function is given by where denotes the directional derivative of in the direction of the basis vector , and denotes the -th component of the vector-valued distribution applied to a test function.
Evaluation of Distributional Curl
Let be an -valued distribution on the 3-dimensional Euclidean space , and let be a Schwartz test function. The value of the distributional curl applied to is a vector in whose components are given by: \begin{align*} ((\nabla \times f) \eta)_0 &= -f(\partial_{2} \eta)_1 + f(\partial_{1} \eta)_2 \\ ((\nabla \times f) \eta)_1 &= -f(\partial_{0} \eta)_2 + f(\partial_{2} \eta)_0 \\ ((\nabla \times f) \eta)_2 &= -f(\partial_{1} \eta)_0 + f(\partial_{0} \eta)_1 \end{align*} where denotes the partial derivative of the test function with respect to the -th coordinate, and denotes the -th component of the vector obtained by applying the distribution to a test function .
for distributions
Let be a real-valued distribution on the 3-dimensional Euclidean space . The distributional curl of the distributional gradient of is the zero distribution, denoted by: where is the distributional gradient and is the distributional curl operator.
