Physlib.Mathematics.InnerProductSpace.Gaussian

Gaussians in inner product spaces

i. Overview

In this module we define Gaussians as Schwartz maps in general inner product spaces.

The most general Gaussian constructed is `exp (-2⁻¹ * ‖B⁻¹ (x - x₀)‖ ^ 2)` (mean `x₀` and covariance `BᵀB`) as a Schwartz map `𝓢(E, 𝕜)`, where `B : D ≃L[ℝ] E` is a linear equivalence of inner product spaces. This is accomplished by first constructing the Gaussian `exp (-2⁻¹ * ‖x‖ ^ 2)` as a Schwartz map `𝓢(E, ℝ)` using explicit bounds on the derivatives of `‖x‖ ^ 2 = innerSL ℝ x x` and limiting properties of the real exponential, then composing with an invertible affine transformation.

The Gaussians are left unnormalized since the appropriate condition will depend on context and whether `E` is finite- or infinite-dimensional. For example, the normalization conditions when interpreted as a probability density function vs. as a quantum state require different pre-factors.

For some relevant Gaussian integrals see `Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform`.

ii. Key results

- `gaussian 𝕜 B x₀` : Given a linear equivalence `B : D ≃L[ℝ] E` and mean `x₀ : E`, the Gaussian `exp (-2⁻¹ * ‖B⁻¹ (x - x₀)‖ ^ 2)` centered on `x₀` as a Schwartz map `𝓢(E, 𝕜)`. - `gaussian₀ 𝕜 B` : Given a linear equivalence `B : D ≃L[ℝ] E` of inner product spaces, the Gaussian `exp (-2⁻¹ * ‖B⁻¹ x‖ ^ 2)` centered on the origin as a Schwartz map `𝓢(E, 𝕜)`. - `stdGaussian E 𝕜` : The standard Gaussian `exp (-2⁻¹ * ‖x‖ ^ 2)` as a Schwartz map `𝓢(E, 𝕜)`.

iii. Table of contents

A. Standard, real-valued
B. General, RCLike-valued

iv. References

A. Standard, real-valued

B. General, RCLike-valued

5 declarations

definition

Standard real Gaussian $\exp\left(-\frac{1}{2} \|x\|^2\right)$

#realStdGaussian

Let $E$ be a real inner product space. The standard real-valued Gaussian is the Schwartz map $f \in \mathcal{S}(E, \mathbb{R})$ defined by $f(x) = \exp\left(-\frac{1}{2} \|x\|^2\right)$ for any $x \in E$ , where $\|x\|$ denotes the norm induced by the inner product on $E$ .

definition

$\mathbb{k}$ -valued Gaussian $\exp\left(-\frac{1}{2} \|B^{-1}(x - x_0)\|^2\right)$ as a Schwartz map

#gaussian

Let $E$ and $D$ be real inner product spaces, and let $\mathbb{k}$ be a field (typically $\mathbb{R}$ or $\mathbb{C}$ ). Given a continuous linear equivalence $B : D \cong E$ and a vector $x_0 \in E$ (representing the mean), the Gaussian is the (unnormalized) Schwartz map $g \in \mathcal{S}(E, \mathbb{k})$ defined by $g(x) = \exp\left(-\frac{1}{2} \|B^{-1}(x - x_0)\|^2\right)$ for all $x \in E$ , where the norm $\|\cdot\|$ is the norm on $D$ induced by its inner product.

theorem

Evaluation of the Gaussian $\exp\left(-\frac{1}{2} \|B^{-1}(x - x_0)\|^2\right)$ at $x$

#gaussian_apply

Let $E$ and $D$ be real inner product spaces, and let $\mathbb{k}$ be an $\text{RCLike}$ field (such as $\mathbb{R}$ or $\mathbb{C}$ ). For a continuous linear equivalence $B : D \cong E$ , a vector $x_0 \in E$ representing the mean, and any point $x \in E$ , the value of the Gaussian Schwartz map $g = \text{gaussian}(\mathbb{k}, B, x_0)$ at $x$ is given by $g(x) = \exp\left(-\frac{1}{2} \|B^{-1}(x - x_0)\|^2\right),$ where the norm $\|\cdot\|$ is the norm on $D$ induced by its inner product, $\exp$ is the real exponential function, and the result is implicitly cast from $\mathbb{R}$ to $\mathbb{k}$ .

abbrev

$\mathbb{k}$ -valued Gaussian $\exp\left(-\frac{1}{2} \|B^{-1}x\|^2\right)$ as a Schwartz map

#gaussian₀

Let $E$ and $D$ be real inner product spaces and $\mathbb{k}$ be a field (typically $\mathbb{R}$ or $\mathbb{C}$ ). Given a continuous linear equivalence $B : D \cong E$ , the Gaussian centered at the origin is the unnormalized Schwartz map $g \in \mathcal{S}(E, \mathbb{k})$ defined by $g(x) = \exp\left(-\frac{1}{2} \|B^{-1}x\|^2\right)$ for all $x \in E$ , where $\| \cdot \|$ is the norm on $D$ induced by its inner product.

abbrev

Standard Gaussian $\exp\left(-\frac{1}{2} \|x\|^2\right)$ as a Schwartz map

#stdGaussian

Let $E$ be a real inner product space and $\mathbb{k}$ be an $\text{RCLike}$ field (typically $\mathbb{R}$ or $\mathbb{C}$ ). The standard Gaussian is the unnormalized Schwartz map $g \in \mathcal{S}(E, \mathbb{k})$ defined by $g(x) = \exp\left(-\frac{1}{2} \|x\|^2\right)$ for all $x \in E$ , where $\| \cdot \|$ is the norm on $E$ induced by its inner product. This corresponds to the case where the covariance transformation is the identity map.