Physlib.Mathematics.VariationalCalculus.HasVarGradient

The proposition `HasVarGradientAt F grad u` states that the function $\text{grad} : X \to U$ is the variational gradient (functional derivative) $\frac{\delta S}{\delta u}$ of a functional $S$ at the point $u : X \to U$. The functional $S$ is defined by the density mapping $F : (X \to U) \to (X \to \mathbb{R})$, where the total functional is given by $S[u] = \int_X F(u)(x) \, d\mu(x)$. This formalizes the relationship where $\text{grad}$ represents the functional derivative $\frac{\delta S}{\delta u}$ evaluated at $u$.

Let $F$ and $F'$ be functional density mappings from $(X \to U)$ to $(X \to \mathbb{R})$. If $F$ has a variational gradient $\text{grad} : X \to U$ at $u : X \to U$, and $F'$ has a variational gradient $\text{grad}' : X \to U$ at $u$, then the sum mapping $F + F'$ (defined by $(F + F')(v)(x) = F(v)(x) + F'(v)(x)$) has the variational gradient $\text{grad} + \text{grad}'$ at $u$. This holds provided that $X$ is a measurable space where the volume measure is finite on compact sets.

Let $\iota$ be a finite index set. Let $F_i : (X \to U) \to (X \to \mathbb{R})$ be a family of functional density mappings for $i \in \iota$. Suppose that for each $i \in \iota$, the mapping $F_i$ has a variational gradient $\text{grad}_i : X \to U$ at $u : X \to U$. Provided that $u$ is $C^\infty$ and $X$ is a measurable space where the volume measure is finite on compact sets, the functional defined by the sum of these densities, $(\sum_{i \in \iota} F_i)(v)(x) = \sum_{i \in \iota} F_i(v)(x)$, has the variational gradient $\sum_{i \in \iota} \text{grad}_i$ at $u$.

Let $F: (X \to U) \to (X \to \mathbb{R})$ be a density mapping defining a functional $S[u] = \int_X F(u)(x) \, d\mu(x)$. If $\text{grad}: X \to U$ is the variational gradient (functional derivative) $\frac{\delta S}{\delta u}$ of $F$ at the point $u$, then the variational gradient of the functional defined by the density mapping $-F$ at $u$ is $-\text{grad}$.

Given a mapping $F: (X \to U) \to (X \to \mathbb{R})$ that represents the integrand of a functional $S[u] = \int_X F(u)(x) \, d\mu(x)$, and a function $u: X \to U$, the variational gradient is the function $g: X \to U$ representing the functional derivative $\frac{\delta S}{\delta u}$ evaluated at $u$. If there exists a function $g$ satisfying the property `HasVarGradientAt F g u`, the definition returns this $g$; otherwise, it returns the zero function $0: X \to U$.

This notation provides a syntax for the variational gradient (functional derivative) of an integral functional. For a function $u$ and an integrand $b$ that depends on $u$ and a spatial variable $x$, the expression $\delta u, \int x, b$ represents the variational gradient of the functional $F[u] = \int b(u, x) \, dx$. Mathematically, this corresponds to the functional derivative $\frac{\delta}{\delta u(x)} \int b(u, x) \, dx$, which is a function of $x$.

This notation $\delta(u := u'), \int x, b$ represents the variational gradient (also known as the functional derivative) of an integral functional $S[u] = \int b(u, x) dx$ with respect to the function $u$, evaluated at a specific function $u = u'$. In this syntax, $u$ is the bound function variable, $u'$ is the point in the function space where the gradient is calculated, $x$ is the integration variable, and $b$ is the integrand expression. The result is a function of $x$ corresponding to the variational derivative $\left. \frac{\delta S}{\delta u} \right|_{u=u'}$.

Let $S' : (X \to U) \to (X \to \mathbb{R})$ be a mapping that defines a functional $S[u] = \int_X S'(u)(x) \, d\mu(x)$. If $\text{grad}$ and $\text{grad}'$ are both variational gradients of $S'$ at the function $u : X \to U$ (i.e., they both satisfy the property $\text{HasVarGradientAt}$ for $S'$ at $u$), then $\text{grad} = \text{grad}'$.

Let $F: (X \to U) \to (X \to \mathbb{R})$ be a density mapping such that the total functional is given by $S[u] = \int_X F(u)(x) \, d\mu(x)$. If $\text{grad}: X \to U$ is a function that satisfies the property of being the variational gradient (functional derivative) of $F$ at the point $u: X \to U$ (i.e., `HasVarGradientAt F grad u` holds), then the variational gradient defined by the operator `varGradient F u` is equal to $\text{grad}$.