Physlib.QuantumMechanics.DDimensions.SpaceDHilbertSpace.Basic

For a natural number $d$, the Hilbert space for single-particle quantum mechanics on $\text{Space } d$ is defined as the space $L^2(\text{Space } d, \mathbb{C})$ of square-integrable functions from $\text{Space } d$ to the complex numbers $\mathbb{C}$, where functions that are equal almost everywhere are identified as equivalence classes.

For a natural number $d$, let $\mathcal{H}_d = L^2(\text{Space } d, \mathbb{C})$ be the Hilbert space of square-integrable functions. The function `toBra` is the antilinear map from $\mathcal{H}_d$ to its strong dual space $\mathcal{H}_d^*$. For any $f \in \mathcal{H}_d$, the resulting linear functional $\text{toBra}(f)$ acts on an element $g \in \mathcal{H}_d$ by the inner product $\langle f, g \rangle$. In the context of quantum mechanics, this represents the mapping of a state vector (a "ket") to its corresponding dual vector (a "bra").

Let $d$ be a natural number and $\mathcal{H}_d = L^2(\text{Space } d, \mathbb{C})$ be the Hilbert space of square-integrable functions. For any two elements $f, g \in \mathcal{H}_d$, the evaluation of the linear functional $\text{toBra}(f)$ at the element $g$ is equal to the complex inner product $\langle f, g \rangle_{\mathbb{C}}$.

Let $d$ be a natural number and $\mathcal{H}_d = L^2(\text{Space } d, \mathbb{C})$ be the Hilbert space of square-integrable functions. The antilinear map $\text{toBra} : \mathcal{H}_d \to \mathcal{H}_d^*$, which maps a state vector $f \in \mathcal{H}_d$ (a "ket") to its corresponding dual vector (a "bra") defined by the inner product $\langle f, \cdot \rangle$, is surjective.

For a natural number $d$, let $\mathcal{H}_d = L^2(\text{Space } d, \mathbb{C})$ be the Hilbert space of square-integrable functions. The antilinear map $\text{toBra}: \mathcal{H}_d \to \mathcal{H}_d^*$, which maps a state vector $f \in \mathcal{H}_d$ (a "ket") to its corresponding dual vector (a "bra") defined by the inner product $\langle f, \cdot \rangle$, is injective.

The proposition $\text{MemHS}(f)$ asserts that a complex-valued function $f: \text{Space } d \to \mathbb{C}$ is a member of the $L^2$ space. This means that $f$ is almost everywhere strongly measurable and square-integrable, satisfying $\int \|f(x)\|^2 \, dx < \infty$. This condition allows the function to be lifted to the Hilbert space associated with the physical system.

Let $f: \text{Space } d \to \mathbb{C}$ be a complex-valued function. If $f \in L^2(\text{Space } d)$ (i.e., $f$ is a member of the Hilbert space associated with the system), then $f$ is almost everywhere strongly measurable.

A complex-valued function $f: \text{Space } d \to \mathbb{C}$ satisfies the property $\text{MemHS}(f)$ if and only if it is almost everywhere strongly measurable and square-integrable, meaning that the integral of its squared norm $\int \|f(x)\|^2 \, dx$ is finite.

The zero function $f(x) = 0$ on $\text{Space } d$ is a member of the Hilbert space $L^2(\text{Space } d)$, satisfying the property $\text{MemHS}(f)$. This means that the zero function is almost everywhere strongly measurable and square-integrable, such that $\int \|f(x)\|^2 \, dx < \infty$.

The constant zero function $f: \text{Space } d \to \mathbb{C}$, defined by $f(x) = 0$ for all $x \in \text{Space } d$, is a member of the Hilbert space $L^2(\text{Space } d)$ (i.e., it satisfies the $\text{MemHS}$ property).

For any complex-valued functions $f, g: \text{Space } d \to \mathbb{C}$, if both $f$ and $g$ are members of the $L^2$ space (meaning they are square-integrable such that $\int \|f(x)\|^2 \, dx < \infty$), then their sum $f + g$ is also a member of the $L^2$ space.

Let $f: \text{Space } d \to \mathbb{C}$ be a complex-valued function and $c \in \mathbb{C}$ be a complex scalar. If $f$ is a member of the Hilbert space $L^2(\text{Space } d)$ (meaning $f$ is square-integrable), then the scalar product $c \cdot f$ is also a member of $L^2(\text{Space } d)$.

Let $f, g: \text{Space } d \to \mathbb{C}$ be complex-valued functions. If $f$ is square-integrable (satisfying the property $\text{MemHS}(f)$) and $f$ is equal to $g$ almost everywhere with respect to the volume measure ($f =ᵐ[\text{volume}] g$), then $g$ is also square-integrable (satisfying $\text{MemHS}(g)$).

For a natural number $d$ and an almost everywhere strongly measurable function $f: \text{Space } d \to \mathbb{C}$, the equivalence class of functions equal to $f$ almost everywhere is an element of the Hilbert space $L^2(\text{Space } d, \mathbb{C})$ if and only if $f$ satisfies the square-integrability property $\text{MemHS}(f)$.

Given a complex-valued function $f: \text{Space } d \to \mathbb{C}$ and a proof $h_f$ that $f$ is square-integrable (i.e., $\text{MemHS}(f)$ holds), this definition constructs the corresponding element in the Hilbert space $L^2(\text{Space } d, \mathbb{C})$. The resulting element is the equivalence class of functions that are equal to $f$ almost everywhere.

For any element $f$ in the Hilbert space $L^2(\text{Space } d, \mathbb{C})$, the coerced function $f: \text{Space } d \to \mathbb{C}$ satisfies the property $\text{MemHS}(f)$, meaning it is almost everywhere strongly measurable and square-integrable.

For every element $f$ in the Hilbert space $L^2(\text{Space } d, \mathbb{C})$, there exists a complex-valued function $g: \text{Space } d \to \mathbb{C}$ and a proof $h_g$ that $g$ is square-integrable (i.e., $\text{MemHS}(g)$ holds), such that the element in the Hilbert space constructed from $g$, denoted $\text{mk}(h_g)$, is equal to $f$. In other words, every element of the Hilbert space is represented by at least one square-integrable function.

For any square-integrable function $f : \text{Space } d \to \mathbb{C}$ (i.e., such that $\text{MemHS}(f)$ holds), the element $\text{mk}(f)$ in the Hilbert space $L^2(\text{Space } d)$ constructed from $f$ is equal to $f$ almost everywhere with respect to the volume measure.

For any two complex-valued functions $f, g: \text{Space } d \to \mathbb{C}$ that are square-integrable (i.e., $\text{MemHS}(f)$ and $\text{MemHS}(g)$ hold), the inner product of their corresponding elements $\text{mk}(f)$ and $\text{mk}(g)$ in the Hilbert space $L^2(\text{Space } d, \mathbb{C})$ is equal to the integral of the product of the complex conjugate of $f$ and the function $g$: $$\langle \text{mk}(f), \text{mk}(g) \rangle_{\mathbb{C}} = \int_{\text{Space } d} \overline{f(x)} g(x) \, dx$$ where $\overline{f(x)}$ denotes the complex conjugate of $f(x)$.

For any complex-valued function $f: \text{Space } d \to \mathbb{C}$ that is square-integrable (i.e., $\text{MemHS}(f)$ holds), the $L^2$ norm of the element $[f]$ in the Hilbert space $L^2(\text{Space } d, \mathbb{C})$ constructed from $f$ is equal to the $L^2$ norm of the function $f$ itself: $$\| [f] \|_{L^2} = \| f \|_{L^2}$$ where $[f]$ (denoted in the formal statement as `mk hf`) represents the equivalence class of functions equal to $f$ almost everywhere.

Let $f: \text{Space } d \to \mathbb{C}$ be an almost everywhere strongly measurable function. The equivalence class of $f$ (functions equal almost everywhere) belongs to the Hilbert space $L^2(\text{Space } d, \mathbb{C})$ if and only if the function $x \mapsto \|f(x)\|^2$ is integrable over $\text{Space } d$.

Let $f, g: \text{Space } d \to \mathbb{C}$ be two square-integrable functions (satisfying $\text{MemHS}(f)$ and $\text{MemHS}(g)$). Let $[f]$ and $[g]$ denote the elements (equivalence classes) in the Hilbert space $L^2(\text{Space } d, \mathbb{C})$ constructed from these functions. Then the Hilbert space element corresponding to the sum of the functions $f + g$ is equal to the sum of the individual Hilbert space elements, that is, $[f + g] = [f] + [g]$.

Let $f: \text{Space } d \to \mathbb{C}$ be a square-integrable function and $c \in \mathbb{C}$ be a complex scalar. Let $[f]$ denote the element in the Hilbert space $L^2(\text{Space } d, \mathbb{C})$ constructed from $f$. Then the Hilbert space element corresponding to the scaled function $c \cdot f$ is equal to the scalar $c$ multiplied by the element $[f]$, that is, $[c \cdot f] = c \cdot [f]$.

Let $f, g: \text{Space } d \to \mathbb{C}$ be two square-integrable functions (satisfying the property $\text{MemHS}$). Let $[f]$ and $[g]$ denote the corresponding elements (equivalence classes) in the Hilbert space $L^2(\text{Space } d, \mathbb{C})$ constructed via the `mk` operation. Then $[f] = [g]$ in the Hilbert space if and only if $f$ and $g$ are equal almost everywhere with respect to the volume measure ($f =^{a.e.} g$).

For any two elements $f$ and $g$ in the Hilbert space $L^2(\text{Space } d, \mathbb{C})$, $f = g$ if and only if their representative functions from $\text{Space } d$ to $\mathbb{C}$ are equal almost everywhere with respect to the volume measure.