Physlib.SpaceAndTime.Space.Derivatives.Grad

For a real-valued function $f: \text{Space } d \to \mathbb{R}$, the gradient $\nabla f$ is a vector field mapping each point $x \in \text{Space } d$ to an element of the Euclidean space $\mathbb{R}^d$. The $i$-th component of the gradient at point $x$ is given by the partial derivative of $f$ with respect to the $i$-th spatial coordinate, denoted as $\partial_i f(x)$ or $\frac{\partial f}{\partial x_i}(x)$.

The notation $\nabla$ is introduced to represent the gradient operator `grad`. For a function $f : \text{Space } d \to \mathbb{R}$, $\nabla f$ denotes the gradient of $f$, which is a vector field mapping points in $\text{Space } d$ to the Euclidean space $\mathbb{R}^d$.

The gradient of the zero function $f: \text{Space } d \to \mathbb{R}$ (defined by $f(x) = 0$ for all $x \in \text{Space } d$) is the zero vector field, denoted as $\nabla 0 = 0$.

Let $f_1, f_2: \text{Space } d \to \mathbb{R}$ be two real-valued functions that are differentiable on $\text{Space } d$. The gradient of the sum of these functions is equal to the sum of their individual gradients: $$\nabla (f_1 + f_2) = \nabla f_1 + \nabla f_2$$ where $\nabla$ denotes the gradient operator.

For any real constant $c$, the gradient of the constant function $f: \text{Space } d \to \mathbb{R}$ defined by $f(x) = c$ is the zero vector field, denoted as $\nabla f = 0$.

For a differentiable function $f: \text{Space } d \to \mathbb{R}$ and a real scalar $k \in \mathbb{R}$, the gradient of the scalar multiplication of $k$ and $f$ is equal to $k$ times the gradient of $f$: \[ \nabla (k \cdot f) = k \cdot \nabla f \] where $\nabla$ denotes the gradient operator.

For any real-valued function $f: \text{Space } d \to \mathbb{R}$, the gradient of the negation of $f$ is equal to the negation of the gradient of $f$: \[ \nabla (-f) = -\nabla f \] where $\nabla$ denotes the gradient operator.

For any real-valued function $f: \text{Space } d \to \mathbb{R}$ and any point $x \in \text{Space } d$, the gradient $\nabla f(x)$ is equal to the sum over all coordinates $i \in \{0, \dots, d-1\}$ of the partial derivative of $f$ at $x$ in the $i$-th direction, $\partial_i f(x)$, multiplied by the $i$-th standard basis vector $\mathbf{e}_i$: \[ \nabla f(x) = \sum_{i=0}^{d-1} \partial_i f(x) \mathbf{e}_i \] where $\partial_i f(x)$ corresponds to the spatial derivative `deriv i f x` and $\mathbf{e}_i$ corresponds to the unit vector `EuclideanSpace.single i 1`.

For any real-valued function $f: \text{Space } d \to \mathbb{R}$ and any point $x \in \text{Space } d$, the $i$-th component of the gradient vector $\nabla f(x)$ (where $i \in \{0, \dots, d-1\}$) is equal to the partial derivative of $f$ at $x$ with respect to the $i$-th coordinate, denoted as $\partial_i f(x)$ or $\frac{\partial f}{\partial x_i}(x)$.

For a real-valued function $f: \text{Space } d \to \mathbb{R}$ and a point $x \in \text{Space } d$, the inner product of the gradient $\nabla f(x)$ with the $i$-th standard basis vector $e_i$ (where $e_i$ is the vector with $1$ at the $i$-th component and $0$ elsewhere) is equal to the partial derivative of $f$ at $x$ with respect to the $i$-th coordinate, denoted as $\partial_i f(x)$. Mathematically, this is expressed as: $$\langle \nabla f(x), e_i \rangle = \partial_i f(x)$$

For a real-valued function $f: \text{Space } d \to \mathbb{R}$, a point $x \in \text{Space } d$, and a vector $y \in \mathbb{R}^d$, the inner product of the gradient $\nabla f(x)$ and the vector $y$ is equal to the sum over all coordinate indices $i$ of the product of the $i$-th component of $y$ and the partial derivative of $f$ at $x$ with respect to the $i$-th coordinate. Mathematically, this is expressed as: $$\langle \nabla f(x), y \rangle = \sum_i y_i \partial_i f(x)$$ where $\partial_i f(x)$ (or $\frac{\partial f}{\partial x_i}(x)$) is the spatial derivative of $f$ at $x$ in the direction of the $i$-th standard basis vector.

For a real-valued function $f: \text{Space } d \to \mathbb{R}$, a vector $x \in \mathbb{R}^d$, and a point $y \in \text{Space } d$, the inner product of $x$ and the gradient $\nabla f(y)$ is equal to the sum over all coordinate indices $i$ of the product of the $i$-th component of $x$ and the partial derivative of $f$ at $y$ with respect to the $i$-th coordinate. Mathematically, this is expressed as: $$\langle x, \nabla f(y) \rangle = \sum_i x_i \partial_i f(y)$$ where $x_i$ is the $i$-th component of $x$ and $\partial_i f(y)$ (also denoted as $\frac{\partial f}{\partial x_i}(y)$) is the spatial derivative of $f$ at $y$ in the direction of the $i$-th standard basis vector.

Let $f: \text{Space } d \to \mathbb{R}$ be a real-valued function. For any points $x, y \in \text{Space } d$, the inner product between the gradient of $f$ at $x$ and the coordinate representation of $y$ with respect to the standard orthonormal basis is equal to the Fréchet derivative of $f$ at $x$ evaluated in the direction $y$: $$\langle \nabla f(x), \text{repr}(y) \rangle = Df(x)(y)$$ where $\nabla f(x)$ is the gradient vector in $\mathbb{R}^d$, $\text{repr}(y)$ is the coordinate vector of $y$, and $Df(x)(y)$ (denoted in Lean as `fderiv ℝ f x y`) is the Fréchet derivative.

Let $f: \text{Space } d \to \mathbb{R}$ be a real-valued function. For any points $x, y \in \text{Space } d$, the inner product between the coordinate representation of $x$ (with respect to the standard orthonormal basis) and the gradient of $f$ at $y$ is equal to the Fréchet derivative of $f$ at $y$ evaluated in the direction $x$: $$\langle \text{repr}(x), \nabla f(y) \rangle = Df(y)(x)$$ where $\text{repr}(x)$ is the vector in $\mathbb{R}^d$ representing $x$, $\nabla f(y)$ is the gradient vector of $f$ at $y$, and $Df(y)(x)$ (denoted as `fderiv ℝ f y x`) is the Fréchet derivative.

For a real-valued function $f : \text{Space } d \to \mathbb{R}$, let $\nabla f$ be the gradient of $f$ that maps each point in $\text{Space } d$ to a coordinate vector in the Euclidean space $\mathbb{R}^d$. Let $\text{gradient } f$ be the gradient of $f$ as defined in Mathlib (the vector in $\text{Space } d$ associated with the Fréchet derivative via the Riesz representation theorem). Let $\text{repr} : \text{Space } d \to \mathbb{R}^d$ be the isometric isomorphism that maps a vector to its coordinates with respect to the standard orthonormal basis of $\text{Space } d$. Then the gradient $\nabla f$ is equal to the composition of the coordinate representation map and the Mathlib gradient: $$\nabla f = \text{repr} \circ \text{gradient } f$$

For a real-valued function $f : \text{Space } d \to \mathbb{R}$, let $\text{gradient } f$ be the gradient of $f$ as defined in Mathlib (the vector in $\text{Space } d$ associated with the Fréchet derivative via the Riesz representation theorem). Let $\nabla f$ be the gradient operator that maps each point in $\text{Space } d$ to its coordinate vector in the Euclidean space $\mathbb{R}^d$. Let $\text{repr}^{-1} : \mathbb{R}^d \to \text{Space } d$ be the inverse of the isometric isomorphism that maps a vector to its coordinates with respect to the standard orthonormal basis of $\text{Space } d$. Then the Mathlib gradient is equal to the composition of the inverse coordinate representation map and the coordinate-based gradient $\nabla f$: $$\text{gradient } f = \text{repr}^{-1} \circ \nabla f$$

For any dimension $d$ and any real-valued function $f: \text{Space } d \to \mathbb{R}$, the gradient of $f$ at a point $x \in \text{Space } d$ is equal to the sum over all indices $i \in \{0, \dots, d-1\}$ of the partial derivative of $f$ in the direction of the $i$-th standard basis vector, multiplied by that basis vector: $$\text{grad } f(x) = \sum_{i=0}^{d-1} \partial_i f(x) \mathbf{e}_i$$ where $\partial_i f(x)$ is the spatial derivative `deriv i f x` and $\mathbf{e}_i$ is the $i$-th orthonormal basis vector `basis i`.

Let $d$ be a natural number and $\mathbb{R}^d$ be the $d$-dimensional Euclidean space. For any function $f: \mathbb{R}^d \to \mathbb{R}$ and any point $x \in \mathbb{R}^d$, the gradient of $f$ at $x$ is equal to the sum of its directional derivatives along the standard basis vectors $\mathbf{e}_i$ multiplied by those basis vectors: $$\nabla f(x) = \sum_{i} (D f(x) \cdot \mathbf{e}_i) \mathbf{e}_i$$ where $\mathbf{e}_i$ is the $i$-th standard basis vector (defined as `EuclideanSpace.single i 1`) and $D f(x)$ denotes the Fréchet derivative of $f$ at $x$.

Let $d$ be a natural number, $f: \text{Space } d \to \mathbb{R}$ be a differentiable function, and $x \in \text{Space } d$ be a point. The inner product of the gradient $\nabla f(x)$ with the unit vector in the direction of $x$ (represented by $\|x\|^{-1} \cdot \text{basis.repr } x$) is equal to the derivative of the function $r \mapsto f(r \cdot \frac{x}{\|x\|})$ evaluated at $r = \|x\|$. Mathematically, this is expressed as: \[ \left\langle \nabla f(x), \frac{1}{\|x\|} \text{basis.repr } x \right\rangle = \left. \frac{d}{dr} f\left( r \frac{x}{\|x\|} \right) \right|_{r = \|x\|} \] where $\nabla f(x)$ is the gradient of $f$ at $x$, $\|x\|$ is the Euclidean norm, and $\text{basis.repr } x$ is the coordinate representation of $x$ in $\mathbb{R}^d$.

Let $d$ be a natural number, $f: \text{Space } d \to \mathbb{R}$ be a differentiable function, and $x \in \text{Space } d$ be a point. The inner product of the gradient $\nabla f(x)$ with the coordinate representation of $x$ (denoted $\text{basis.repr } x$) is equal to the norm $\|x\|$ multiplied by the radial derivative of $f$ evaluated at $x$. Mathematically, this is expressed as: \[ \left\langle \nabla f(x), \text{basis.repr } x \right\rangle = \|x\| \cdot \left. \frac{d}{dr} f\left( r \frac{x}{\|x\|} \right) \right|_{r = \|x\|} \] where $\nabla f(x)$ is the gradient of $f$ at $x$, $\|x\|$ is the Euclidean norm, and $\text{basis.repr } x$ is the representation of $x$ as a vector in the Euclidean space $\mathbb{R}^d$.

For any point $x$ in the $d$-dimensional real inner product space $\text{Space } d$, the gradient of the squared norm function $x \mapsto \|x\|^2$ evaluated at $x$ is equal to twice the coordinate representation of $x$ with respect to the standard orthonormal basis: \[ \nabla (\|x\|^2) = 2 \cdot \text{basis.repr } x \] where $\|x\|$ denotes the Euclidean norm and $\text{basis.repr } x$ is the vector in $\mathbb{R}^d$ whose components are the coordinates of $x$.

For any dimension $d$, the gradient of the function $f: \text{Space } d \to \mathbb{R}$ defined by $f(y) = \langle y, y \rangle$ is the vector field that maps each point $z \in \text{Space } d$ to twice its coordinate representation in the standard orthonormal basis. That is, $\nabla (\langle y, y \rangle) (z) = 2 \cdot \text{basis.repr } z$, where $\langle \cdot, \cdot \rangle$ denotes the real inner product and $\text{basis.repr}$ is the isometric isomorphism from $\text{Space } d$ to the Euclidean space $\mathbb{R}^d$.

For any dimension $d$ and a fixed vector $x$ in the $d$-dimensional real inner product space $\text{Space } d$, the gradient of the real-valued function $y \mapsto \langle y, x \rangle$ is the constant vector field whose value at any point is the coordinate representation of $x$ with respect to the standard orthonormal basis. That is: \[ \nabla (\langle y, x \rangle) = \text{basis.repr } x \] where $\langle \cdot, \cdot \rangle$ denotes the real inner product and $\text{basis.repr}$ is the isometric isomorphism mapping a vector in $\text{Space } d$ to its coordinates in the Euclidean space $\mathbb{R}^d$.

For any dimension $d \in \mathbb{N}$ and a fixed vector $x \in \text{Space } d$, the gradient of the real-valued function $y \mapsto \langle x, y \rangle$ is the constant vector field whose value at any point is the coordinate representation of $x$ with respect to the standard orthonormal basis. That is: \[ \nabla (\langle x, y \rangle) = \text{basis.repr } x \] where $\langle \cdot, \cdot \rangle$ denotes the real inner product on $\text{Space } d$ and $\text{basis.repr}$ is the isometric isomorphism mapping a vector in $\text{Space } d$ to its coordinates in the Euclidean space $\mathbb{R}^d$.

Let $d = n + 1$ for some natural number $n$. If $f: \text{Space } d \to \mathbb{R}^d$ is a distribution-bounded function and $\eta: \text{Space } d \to \mathbb{R}$ is a Schwartz function, then the function $x \mapsto \langle f(x), \nabla \eta(x) \rangle$ is integrable over $\text{Space } d$ with respect to the volume measure, where $\nabla \eta$ denotes the gradient of $\eta$ and $\langle \cdot, \cdot \rangle$ denotes the standard inner product.

Let $d = n + 1$ for some natural number $n$. Suppose $f: \text{Space } d \to \mathbb{R}^d$ is a distribution-bounded function and $\eta: \text{Space } d \to \mathbb{R}$ is a Schwartz function. Let $\Phi: \text{Space } d \setminus \{0\} \to S^{d-1} \times (0, \infty)$ be the homeomorphism mapping a vector to its spherical coordinates (the direction on the unit sphere $S^{d-1}$ and the radial distance). Then the function mapping $x \mapsto \langle f(x), \nabla \eta(x) \rangle$, when transformed into spherical coordinates via $\Phi^{-1}$, is integrable with respect to the product measure $\sigma \otimes \mu$, where $\sigma$ is the measure on the unit sphere $S^{d-1}$ and $\mu$ is the radial measure on $(0, \infty)$ with density $r^{d-1}$ relative to the Lebesgue measure.

Let $f: \text{Space} \to \mathbb{R}$ be a function. If $f$ is continuously differentiable of order $n+1$ ($C^{n+1}$), then its gradient field $\nabla f$, which maps each point $x$ to the vector of its partial derivatives, is continuously differentiable of order $n$ ($C^n$).

Let $V = \text{Space } d$ be a $d$-dimensional real inner product space. The distributional gradient operator is a linear map that transforms a scalar-valued distribution $f \in \mathcal{D}'(V, \mathbb{R})$ into a vector-valued distribution $\nabla f \in \mathcal{D}'(V, \mathbb{R}^d)$. For a distribution $f$, its gradient is defined by taking its distributional Fréchet derivative $Df$ (which is a distribution valued in the dual space $V^*$), applying the Riesz representation theorem to identify $V^*$ with $V$ via the inner product, and then mapping the resulting vector to its coordinate representation in $\mathbb{R}^d$ using the standard orthonormal basis. Specifically, for a test function $\eta$ and a vector $y \in \mathbb{R}^d$, the gradient satisfies the relation $\langle (\nabla f) \eta, y \rangle = (Df) \eta (\mathbf{b}^{-1}(y))$, where $\mathbf{b}^{-1}$ is the inverse basis representation.

Let $V = \text{Space } d$ be a $d$-dimensional real inner product space equipped with a standard orthonormal basis representation $\mathbf{b} : V \to \mathbb{R}^d$. For a scalar-valued distribution $f \in \mathcal{D}'(V, \mathbb{R})$, a Schwartz test function $\eta \in \mathcal{S}(V, \mathbb{R})$, and a vector $y \in \mathbb{R}^d$, the inner product of the distributional gradient evaluation $(\nabla f)(\eta)$ with $y$ is equal to the evaluation of the distributional Fréchet derivative $(Df)(\eta)$ on the vector $\mathbf{b}^{-1}(y) \in V$. That is, $$\langle (\nabla f)(\eta), y \rangle_{\mathbb{R}^d} = ((Df)(\eta))(\mathbf{b}^{-1}(y))$$ where $\mathbf{b}^{-1}$ is the inverse of the basis representation mapping.

Let $V = \text{Space } d$ be a $d$-dimensional real inner product space and let $\mathbf{b} : V \to \mathbb{R}^d$ be its standard orthonormal basis representation. Let $f \in \mathcal{D}'(V, \mathbb{R})$ be a scalar-valued distribution and $g \in \mathcal{D}'(V, \mathbb{R}^d)$ be a vector-valued distribution. If for every Schwartz test function $\eta \in \mathcal{S}(V, \mathbb{R})$ and every vector $y \in V$, the distributional Fréchet derivative $Df$ satisfies the relation: $$(Df)(\eta)(y) = \langle g(\eta), \mathbf{b}(y) \rangle_{\mathbb{R}^d}$$ where $\langle \cdot, \cdot \rangle_{\mathbb{R}^d}$ is the standard Euclidean inner product, then the distributional gradient of $f$ is equal to $g$ ($\nabla f = g$).

Let $V = \text{Space } d$ be a $d$-dimensional real inner product space equipped with a standard orthonormal basis $\{\mathbf{e}_i\}_{i \in \{0, \dots, d-1\}}$. For any scalar-valued distribution $f \in \mathcal{D}'(V, \mathbb{R})$ and any Schwartz test function $\eta \in \mathcal{S}(V, \mathbb{R})$, the evaluation of the distributional gradient $(\nabla f)(\eta) \in \mathbb{R}^d$ is given by the sum: $$(\nabla f)(\eta) = \sum_i -f(\partial_{\mathbf{e}_i} \eta) \mathbf{\hat{e}}_i$$ where $\partial_{\mathbf{e}_i} \eta$ is the directional derivative of the test function $\eta$ in the direction of the $i$-th basis vector $\mathbf{e}_i$, and $\mathbf{\hat{e}}_i$ denotes the $i$-th standard basis vector of the Euclidean space $\mathbb{R}^d$.

Let $V = \text{Space } d$ be a $d$-dimensional real inner product space. For any scalar-valued distribution $f \in \mathcal{D}'(V, \mathbb{R})$ and any Schwartz test function $\epsilon \in \mathcal{S}(V, \mathbb{R})$, the evaluation of the distributional gradient $(\nabla f)(\epsilon)$ is the vector in $\mathbb{R}^d$ whose components are the distributional partial derivatives of $f$ evaluated at $\epsilon$. Mathematically, this is expressed as: $$((\nabla f)(\epsilon))_i = (\partial_i f)(\epsilon)$$ for each $i \in \{0, \dots, d-1\}$, where $\nabla$ is the distributional gradient operator `distGrad` and $\partial_i$ is the $i$-th distributional partial derivative operator `distDeriv i`.

Let $V = \text{Space } d$ be a $d$-dimensional real inner product space. For any scalar-valued distribution $f \in \mathcal{D}'(V, \mathbb{R})$ and any Schwartz test function $\epsilon \in \mathcal{S}(V, \mathbb{R})$, the evaluation of the distributional gradient $(\nabla f)(\epsilon)$ is the vector in $\mathbb{R}^d$ whose $i$-th component is the $i$-th distributional partial derivative of $f$ evaluated at $\epsilon$. Mathematically, this is expressed as: $$((\nabla f)(\epsilon))_i = (\partial_i f)(\epsilon)$$ for each $i \in \{0, \dots, d-1\}$, where $\nabla$ is the distributional gradient operator and $\partial_i$ is the $i$-th distributional partial derivative operator.

The definition `gradSchwartz` represents the gradient operator as a continuous linear map from the space of real-valued Schwartz functions $\mathcal{S}(\text{Space } d, \mathbb{R})$ to the space of vector-valued Schwartz functions $\mathcal{S}(\text{Space } d, \mathbb{R}^d)$. For a given Schwartz function $\eta$, the map returns the vector field $\nabla \eta$, where the component in the direction of the $i$-th basis vector is the partial derivative of $\eta$ with respect to that coordinate.

For any real-valued Schwartz function $\eta \in \mathcal{S}(\text{Space } d, \mathbb{R})$ and any point $x \in \text{Space } d$, the value of the Schwartz gradient operator applied to $\eta$ at $x$, denoted $\text{gradSchwartz}(\eta)(x)$, is equal to the standard gradient $\nabla \eta(x)$.