Physlib.QuantumMechanics.HilbertSpaces.FiniteTarget.Basic

The Hilbert space of a finite target quantum mechanical system

A finite target quantum mechanical system is one whose states live in a finite dimensional Hilbert space, with the basis states labelled by a finite type `d` (for example the sites of a finite lattice, or the levels of a qudit).

This file contains - the definition of `FiniteHilbertSpace d`, the Hilbert space of such a system, as a structure wrapping `EuclideanSpace ℂ d`, together with the notation `𝓗[d]`; - its vector space structure (`AddCommGroup` and `Module ℂ`), transferred from `EuclideanSpace ℂ d` along the equivalence `equivEuclidean`; - its Hilbert space structure (`NormedAddCommGroup`, `InnerProductSpace ℂ`, `FiniteDimensional ℂ` and `CompleteSpace`), induced along `linearEquivEuclidean`; - the standard orthonormal basis `basisFun`, whose elements are the states localized at the points of `d`.

The vector space structure on `FiniteHilbertSpace d`

The vector space structure is transferred from `EuclideanSpace ℂ d` along the equivalence `equivEuclidean`.

The Hilbert space structure on `FiniteHilbertSpace d`

The norm and inner product are induced from `EuclideanSpace ℂ d` along `linearEquivEuclidean`, making `FiniteHilbertSpace d` a finite dimensional (and hence complete) inner product space, that is, a Hilbert space.

The standard orthonormal basis of `FiniteHilbertSpace d`

4 declarations

definition

Notation for the Hilbert space $\mathcal{H}[S]$

#term𝓗[_]

The notation $\mathcal{H}[S]$ represents the Hilbert space associated with a quantum mechanical system defined over a finite target space $S$ .

definition

Equivalence $\text{FiniteHilbertSpace } d \simeq \text{EuclideanSpace } \mathbb{C} \text{ } d$

#equivEuclidean

For a finite type $d$ with decidable equality, this is the equivalence (isomorphism) between the finite-dimensional Hilbert space `FiniteHilbertSpace d` and the standard complex Euclidean space $\mathbb{C}^d$ (represented as `EuclideanSpace ℂ d`).

instance

$\text{FiniteHilbertSpace}(d)$ is an additive commutative group

#instAddCommGroup

For a finite set $d$ with decidable equality, the finite-dimensional complex Hilbert space $\text{FiniteHilbertSpace}(d)$ is equipped with the structure of an additive commutative group. This means that elements of the Hilbert space (vectors) can be added together, addition is commutative and associative, there exists a zero vector, and every vector has an additive inverse.

instance

Complex module structure on `FiniteHilbertSpace d`

#instModuleComplex

For a finite set $d$ with decidable equality, the finite-dimensional Hilbert space $\mathcal{H}_d$ (represented by `QuantumMechanics.FiniteHilbertSpace d`) is equipped with the structure of a module over the complex numbers $\mathbb{C}$ .