Physlib.QuantumMechanics.FiniteTarget.HilbertSpace

For a given natural number $n$, the definition `FiniteHilbertSpace n` represents the $n$-dimensional complex Hilbert space, mathematically equivalent to $\mathbb{C}^n$, constructed as the Euclidean space over the complex numbers $\mathbb{C}$ with coordinates indexed by the finite set $\{0, 1, \dots, n-1\}$.

For any natural number $n$, the $n$-dimensional complex Hilbert space $\mathbb{C}^n$ (represented by `FiniteHilbertSpace n`) is equipped with the structure of an additive commutative group.

For any natural number $n$, the $n$-dimensional complex Hilbert space $\mathbb{C}^n$ (represented by `FiniteHilbertSpace n`) is equipped with the structure of a vector space over the field of complex numbers $\mathbb{C}$.

For any natural number $n$, the $n$-dimensional complex Hilbert space $\mathbb{C}^n$ (represented by `FiniteHilbertSpace n`) is equipped with the structure of a normed additive commutative group.

For any natural number $n$, the $n$-dimensional complex Hilbert space $\mathbb{C}^n$ (represented by `FiniteHilbertSpace n`) is equipped with the structure of an inner product space over the field of complex numbers $\mathbb{C}$.

For any natural number $n$, the $n$-dimensional complex Hilbert space $\mathbb{C}^n$ is a complete space.

In the $d$-dimensional complex Hilbert space $\mathbb{C}^d$ (modeled by `FiniteHilbertSpace d`), for any two vectors $\psi$ and $\phi$, the underlying coordinate representation of their sum $\psi + \phi$ is equal to the sum of their individual coordinate representations: $(\psi + \phi).val = \psi.val + \phi.val$.

In the $d$-dimensional complex Hilbert space $\mathbb{C}^d$ (modeled by `FiniteHilbertSpace d`), for any complex number $c$ and any vector $\psi$, the underlying coordinate representation of the scalar multiplication $c \cdot \psi$ is equal to the scalar multiplication of $c$ and the coordinate representation of $\psi$: $(c \cdot \psi).val = c \cdot \psi.val$.

In the $d$-dimensional complex Hilbert space $\mathbb{C}^d$, the value (coordinate representation) of the zero vector is equal to the zero vector $0$.

For a natural number $d$, this definition provides the $\mathbb{C}$-linear equivalence (isomorphism of complex vector spaces) between the finite-dimensional Hilbert space `FiniteHilbertSpace d` and the standard complex Euclidean space $\mathbb{C}^d$.

For a natural number $d$, the $d$-dimensional complex Hilbert space $\mathbb{C}^d$ (represented by `FiniteHilbertSpace d`) is equipped with the structure of a normed additive commutative group. This means it possesses a commutative addition, a zero vector, additive inverses, and a norm $\|\cdot\|$ that satisfies the triangle inequality.

For any vector $\psi$ in the $d$-dimensional complex Hilbert space $\mathbb{C}^d$ (represented by `FiniteHilbertSpace d`), the norm of $\psi$, denoted as $\|\psi\|$, is equal to the norm of its underlying value $\psi.\text{val}$.

For a natural number $d$, the $d$-dimensional complex Hilbert space (represented by `FiniteHilbertSpace d`, which is equivalent to $\mathbb{C}^d$) is equipped with the structure of an inner product space over the complex numbers $\mathbb{C}$. This defines a complex-valued inner product $\langle \cdot, \cdot \rangle$ that is conjugate-linear in the first argument, linear in the second argument, and positive definite.

In the $d$-dimensional complex Hilbert space $\mathbb{C}^d$ (represented by `FiniteHilbertSpace d`), the inner product $\langle \psi, \varphi \rangle$ of two vectors $\psi$ and $\varphi$ is equal to the inner product of their underlying values $\psi.\text{val}$ and $\varphi.\text{val}$.

For any natural number $d$, the $d$-dimensional complex Hilbert space (represented as `FiniteHilbertSpace d`, which is equivalent to $\mathbb{C}^d$) is a finite-dimensional vector space over the complex numbers $\mathbb{C}$.

For any natural number $d$, the $d$-dimensional complex Hilbert space $\mathbb{C}^d$ is a complete space, meaning that every Cauchy sequence in the space converges to an element within it.

For a natural number $d$, the $d$-dimensional complex Hilbert space (represented by `FiniteHilbertSpace d`) is linearly isometrically equivalent to the standard complex Euclidean space $\mathbb{C}^d$. This equivalence is a bijective $\mathbb{C}$-linear map that preserves the inner product and the norm.

For a finite index set $d$, `basisFun` defines the standard orthonormal basis $\{e_i\}_{i \in d}$ for the $d$-dimensional complex Hilbert space $\mathbb{C}^d$ (represented by `FiniteHilbertSpace d`). This basis is indexed by the elements of $d$, where each basis vector $e_i$ corresponds to the unit vector in the $i$-th coordinate, satisfying the orthonormality condition $\langle e_i, e_j \rangle = \delta_{ij}$.

Let $d$ be a finite index set. For any element $i \in d$, the $i$-th basis vector of the standard orthonormal basis for the $d$-dimensional complex Hilbert space $\mathbb{C}^d$ is equal to the vector with $1$ at index $i$ and $0$ elsewhere (the standard unit vector).