Physlib.QuantumMechanics.DDimensions.SpaceDHilbertSpace.PolyBddSchwartzSubmodule

For a given dimension $d$ and an extended natural number $a \in \mathbb{N} \cup \{\infty\}$, the space of polynomially bounded Schwartz maps is defined as the $\mathbb{C}$-submodule of the Schwartz space $\mathcal{S}(\mathbb{R}^d, \mathbb{C})$ (denoted in Lean as `𝓢(Space d, ℂ)`) consisting of functions $f$ that satisfy specific growth conditions. A Schwartz function $f$ belongs to this submodule if for every natural number $k$ such that $k \le a$, there exists a constant $C > 0$ such that for all $x \in \mathbb{R}^d$: $$\|x\|^{-k} \|f(x)\| \le C,$$ where $\| \cdot \|$ denotes the Euclidean norm on $\mathbb{R}^d$. This condition ensures that the function $f$ grows no faster than $\|x\|^k$ for all $k \le a$.

For a dimension $d \in \mathbb{N}$ and an extended natural number $a \in \mathbb{N} \cup \{\infty\}$, the map $\iota: \text{PolyBddSchwartzMap}(d, a) \to L^2(\mathbb{R}^d, \mathbb{C})$ is the continuous linear inclusion of the submodule of polynomially bounded Schwartz maps into the Hilbert space of square-integrable functions. This map is obtained by restricting the domain of the canonical inclusion from the Schwartz space $\mathcal{S}(\mathbb{R}^d, \mathbb{C})$ to $L^2(\mathbb{R}^d, \mathbb{C})$ to the submodule defined by the growth condition $\|x\|^{-k} \|f(x)\| \le C_k$ for all $k \le a$.

For a given dimension $d \in \mathbb{N}$ and an extended natural number $a \in \mathbb{N} \cup \{\infty\}$, the polynomially-bounded Schwartz submodule is the $\mathbb{C}$-submodule of the Hilbert space $L^2(\text{Space } d, \mathbb{C})$ defined as the image (range) of the space of polynomially bounded Schwartz maps $\text{PolyBddSchwartzMap}(d, a)$ under the canonical inclusion into $L^2$. This submodule consists of Schwartz functions $f \in \mathcal{S}(\text{Space } d, \mathbb{C})$ such that for every natural number $k \le a$, there exists a constant $C_k > 0$ satisfying $\|x\|^{-k} \|f(x)\| \le C_k$ for all $x \in \text{Space } d$.

For any dimension $d \in \mathbb{N}$ and any extended natural number $a \in \mathbb{N} \cup \{\infty\}$, the continuous linear inclusion map $\iota: \text{PolyBddSchwartzMap}(d, a) \to L^2(\text{Space } d, \mathbb{C})$ is injective.

For a dimension $d \in \mathbb{N}$ and an extended natural number $a \in \mathbb{N} \cup \{\infty\}$, there is a linear equivalence over $\mathbb{C}$ between the space of polynomially bounded Schwartz maps $\text{PolyBddSchwartzMap}(d, a)$ and the corresponding submodule $\text{PolyBddSchwartzSubmodule}(d, a)$ of the Hilbert space $L^2(\text{Space } d, \mathbb{C})$. This equivalence is established by restricting the codomain of the injective linear inclusion $\iota: \text{PolyBddSchwartzMap}(d, a) \to L^2(\text{Space } d, \mathbb{C})$ to its range.

For any dimension $d \in \mathbb{N}$ and any extended natural number $a \in \mathbb{N} \cup \{\infty\}$, there is a natural inclusion mapping each polynomially bounded Schwartz function $f \in \text{PolyBddSchwartzMap}(d, a)$ to its corresponding element in the full Schwartz space $\mathcal{S}(\mathbb{R}^d, \mathbb{C})$.

For a dimension $d \in \mathbb{N}$ and an extended natural number $a \in \mathbb{N} \cup \{\infty\}$, an element $f$ in the $\mathbb{C}$-submodule of polynomially bounded Schwartz maps, $\text{PolyBddSchwartzMap}(d, a)$, can be treated as a function from $\mathbb{R}^d$ to $\mathbb{C}$. This coercion maps the element $f$ to its underlying function $x \mapsto f(x)$, allowing it to be evaluated at any point $x \in \mathbb{R}^d$.

For any dimension $d \in \mathbb{N}$ and any extended natural number $a \in \mathbb{N} \cup \{\infty\}$, let $f$ be a polynomially bounded Schwartz map in the submodule $\text{PolyBddSchwartzMap}(d, a)$. For any point $x \in \mathbb{R}^d$, the value of the underlying function of $f$ evaluated at $x$ is equal to the value of the Schwartz map $f$ evaluated at $x$.

For a dimension $d \in \mathbb{N}$ and an extended natural number $a \in \mathbb{N} \cup \{\infty\}$, let $\psi$ be an element of the Schwartz submodule $\text{SchwartzSubmodule}(d)$ of the Hilbert space $L^2(\text{Space } d, \mathbb{C})$. If $\psi$ is contained in the polynomially-bounded Schwartz submodule $\text{PolyBddSchwartzSubmodule}(d, a)$, then the Schwartz function $f \in \mathcal{S}(\text{Space } d, \mathbb{C})$ obtained by applying the inverse of the linear equivalence $\text{polyBddSchwartzEquiv}$ to $\psi$ is equal to the Schwartz function obtained by applying the inverse of the general linear equivalence $\text{schwartzEquiv}$ to $\psi$.

For any dimension $d \in \mathbb{N}$ and extended natural number $a \in \mathbb{N} \cup \{\infty\}$, let $f$ be a polynomially bounded Schwartz map in $\text{PolyBddSchwartzMap}(d, a)$. The image of $f$ under the linear equivalence $\text{polyBddSchwartzEquiv}$ is equal to the underlying function $f$ almost everywhere with respect to the Lebesgue volume measure.

For any dimension $d \in \mathbb{N}$, the space of polynomially bounded Schwartz maps with growth parameter $a = 0$, denoted as $\text{PolyBddSchwartzMap}(d, 0)$, is equal to the entire space of Schwartz functions $\mathcal{S}(\mathbb{R}^d, \mathbb{C})$.

Let $d$ be a natural number and let $a, b \in \mathbb{N} \cup \{\infty\}$ be extended natural numbers. If $a \le b$, then the $\mathbb{C}$-submodule of Schwartz maps $\text{PolyBddSchwartzMap}(d, b)$ is contained within the submodule $\text{PolyBddSchwartzMap}(d, a)$. Here, $\text{PolyBddSchwartzMap}(d, a)$ is defined as the set of Schwartz functions $f \in \mathcal{S}(\mathbb{R}^d, \mathbb{C})$ such that for every natural number $k \le a$, there exists a constant $C > 0$ such that $\|x\|^{-k} \|f(x)\| \le C$ for all $x \in \mathbb{R}^d$.

For any dimension $d \in \mathbb{N}$, the polynomially-bounded Schwartz submodule with growth parameter $a = 0$, denoted as $\text{PolyBddSchwartzSubmodule}(d, 0)$, is equal to the submodule of all Schwartz functions $\text{SchwartzSubmodule}(d)$ within the Hilbert space $L^2(\text{Space } d, \mathbb{C})$.

For any dimension $d \in \mathbb{N}$ and any extended natural number $a \in \mathbb{N} \cup \{\infty\}$, the polynomially-bounded Schwartz submodule $\text{PolyBddSchwartzSubmodule}(d, a)$ of the Hilbert space $L^2(\text{Space } d, \mathbb{C})$ is a submodule of (and thus contained within) the Schwartz submodule $\text{SchwartzSubmodule}(d)$.

For any dimension $d \in \mathbb{N}$ and extended natural numbers $a, b \in \mathbb{N} \cup \{\infty\}$, if $a \le b$, then the polynomially-bounded Schwartz submodule of the Hilbert space $L^2(\text{Space } d, \mathbb{C})$ associated with $b$ is contained within the submodule associated with $a$, i.e., $\text{PolyBddSchwartzSubmodule}(d, b) \subseteq \text{PolyBddSchwartzSubmodule}(d, a)$.

For any dimension $d \in \mathbb{N}$, the polynomially-bounded Schwartz submodule $\text{PolyBddSchwartzSubmodule}(d, \infty)$ is dense in the Hilbert space $L^2(\text{Space } d, \mathbb{C})$. This submodule consists of the Schwartz functions $f \in \mathcal{S}(\text{Space } d, \mathbb{C})$ such that for every natural number $k$, there exists a constant $C_k > 0$ satisfying $\|x\|^{-k} \|f(x)\| \le C_k$ for all $x \in \text{Space } d$.

For any dimension $d \in \mathbb{N}$ and any extended natural number $a \in \mathbb{N} \cup \{\infty\}$, the polynomially-bounded Schwartz submodule is dense in the Hilbert space $L^2(\text{Space } d, \mathbb{C})$. This submodule consists of all Schwartz functions $f: \text{Space } d \to \mathbb{C}$ such that for every natural number $k \le a$, there exists a constant $C_k > 0$ satisfying $\|x\|^{-k} \|f(x)\| \le C_k$ for all $x \in \text{Space } d$, where $\text{Space } d$ is a $d$-dimensional real inner product space.