Physlib.SpaceAndTime.Space.DistOfFunction

Let $f: \text{Space } d \to F$ be a function from a $d$-dimensional Euclidean space to a normed space $F$. If $f$ satisfies the distribution-boundedness condition `IsDistBounded f` (meaning $f$ is measurable and its growth is bounded by a polynomial), then `distOfFunction f hf` is the $F$-valued distribution on $\text{Space } d$ (an element of the distribution space $(\text{Space } d) \to_d[\mathbb{R}] F$) defined by its action on a Schwartz test function $\eta \in \mathcal{S}(\text{Space } d, \mathbb{R})$ as the integral: \[ \eta \mapsto \int_{\text{Space } d} \eta(x) \cdot f(x) \, dx \] where $\cdot$ denotes the scalar multiplication of the vector $f(x) \in F$ by the real value $\eta(x)$.

Let $f: \text{Space } d \to F$ be a function from a $d$-dimensional Euclidean space to a normed space $F$. If $f$ is distribution-bounded (satisfying the property `IsDistBounded f`), then for any Schwartz test function $\eta \in \mathcal{S}(\text{Space } d, \mathbb{R})$, the distribution associated with $f$ (denoted by `distOfFunction f hf`) acts on $\eta$ according to the integral: $$(\text{distOfFunction } f)(\eta) = \int_{\text{Space } d} \eta(x) f(x) \, dx$$ where $\eta(x) f(x)$ denotes the scalar multiplication of the vector $f(x) \in F$ by the real value $\eta(x)$.

For any natural number $d$, the distribution associated with the constant zero function $f: \text{Space } d \to F$ (defined by $f(x) = 0$ for all $x$) is equal to the zero distribution.

Let $f: \text{Space } d \to F$ be a function from a $d$-dimensional Euclidean space to a normed space $F$. If $f$ is distribution-bounded (satisfying the property `IsDistBounded f`), then for any scalar $c \in \mathbb{R}$, the distribution associated with the function $x \mapsto c \cdot f(x)$ is equal to $c$ times the distribution associated with $f$. That is: \[ \text{distOfFunction}(c \cdot f) = c \cdot \text{distOfFunction}(f) \] where the distribution $\text{distOfFunction}(f)$ is the continuous linear map from the Schwartz space $\mathcal{S}(\text{Space } d, \mathbb{R})$ to $F$ defined by the integral against $f$.

Let $d$ be a natural number and $F$ be a normed space. Suppose $f: \text{Space } d \to F$ is a distribution-bounded function (satisfying the property `IsDistBounded f`). For any real scalar $c \in \mathbb{R}$, the distribution associated with the function $x \mapsto c \cdot f(x)$ is equal to $c$ times the distribution associated with $f$. Mathematically, this is expressed as: \[ \text{distOfFunction}(c \cdot f) = c \cdot \text{distOfFunction}(f) \] where $\text{distOfFunction}(f)$ denotes the $F$-valued distribution on $\text{Space } d$ defined by the action $\eta \mapsto \int \eta(x) f(x) \, dx$ for test functions $\eta \in \mathcal{S}(\text{Space } d, \mathbb{R})$.

Let $f: \text{Space } d \to \mathbb{R}$ be a real-valued function on a $d$-dimensional Euclidean space. Suppose $f$ is distribution-bounded (satisfying the property `IsDistBounded f`). For any real scalar $c \in \mathbb{R}$, the distribution associated with the function $x \mapsto c \cdot f(x)$ is equal to the scalar $c$ times the distribution associated with $f$. Mathematically, this is expressed as: \[ \text{distOfFunction}(c \cdot f) = c \cdot \text{distOfFunction}(f) \] where $\text{distOfFunction}(f)$ denotes the distribution on $\text{Space } d$ defined by its action on a Schwartz test function $\eta \in \mathcal{S}(\text{Space } d, \mathbb{R})$ as the integral: \[ \eta \mapsto \int_{\text{Space } d} \eta(x) f(x) \, dx \]

Let $d$ be a natural number and $F$ be a normed space over $\mathbb{R}$. Suppose $f: \text{Space } d \to F$ is a function such that its pointwise negation $-f$ is distribution-bounded (satisfying the property `IsDistBounded (fun x => -f x)`). The distribution associated with the function $-f$ is equal to the negation of the distribution associated with $f$. Mathematically, this is expressed as: \[ \text{distOfFunction}(-f) = -\text{distOfFunction}(f) \] where $\text{distOfFunction}(f)$ denotes the $F$-valued distribution on $\text{Space } d$ defined by the action $\eta \mapsto \int \eta(x) f(x) \, dx$ for test functions $\eta \in \mathcal{S}(\text{Space } d, \mathbb{R})$.

Let $f: \text{Space } d \to \mathbb{R}^n$ be a distribution-bounded function (satisfying the property `IsDistBounded f`), where $\mathbb{R}^n$ is an $n$-dimensional Euclidean space. For any Schwartz test function $\eta \in \mathcal{S}(\text{Space } d, \mathbb{R})$ and any constant vector $y \in \mathbb{R}^n$, the inner product of the distribution value $T_f(\eta)$ with $y$ is given by the integral of the product of $\eta$ and the pointwise inner product of $f$ and $y$: \[ \langle T_f(\eta), y \rangle = \int_{\text{Space } d} \eta(x) \langle f(x), y \rangle \, dx \] where $T_f$ denotes the distribution associated with $f$ (`distOfFunction f hf`) and $\langle \cdot, \cdot \rangle$ denotes the standard Euclidean inner product.

Let $f: \text{Space } d \to \mathbb{R}^n$ be a distribution-bounded function (satisfying `IsDistBounded f`). For any Schwartz test function $\eta \in \mathcal{S}(\text{Space } d, \mathbb{R})$ and any index $i \in \{0, \dots, n-1\}$, the $i$-th component of the vector-valued distribution associated with $f$ evaluated at $\eta$ is equal to the evaluation at $\eta$ of the distribution associated with the $i$-th component function $x \mapsto f(x)_i$. That is, \[ (T_f(\eta))_i = T_{f_i}(\eta) \] where $T_f$ denotes the distribution `distOfFunction f hf` and $f_i$ is the $i$-th component of $f$.

Let $f: \text{Space } d \to \text{Vector}_n$ be a function from a $d$-dimensional Euclidean space to the space of $n$-dimensional Lorentz vectors that is distribution-bounded (satisfying the predicate `IsDistBounded f`). Let $\eta \in \mathcal{S}(\text{Space } d, \mathbb{R})$ be a Schwartz test function. For any index $i$ in the index set $\text{Fin } 1 \oplus \text{Fin } n$, the $i$-th component of the Lorentz vector resulting from the distribution $T_f$ associated with $f$ acting on $\eta$ is equal to the value of the distribution associated with the scalar-valued component function $f_i : x \mapsto f(x)_i$ acting on $\eta$. That is, $$(T_f \eta)_i = T_{f_i} \eta$$ where $T_f$ is the distribution defined by the integral $\eta \mapsto \int_{\text{Space } d} \eta(x) f(x) \, dx$.