QuantumInfo.Finite.Braket

The notation $\langle \psi \rvert$ represents a linear functional, referred to as a "bra" vector, which is the dual of a state vector $\psi$. In the context of finite-dimensional quantum mechanics, this operator maps elements of a Hilbert space to the complex numbers $\mathbb{C}$.

Let $d$ be a finite index set. For an element $\psi$ that can be interpreted as a vector in $\mathbb{C}^d$, the notation $|\psi\rangle$ denotes the corresponding quantum state (ket) in the space of pure states `Ket d`. This notation acts as a coercion or constructor that treats a vector-like object as a ket in the specified finite-dimensional Hilbert space.

Let $d$ be a finite index set. The type of kets `Ket d`, which represents pure quantum states as vectors in $\mathbb{C}^d$, is endowed with a `FunLike` instance. This allows a ket $|\psi\rangle$ to be treated as a function from the index set $d$ to the complex numbers $\mathbb{C}$, where the value at an index $i \in d$ is the $i$-th component of the underlying vector $\psi.\text{vec}$.

For any quantum state vector (ket) $|\psi\rangle$ in a finite-dimensional Hilbert space with basis $d$, the evaluation of $|\psi\rangle$ as a function from the basis $d$ to the complex numbers $\mathbb{C}$ is equivalent to its underlying vector representation $\psi.\text{vec}$.

Let $d$ be a finite index set. The type of bras `Bra d`, which represents the dual vectors (row vectors) in the finite-dimensional Hilbert space $\mathbb{C}^d$, is endowed with a `FunLike` instance. This allows a bra $\langle \phi |$ to be treated as a function mapping each index $i \in d$ to a complex number $\mathbb{C}$. Specifically, for any bra $\langle \phi |$, the value at index $i$ is defined by the $i$-th component of its underlying vector representation $\phi.\text{vec}$. The mapping is injective, meaning two bras are equal if and only if their vector components are identical.

For any quantum state covector (bra) $\langle \psi |$ in a finite-dimensional Hilbert space with basis $d$, the evaluation of $\langle \psi |$ as a function from the basis $d$ to the complex numbers $\mathbb{C}$ is equivalent to its underlying vector representation $\psi.\text{vec}$.

Given a finite index set $d$, a bra $\langle \xi | \in \text{Bra } d$ and a ket $|\psi\rangle \in \text{Ket } d$ are represented as vectors in $\mathbb{C}^d$. The dot product $\langle \xi | \psi \rangle$ is defined as the sum over the index set $d$ of the product of their components: $$\langle \xi | \psi \rangle = \sum_{x \in d} \xi(x) \psi(x)$$ where $\xi(x)$ and $\psi(x)$ denote the $x$-th components of the bra and ket respectively.

Given a bra vector $\xi \in \text{Bra}(d)$ and a ket vector $\psi \in \text{Ket}(d)$, the notation $\langle \xi \| \psi \rangle$ represents their inner product (or "bracket"), which is a complex number in $\mathbb{C}$. This is defined by applying the dot product function to the vectors $\xi$ and $\psi$.

Let $d$ be a finite index set. For a bra $\langle\psi| \in \text{Bra}(d)$ and a ket $|\varphi\rangle \in \text{Ket}(d)$, the bracket (inner product) $\langle\psi|\varphi\rangle$ is equal to the standard dot product of their underlying vectors, denoted as $\sum_{i \in d} \psi_i \varphi_i$.

Let $d$ be a finite index set and $|\psi\rangle$ be a ket in $\mathbb{C}^d$. For any index $i \in d$, the value of the ket when treated as a function at $i$, denoted $\psi(i)$, is equal to the $i$-th component of its underlying vector $\psi.\text{vec}$.

Let $d$ be a finite index set and $\psi$ be a dual vector in the bra representation (an element of $\text{Bra}(d)$). For any index $i \in d$, the value of the function $\psi$ applied to $i$ is equal to the component of its underlying vector $\psi.\text{vec}$ at index $i$. In other words, $\psi(i) = (\psi.\text{vec})_i$.

Let $\xi$ and $\psi$ be quantum states in the ket representation (elements of type `Ket d`). If for every index $x \in d$, the components of the states are equal, i.e., $\xi(x) = \psi(x)$, then the states themselves are equal, $\xi = \psi$.

Let $d$ be a finite index set representing the dimension of the Hilbert space. For any dual vectors (bras) $\xi, \psi \in \text{Bra}(d)$, if for all basis indices $x \in d$, the components are equal (i.e., $\xi(x) = \psi(x)$), then the dual vectors themselves are equal ($\xi = \psi$).

For any quantum state represented as a ket $|\psi\rangle$ in a finite-dimensional space indexed by $d$, the sum of the squared norms of its components over all indices $x \in d$ is equal to $1$, i.e., $\sum_{x \in d} |\psi(x)|^2 = 1$.

Let $d$ be a finite index set representing the dimensions of a Hilbert space, and let $\psi \in \text{Bra}(d)$ be a dual vector (bra). The sum over all basis indices $x \in d$ of the squared norm of the components $|\psi(x)|^2$ is equal to 1.

Given a finite index set $d$, any ket $|\psi\rangle \in \text{Ket } d$ (represented as a vector in $\mathbb{C}^d$) can be mapped to its corresponding bra $\langle\psi| \in \text{Bra } d$. This transformation is defined by taking the complex conjugate of each element of the vector: $(\text{to\_bra } \psi)_i = \overline{\psi_i}$ for all $i \in d$.

Given a bra vector $\langle \psi |$ in a $d$-dimensional Hilbert space (represented as a function $\psi: d \to \mathbb{C}$ satisfying a normalization condition), the function `Bra.to_ket` maps it to its corresponding ket vector $| \psi \rangle$ by taking the complex conjugate of each component, such that $| \psi \rangle_x = \overline{\psi_x}$.

An instance of the coercion operator from the space of ket vectors $\text{Ket}(d)$ (represented as column vectors) to the space of bra vectors $\text{Bra}(d)$ (represented as row vectors/linear functionals). This coercion is defined by the mapping `Ket.to_bra`, which corresponds to the conjugate transpose operation $| \psi \rangle \mapsto \langle \psi |$.

An instance of the coercion operator from the space of bra vectors $\text{Bra}(d)$ to the space of ket vectors $\text{Ket}(d)$, defined by the correspondence between a linear functional and its dual vector (specifically using the `Bra.to_ket` map).

Let $|\psi\rangle$ be a ket vector in a finite-dimensional Hilbert space indexed by $d$. For any index $i \in d$, the evaluation of the corresponding bra vector $\langle\psi|$ at $i$ is equal to the complex conjugate of the $i$-th component of the ket's underlying vector, denoted as $\langle\psi|i = \overline{\psi_i}$.

For any normalized ket $|\psi\rangle$ in a finite-dimensional Hilbert space (represented as a vector in $\mathbb{C}^d$ where $d$ is a finite index set), there exists at least one index $x \in d$ such that the component $\psi(x)$ is non-zero.

Let $\langle \psi |$ be a normalized bra vector in a finite-dimensional Hilbert space (represented as a function from a finite index set $d$ to the complex numbers $\mathbb{C}$). There exists at least one index $x \in d$ such that the component $\langle \psi | x$ is non-zero.

Given a finite set $d$, a vector $v: d \to \mathbb{C}$, and a proof $h$ that $v$ is not the zero vector (i.e., there exists some $x \in d$ such that $v(x) \neq 0$), this function constructs a normalized ket $|\psi\rangle$. The components of the resulting vector are defined as: $$|\psi\rangle_x = \frac{v_x}{\sqrt{\sum_{i \in d} |v_i|^2}}$$ where the denominator is the $L^2$-norm $\|v\|$. The definition ensures the resulting vector has unit norm, $\sum_x ||\psi\rangle_x|^2 = 1$.

Let $|\psi\rangle$ be a ket (a normalized vector in $\mathbb{C}^d$). If we take the underlying vector $\psi.\text{vec}$ and apply the normalization function `Ket.normalize` (using the fact that $|\psi\rangle$ is non-zero), the resulting ket is equal to the original $|\psi\rangle$. Specifically, for any $|\psi\rangle \in \text{Ket } d$, $\text{Ket.normalize}(\psi.\text{vec}, h) = |\psi\rangle$, where $h$ is the proof that $|\psi\rangle$ has at least one non-zero component.

Given a finite indexing set $d$ and a vector $v \in \mathbb{C}^d$ such that $v$ has at least one non-zero component ($v \neq 0$), the normalization function produces a bra (row vector) $\langle \psi |$ by scaling $v$ by the reciprocal of its $L^2$-norm. Specifically, the resulting vector $\text{vec} \in \mathbb{C}^d$ is defined by $$\text{vec}(x) = \frac{v(x)}{\sqrt{\sum_{i \in d} \|v(i)\|^2}}$$ for each $x \in d$. This construction ensures that the resulting bra satisfies the normalization condition $\sum_{x \in d} \|\text{vec}(x)\|^2 = 1$.

For any normalized row vector (bra) $\psi$ in a $d$-dimensional Hilbert space, normalizing its underlying vector $\psi.\text{vec}$ results in the original bra $\psi$ itself. Here, $\psi.\text{vec}$ is the raw vector representation of the bra, and the normalization process involves dividing the vector by its $L^2$-norm.

Given a finite indexing set $d$ that is non-empty, the uniform superposition state $|+\rangle$ is defined as the normalization of a vector where every component is $1$. Specifically, it is the Ket $|\psi\rangle$ defined by the components: $$|+\rangle_x = \frac{1}{\sqrt{|d|}}$$ for all $x \in d$, where $|d|$ denotes the cardinality of the set $d$. This state represents a coherent superposition of all basis elements with equal probability amplitudes.

For any non-empty finite index set $d$, there exists a default instance of a "Ket" vector $| \psi \rangle$ in the Hilbert space. This default ket is defined as the uniform superposition state: $$| \psi \rangle = \frac{1}{\sqrt{|d|}} \sum_{i \in d} | i \rangle$$ where $|d|$ is the cardinality of the set $d$ and $|i\rangle$ are the computational basis vectors.

Given a finite type $d$, the function constructs a "Ket" vector $|i\rangle$ in the Hilbert space corresponding to a basis element $i \in d$. Representing the state as a function $d \to \mathbb{C}$, it is defined as the Kronecker delta $\delta_{ij}$, which takes the value $1$ when $j = i$ and $0$ otherwise.

Given a finite index set $d$, for any element $i \in d$, the function constructs the corresponding basis "Bra" vector $\langle i |$. It is defined as a linear functional on the space of "Kets" (represented as functions $d \to \mathbb{C}$), such that when applied to a basis element $j \in d$, it yields $1$ if $i = j$ and $0$ otherwise.

For a finite index set $d$, any Bra vector $\xi$ in the dual space can be treated as a function mapping a Ket vector $\psi$ to a complex number $\mathbb{C}$. This mapping is defined by the inner product (or braket) $\langle \xi | \psi \rangle$. The implementation ensures that a Bra is uniquely determined by its action on all Ket vectors.

Let $d$ be a finite index set and $|\psi\rangle$ be a ket in $\mathbb{C}^d$ representing a normalized quantum pure state. The inner product of the state with itself, denoted by $\langle\psi|\psi\rangle$, is equal to $1$.

Given two kets $|\psi_1\rangle \in \text{Ket } d_1$ and $|\psi_2\rangle \in \text{Ket } d_2$ representing pure quantum states in finite-dimensional Hilbert spaces indexed by $d_1$ and $d_2$ respectively, their product $|\psi_1\rangle \otimes |\psi_2\rangle$ is a ket in the tensor product space indexed by $d_1 \times d_2$. The components of the resulting vector are defined by the product of the individual components, i.e., $(|\psi_1\rangle \otimes |\psi_2\rangle)_{(i,j)} = \psi_1(i)\psi_2(j)$ for all $i \in d_1, j \in d_2$. This construction creates an unentangled (separable) state.

This is a notation definition for the tensor product of two quantum ket states. For two kets $|\psi_1\rangle$ of dimension $d_1$ and $|\psi_2\rangle$ of dimension $d_2$, the notation $|\psi_1\rangle \otimes^\phi |\psi_2\rangle$ represents the combined state in the tensor product Hilbert space of dimension $d_1 \times d_2$, computed via the `Ket.prod` function.

A quantum state (ket) $|\psi\rangle$ in the composite Hilbert space $\mathbb{C}^{d_1 \times d_2}$ (representing the tensor product $\mathbb{C}^{d_1} \otimes \mathbb{C}^{d_2}$) is a product state if there exist states $|\xi\rangle \in \mathbb{C}^{d_1}$ and $|\phi\rangle \in \mathbb{C}^{d_2}$ such that $|\psi\rangle = |\xi\rangle \otimes |\phi\rangle$.

A state vector (ket) $|\psi\rangle$ in the tensor product space $\mathbb{C}^{d_1} \otimes \mathbb{C}^{d_2}$ is said to be entangled if it cannot be expressed as a product state (i.e., it is not a decomposable tensor $|\psi_1\rangle \otimes |\psi_2\rangle$ for some $|\psi_1\rangle \in \mathbb{C}^{d_1}$ and $|\psi_2\rangle \in \mathbb{C}^{d_2}$).

Let $\psi_1 \in \mathcal{H}_{d_1}$ and $\psi_2 \in \mathcal{H}_{d_2}$ be two quantum states (kets) in Hilbert spaces of dimensions $d_1$ and $d_2$, respectively. Then their tensor product $\psi_1 \otimes \psi_2$ (denoted `ψ₁.prod ψ₂`) is a product state.

For any two quantum states $|\psi_1\rangle$ in a Hilbert space of dimension $d_1$ and $|\psi_{2}\rangle$ in a Hilbert space of dimension $d_2$, their tensor product state $|\psi_1\rangle \otimes |\psi_2\rangle$ is not an entangled state.

Let $d_1$ and $d_2$ be finite index sets, and let $|\psi\rangle$ be a ket in the tensor product space $\mathbb{C}^{d_1 \times d_2}$. Then $|\psi\rangle$ is a product state if and only if for all indices $i_1, i_2 \in d_1$ and $j_1, j_2 \in d_2$, the components of the ket satisfy the cross-multiplicativity condition: $$\psi(i_1, j_1) \cdot \psi(i_2, j_2) = \psi(i_1, j_2) \cdot \psi(i_2, j_1)$$

Let $d$ be a finite non-empty type. The maximally entangled state (MES) on the system $d \times d$ is a state vector (ket) $|\Psi\rangle \in \mathbb{C}^{d \times d}$ whose components are given by: $$|\Psi\rangle_{i,j} = \begin{cases} \frac{1}{\sqrt{|d|}} & \text{if } i = j \\ 0 & \text{if } i \neq j \end{cases}$$ where $|d|$ denotes the cardinality of $d$. This state corresponds to a normalized superposition of basis states $|i, i\rangle$ with all-positive phases. In the specific case where $d$ has size 2, this definition yields the standard Bell state $|\Phi^+\rangle = \frac{1}{\sqrt{2}}(|00\rangle + |11\rangle)$.

Let $d$ be a type representing a finite-dimensional Hilbert space basis. If $d$ is nontrivial (meaning the dimension of the space is at least $2$), then the maximally entangled state `MES` in the tensor product space $d \times d$ is entangled.

Let $d$ be a finite non-empty type representing the basis of a Hilbert space. For any matrix $M \in \text{Mat}_{d \times d}(\mathbb{C})$, the following identity holds when acting on the vector representation of the maximally entangled state $|\Psi\rangle \in \mathbb{C}^d \otimes \mathbb{C}^d$: $$(M \otimes I) |\Psi\rangle = (I \otimes M^T) |\Psi\rangle$$ where $I$ is the identity matrix, $\otimes$ denotes the Kronecker product (${\otimes_k}$), $M^T$ denotes the transpose of $M$, and $|\Psi\rangle$ is the maximally entangled state `Ket.MES d`.

Let `Ket d` be the type of quantum state vectors (kets) in a system with basis $d$. The relation `Ket.PhaseEquiv` is defined as a setoid (equivalence relation) on `Ket d`, where two kets $a$ and $b$ are equivalent if there exists a complex number $z \in \mathbb{C}$ such that $\|z\| = 1$ and the state vectors satisfy $a.\text{vec} = z \cdot b.\text{vec}$. Mathematically, this captures the notion that two quantum states are equivalent if they differ only by a global phase.

Let $d$ be a type representing the dimensions of a finite-dimensional Hilbert space. The type $\text{KetUpToPhase } d$ is defined as the quotient of the space of kets $\text{Ket } d$ by the equivalence relation $\text{Ket.PhaseEquiv}$. This relation identifies two kets if they differ only by a global phase factor $e^{i\theta}$. This represents the space of pure quantum states, where physical observables are invariant under such phase transformations.

Let $|\psi\rangle$ be a ket in the space $\text{Ket } d$. The function maps the ket $|\psi\rangle$ to its corresponding equivalence class $[|\psi\rangle]$ in the quotient space $\text{KetUpToPhase } d$. This quotient space represents pure quantum states where kets are identified if they differ only by a global phase factor $e^{i\theta}$.

Let $\text{Ket } d$ be the type of quantum state vectors (kets) and $\text{KetUpToPhase } d$ be the quotient space defined by the phase equivalence relation $\sim$, where $|\psi\rangle \sim |\phi\rangle$ if there exists $z \in \mathbb{C}$ with $\|z\|=1$ such that $|\psi\rangle = z|\phi\rangle$. Given a function $f: \text{Ket } d \to \alpha$ and a proof $hf$ that $f$ is phase-invariant (i.e., $\forall |\psi\rangle, |\phi\rangle, |\psi\rangle \sim |\phi\rangle \implies f(|\psi\rangle) = f(|\phi\rangle)$), the function `KetUpToPhase.lift` returns the induced function $\tilde{f}: \text{KetUpToPhase } d \to \alpha$.

Let $Ket(d)$ be the set of finite-dimensional quantum state vectors (kets). Let $KetUpToPhase(d)$ be the quotient of $Ket(d)$ by the phase equivalence relation $\sim$ (where $\psi \sim \varphi$ if they differ only by a complex phase). For any function $f: Ket(d) \to \alpha$ that is invariant under phase changes (i.e., $f(\psi) = f(\varphi)$ whenever $\psi \sim \varphi$), let $\tilde{f}: KetUpToPhase(d) \to \alpha$ be the function induced by $f$ on the quotient space. Then for any ket $|\psi\rangle \in Ket(d)$, the value of $\tilde{f}$ applied to the equivalence class $[|\psi\rangle]$ is equal to $f(|\psi\rangle)$.

Let $\text{KetUpToPhase } d$ be the space of quantum pure states, defined as the quotient of kets $\text{Ket } d$ by the global phase equivalence relation. Let $P$ be a property (predicate) defined on $\text{KetUpToPhase } d$. If $P([|\psi\rangle])$ holds for every ket $|\psi\rangle \in \text{Ket } d$ (where $[|\psi\rangle]$ denotes the equivalence class of $|\psi\rangle$), then $P(q)$ holds for every state $q \in \text{KetUpToPhase } d$.

The quotient map $\text{mk}: \text{Ket } d \to \text{KetUpToPhase } d$, which maps a quantum state vector $|\psi\rangle$ to its equivalence class under global phase, is a surjective function. That is, every pure quantum state in $\text{KetUpToPhase } d$ can be represented by at least one ket $|\psi\rangle \in \text{Ket } d$.