Physlib.ClassicalFieldTheory.Local.Variation

This instance defines a coercion that allows an admissible variation $\eta$ (belonging to the type `AdmissibleVariation d U`) to be treated as a function mapping the space $\text{Space}_d$ to the vector space $U$. Specifically, for any point $x \in \text{Space}_d$, the value $\eta(x)$ is defined by the underlying function of the variation.

Let $\eta$ be an admissible variation from the $d$-dimensional Euclidean space $\text{Space}_d$ to a real normed vector space $U$. Then the underlying function of $\eta$ has compact support.

Given an admissible variation $\eta: \text{Space}_d \to U$ (where $\text{Space}_d$ is a $d$-dimensional Euclidean space and $U$ is a real normed vector space), this mapping views $\eta$ as a continuous map with compact support. Since an admissible variation is defined as a smooth function with compact support, it satisfies the requirements to be an element of the space of compactly supported continuous maps $C_c(\text{Space}_d, U)$.

The zero element of the space of admissible variations $\text{AdmissibleVariation}(d, U)$ is the constant function that maps every point $x \in \text{Space}_d$ to the zero vector $0 \in U$. Here, $\text{Space}_d$ is a $d$-dimensional Euclidean space and $U$ is a real normed vector space.

For any point $x$ in the $d$-dimensional Euclidean space $\text{Space}_d$, the zero element of the space of admissible variations $\text{AdmissibleVariation}(d, U)$ evaluates to the zero vector in $U$, i.e., $0(x) = 0$.

For an admissible variation $\eta$ in the space $\text{AdmissibleVariation}(d, U)$, its negation $-\eta$ is defined pointwise by the rule $(-\eta)(x) = -\eta(x)$ for all $x \in \text{Space}(d)$. This negation preserves the properties of being smooth and compactly supported.

Let $\text{AdmissibleVariation}(d, U)$ be the space of smooth, compactly supported maps from $\text{Space}(d)$ to a real normed vector space $U$. For any admissible variation $\eta \in \text{AdmissibleVariation}(d, U)$ and any point $x \in \text{Space}(d)$, the value of the negated variation $-\eta$ at $x$ is equal to the negation of the value of $\eta$ at $x$: $$(-\eta)(x) = -\eta(x)$$

For two admissible variations $\eta, \xi \in \text{AdmissibleVariation}(d, U)$, their sum $\eta + \xi$ is defined by the pointwise addition $(\eta + \xi)(x) = \eta(x) + \xi(x)$ for all $x \in \text{Space } d$. This operation is well-defined as the sum of two smooth, compactly supported functions is itself smooth and compactly supported.

Let $\eta$ and $\xi$ be admissible variations in $\text{AdmissibleVariation}(d, U)$. For any point $x \in \text{Space } d$, the value of their sum $\eta + \xi$ at $x$ is given by the sum of their individual values: $$(\eta + \xi)(x) = \eta(x) + \xi(x)$$

The space of admissible variations $\text{AdmissibleVariation}(d, U)$, consisting of smooth compactly supported maps from $\text{Space } d$ to a real normed vector space $U$, is equipped with a subtraction operation. For two admissible variations $\eta$ and $\xi$, their difference $\eta - \xi$ is defined pointwise by $(\eta - \xi)(x) = \eta(x) - \xi(x)$ for all $x \in \text{Space } d$. This difference is also an admissible variation because the subtraction of two smooth functions with compact support results in a function that is also smooth and compactly supported.

For any two admissible variations $\eta, \xi \in \text{AdmissibleVariation}(d, U)$ and any point $x \in \text{Space } d$, the value of their difference $(\eta - \xi)$ evaluated at $x$ is equal to the difference of their individual values at that point, i.e., $(\eta - \xi)(x) = \eta(x) - \xi(x)$. Here, an admissible variation is a smooth, compactly supported map from the base space to a real normed vector space $U$.

The space of admissible variations $\text{AdmissibleVariation}(d, U)$, which consists of smooth compactly supported maps from $\text{Space } d$ to a real normed vector space $U$, is equipped with a scalar multiplication by real numbers $c \in \mathbb{R}$. For any variation $\eta$ and scalar $c$, the result $c \cdot \eta$ is defined pointwise as $(c \cdot \eta)(x) = c \cdot \eta(x)$.

For any real number $c \in \mathbb{R}$, any admissible variation $\eta$ (a smooth compactly supported map from $\text{Space } d$ to a real normed vector space $U$), and any point $x \in \text{Space } d$, the evaluation of the scalar-multiplied variation $c \cdot \eta$ at $x$ is equal to the scalar multiplication of the value $\eta(x)$ by $c$, that is, $(c \cdot \eta)(x) = c \cdot \eta(x)$.

Let $\eta: \text{Space } d \to \text{Space } m$ be an admissible variation, which is defined as a smooth function with compact support. For any coordinate index $a \in \{0, 1, \dots, m-1\}$, the $a$-th component function $x \mapsto (\eta(x))_a$ is a test function (a smooth real-valued function with compact support).