1 Vector Calculus Foundation
This chapter establishes the vector calculus infrastructure on \(\mathbb {R}^3\) built atop Mathlib’s Fréchet derivative fderiv.
1.1 Basic Types
A point or vector in \(\mathbb {R}^3\): the type \(\mathrm{Fin}\, 3 \to \mathbb {R}\).
A scalar field \(f : \mathbb {R}^3 \to \mathbb {R}\).
A vector field \(\mathbf{F} : \mathbb {R}^3 \to \mathbb {R}^3\).
A time-dependent scalar field \(f : \mathbb {R}\to \mathbb {R}^3 \to \mathbb {R}\).
A time-dependent vector field \(\mathbf{F} : \mathbb {R}\to \mathbb {R}^3 \to \mathbb {R}^3\).
1.2 Partial Derivatives
The \(i\)-th standard basis vector \(\mathbf{e}_i = \mathrm{Pi.single}\; i\; 1\).
Partial derivative of a scalar field: \(\frac{\partial f}{\partial x_i}(x) = (\mathrm{fderiv}\; \mathbb {R}\; f\; x)(\mathbf{e}_i)\).
Partial derivative of a vector field component: \(\frac{\partial F_j}{\partial x_i}(x) = (\mathrm{fderiv}\; \mathbb {R}\; (y \mapsto F(y)_j)\; x)(\mathbf{e}_i)\).
Second partial derivative of a scalar field: \(\frac{\partial ^2 f}{\partial x_i^2}\).
Second partial derivative of a vector field component: \(\frac{\partial ^2 F_j}{\partial x_i^2}\).
Time derivative of a time-dependent scalar field: \(\frac{\partial f}{\partial t}(t, x) = \mathrm{deriv}\; (s \mapsto f(s, x))\; t\).
Time derivative of a time-dependent vector field component: \(\frac{\partial F_j}{\partial t}(t, x) = \mathrm{deriv}\; (s \mapsto F(s, x)_j)\; t\).
Second time derivative of a scalar field: \(\frac{\partial ^2 f}{\partial t^2}\).
Second time derivative of a vector field component: \(\frac{\partial ^2 F_j}{\partial t^2}\).
1.3 Vector Calculus Operators
Gradient of a scalar field: \((\nabla f)(x)_i = \frac{\partial f}{\partial x_i}(x)\).
Divergence of a vector field: \((\nabla \! \cdot \! \mathbf{F})(x) = \sum _{i=0}^{2} \frac{\partial F_i}{\partial x_i}(x)\).
Curl of a vector field: \((\nabla \! \times \! \mathbf{F})_k = \varepsilon _{kij}\, \frac{\partial F_j}{\partial x_i}\), defined by explicit pattern matching on the three components.
Scalar Laplacian: \((\nabla ^2_sf)(x) = \sum _{i=0}^{2} \frac{\partial ^2 f}{\partial x_i^2}(x)\).
Vector Laplacian: \((\nabla ^2\mathbf{F})(x)_j = \sum _{i=0}^{2} \frac{\partial ^2 F_j}{\partial x_i^2}(x)\).
1.4 Smoothness Predicates
A scalar field is \(C^2\): \(\mathrm{ContDiff}\; \mathbb {R}\; 2\; f\).
A vector field is \(C^2\): each component \(y \mapsto F(y)_j\) is \(\mathrm{ContDiff}\; \mathbb {R}\; 2\).
1.5 Fundamental Lemma and Vector Identities
For \(C^2\) scalar fields, mixed partial derivatives commute (Clairaut/Schwarz):
Connects to Mathlib’s IsSymmSndFDerivAt via the chain rule for CLM evaluation.
\(\nabla \! \times \! (\nabla f) = 0\) for \(C^2\) scalar fields. Each component \(\frac{\partial }{\partial x_i}\frac{\partial f}{\partial x_j} - \frac{\partial }{\partial x_j}\frac{\partial f}{\partial x_i} = 0\) by symmetry of mixed partials.
\(\nabla \! \cdot \! (\nabla \! \times \! \mathbf{F}) = 0\) for \(C^2\) vector fields. Expands to a sum of mixed partials that cancel pairwise.
\(\nabla \! \times \! (\nabla \! \times \! \mathbf{F}) = \nabla (\nabla \! \cdot \! \mathbf{F}) - \nabla ^2\mathbf{F}\). The critical identity for deriving wave equations. Proved component-by-component using symmetry of mixed partials.
1.6 Curl Linearity
\(C^2\) vector field components are differentiable at every point.
\(\nabla \! \times \! (-\mathbf{F}) = -(\nabla \! \times \! \mathbf{F})\).
\(\nabla \! \times \! (\mathbf{F} + \mathbf{G}) = \nabla \! \times \! \mathbf{F} + \nabla \! \times \! \mathbf{G}\), given differentiability of components.
\(\nabla \! \times \! (c\, \mathbf{F}) = c\, (\nabla \! \times \! \mathbf{F})\), given differentiability of components.