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.

For any elements $\psi$ and $\phi$ in the Hilbert space $L^2(\text{Space } d, \mathbb{C})$, the representative function of their sum $\psi + \phi$ is equal to the pointwise sum of the representative functions of $\psi$ and $\phi$ almost everywhere with respect to the volume measure.

For any elements $\psi$ and $\phi$ in the Hilbert space $L^2(\text{Space } d, \mathbb{C})$, the function representing their difference $\psi - \phi$ is equal to the pointwise difference of the functions representing $\psi$ and $\phi$ almost everywhere with respect to the volume measure.

For a natural number $d$, let $L^2(\text{Space } d, \mathbb{C})$ be the Hilbert space of square-integrable functions from $\text{Space } d$ to the complex numbers $\mathbb{C}$. For any scalar $c$ and any element $\psi \in L^2(\text{Space } d, \mathbb{C})$, the representative function of the scalar multiplication $c \cdot \psi$ is equal to the pointwise product of $c$ and the representative function of $\psi$ almost everywhere with respect to the volume measure. That is, $(c \cdot \psi)(x) = c \cdot \psi(x)$ for almost all $x \in \text{Space } d$.

In the Hilbert space $L^2(\text{Space } d, \mathbb{C})$ of square-integrable functions, a family of functions $\psi_a$ indexed by elements of a type $\alpha$ converges to zero along a filter $l$ if and only if the integral of their squared norms converges to zero. That is, $$\lim_{a \to l} \psi_a = 0 \iff \lim_{a \to l} \int_{\text{Space } d} \|\psi_a(x)\|^2 \, dx = 0$$ where the limit on the left is taken in the $L^2$ norm topology and the integral is the standard Lebesgue integral over the volume of $\text{Space } d$.

For a subset $\Omega \subseteq \text{Space } d$ and a measure $\mu$, this definition provides a $\mathbb{C}$-linear map from the Hilbert space $L^2(\text{Space } d, \mathbb{C}, \mu)$ to the Hilbert space $L^2(\text{Space } d, \mathbb{C}, \mu|_\Omega)$, where $\mu|_\Omega$ denotes the restriction of the measure $\mu$ to the set $\Omega$.

For any subset $\Omega \subseteq \text{Space } d$ and any wavefunction $\psi \in L^2(\text{Space } d, \mathbb{C}, \mu)$, the projection of $\psi$ onto the restricted Hilbert space $L^2(\text{Space } d, \mathbb{C}, \mu|_\Omega)$ is equal to $\psi$ almost everywhere with respect to the restricted measure $\mu|_\Omega$.

Let $L^2(\text{Space } d, \mathbb{C}, \mu)$ be the Hilbert space of square-integrable functions on $\text{Space } d$ with respect to a measure $\mu$. For any subset $\Omega \subseteq \text{Space } d$, let $P_\Omega$ denote the linear projection map from $L^2(\text{Space } d, \mathbb{C}, \mu)$ to $L^2(\text{Space } d, \mathbb{C}, \mu|_\Omega)$ (where $\mu|_\Omega$ is the restriction of $\mu$ to $\Omega$). For any wavefunction $\psi \in L^2(\text{Space } d, \mathbb{C}, \mu)$, the $L^2$-norm of the projected wavefunction is less than or equal to the $L^2$-norm of the original wavefunction: $$\|P_\Omega \psi\| \leq \|\psi\|$$

For a measurable set $\Omega \subseteq \text{Space } d$ and a measure $\mu$, this definition is the $\mathbb{C}$-linear isometry from the Hilbert space $L^2(\text{Space } d, \mu|_\Omega, \mathbb{C})$ to $L^2(\text{Space } d, \mu, \mathbb{C})$. It maps a wavefunction $\psi$ to its extension by zero outside of $\Omega$, represented by the indicator function $\mathbb{1}_\Omega \psi$.

Let $d$ be a natural number and $\mu$ be a measure on $\text{Space } d$. For any measurable set $\Omega \subseteq \text{Space } d$ and any wave function $\psi$ in the Hilbert space $L^2(\text{Space } d, \mu|_\Omega, \mathbb{C})$, the inclusion of $\psi$ into the global Hilbert space $L^2(\text{Space } d, \mu, \mathbb{C})$ is equal to the indicator function $\mathbb{1}_\Omega \psi$ almost everywhere with respect to $\mu$.

For a measurable set $\Omega \subseteq \text{Space } d$ and a measure $\mu$ on $\text{Space } d$, let $L^2(\text{Space } d, \mu, \mathbb{C})$ denote the Hilbert space of square-integrable functions. Let $I_\Omega : L^2(\text{Space } d, \mu|_\Omega) \hookrightarrow L^2(\text{Space } d, \mu)$ be the linear isometry inclusion that extends a wavefunction by zero outside of $\Omega$, and let $P_\Omega : L^2(\text{Space } d, \mu) \to L^2(\text{Space } d, \mu|_\Omega)$ be the linear projection map that restricts a wavefunction to $\Omega$. Then $P_\Omega$ is a left inverse of $I_\Omega$, which means that for any $\psi \in L^2(\text{Space } d, \mu|_\Omega)$, we have $P_\Omega(I_\Omega(\psi)) = \psi$.

Let $\Omega \subseteq \text{Space } d$ be a measurable set and $\mu$ be a measure on $\text{Space } d$. Let $L^2(\text{Space } d, \mu, \mathbb{C})$ be the Hilbert space of square-integrable functions, and let $L^2(\text{Space } d, \mu|_\Omega, \mathbb{C})$ be the Hilbert space with respect to the measure $\mu$ restricted to $\Omega$. If $i : L^2(\mu|_\Omega) \hookrightarrow L^2(\mu)$ is the linear isometry that includes a wavefunction $\psi$ into the larger space (by extending it by zero outside $\Omega$) and $p : L^2(\mu) \to L^2(\mu|_\Omega)$ is the linear projection map, then for any $\psi \in L^2(\mu|_\Omega)$, it holds that $p(i(\psi)) = \psi$.

Let $d$ be a natural number and let $\mu$ be a measure on $\text{Space } d$. For any measurable subset $\Omega \subseteq \text{Space } d$, the linear projection map from the Hilbert space $L^2(\text{Space } d, \mathbb{C}, \mu)$ to the Hilbert space $L^2(\text{Space } d, \mathbb{C}, \mu|_\Omega)$ is surjective, where $\mu|_\Omega$ denotes the restriction of the measure $\mu$ to the set $\Omega$.