QuantumInfo.Finite.MState

For a finite index set $d$, there exists a coercion that maps a quantum mixed state $\rho$ of type `MState d` to its underlying representation as a complex Hermitian matrix $M \in \mathcal{H}_d(\mathbb{C})$. This allows a mixed state to be treated as a Hermitian matrix in mathematical contexts.

For a quantum mixed state $\rho$ of finite dimension $d$, the function $m(\rho)$ returns the underlying $d \times d$ complex matrix representation of the state. It is defined as the matrix component of the Hermitian operator $M$ associated with $\rho$.

For a quantum mixed state $\rho$ of dimension $d$, the underlying matrix of the Hermitian operator $M$ associated with $\rho$ is equal to the matrix representation $m$ of the state $\rho$. Specifically, let $\rho \in \text{MState } d$; then the identity $\rho.M.\text{mat} = \rho.m$ holds.

Let $\rho$ be a quantum mixed state of finite dimension $d$. Let $M$ be the Hermitian operator associated with $\rho$. Then $M$ is strictly positive-definite, denoted by $0 < M$.

The definition provides a tactic extension for the `positivity` framework to automatically prove that the Hermitian operator $M$ associated with a finite-dimensional quantum mixed state $\rho$ is strictly positive-definite ($0 < \rho.M$). By analyzing the expression $e$ representing the operator projection $\rho.M$, the tactic extracts the state $\rho$ and constructs a proof of its positivity using the lemma `MState.pos`.

For a finite-dimensional quantum mixed state $\rho$, its associated matrix implementation $\rho.m$ is positive semidefinite.

Let $\rho$ be a finite-dimensional quantum mixed state of dimension $d$. Let $\rho.m$ denote the density matrix in $\text{Matrix}(d, d, \mathbb{C})$ associated with the state. The matrix $\rho.m$ is Hermitian, meaning it is equal to its own conjugate transpose, $\rho.m = (\rho.m)^\dagger$.

Let $\rho$ be a finite-dimensional quantum mixed state of dimension $d$. Let $\rho.m$ denote the density matrix in $\text{Matrix}(d, d, \mathbb{C})$ associated with the state. The trace of the density matrix is equal to 1, i.e., $\text{Tr}(\rho.m) = 1$.

Let $\rho_1$ and $\rho_2$ be finite-dimensional quantum mixed states of dimension $d$. If the density matrices associated with these states are equal, i.e., $\rho_1.m = \rho_2.m$, then the mixed states themselves are equal, $\rho_1 = \rho_2$.

Let $d$ be a finite dimension associated with a quantum system. Let $\rho_1, \rho_2$ be quantum mixed states in $MState(d)$, and let $m(\rho)$ denote the density matrix in $Matrix(d, d, \mathbb{C})$ associated with a mixed state $\rho$. The mapping $m: MState(d) \to Matrix(d, d, \mathbb{C})$ is injective; that is, if $m(\rho_1) = m(\rho_2)$, then $\rho_1 = \rho_2$.

For a finite-dimensional quantum system of dimension $d$, the map $M$ that assigns a density matrix to each mixed state $\rho \in \text{MState}(d)$ is injective. That is, for any two mixed states $\rho_1$ and $\rho_2$, if $M(\rho_1) = M(\rho_2)$, then $\rho_1 = \rho_2$.

The set of all matrices corresponding to finite-dimensional mixed states $\rho$ of dimension $d$ (the range of the map `MState.M`) is a convex set over the real numbers $\mathbb{R}$.

The type `MState d`, representing mixed states of a $d$-dimensional quantum system, is an instance of a `Mixable` structure over the space of Hermitian matrices $\text{Herm}_d(\mathbb{C})$. This means that `MState d` is equipped with a convex structure induced by its embedding into the vector space of Hermitian matrices, allowing for the formation of convex combinations (mixtures) of quantum states. Specifically, this instance utilizes the mapping from mixed states to their matrix representations, ensures the mapping is injective, and verifies that the set of mixed states (positive semi-definite matrices with unit trace) is a convex subset of $\text{Herm}_d(\mathbb{C})$.

For a finite-dimensional quantum mixed state of dimension $d$ to exist, the underlying index type $d$ must be non-empty (i.e., $d$ must have at least one element).

For any finite dimensional quantum mixed state $\rho$ and any index $i$ of its basis, the $i$-th eigenvalue of the Hermitian matrix associated with $\rho$ is non-negative, i.e., $0 \le \lambda_i(\rho)$.

For any finite-dimensional quantum mixed state $\rho$ and any index $i$, the $i$-th eigenvalue of the Hermitian matrix associated with $\rho$ is less than or equal to 1, i.e., $\lambda_i(\rho) \le 1$.

For any finite dimensional quantum mixed state $\rho$ with associated density matrix $M_\rho$, the matrix $M_\rho$ is less than or equal to the identity matrix in the Loewner order, denoted as $M_\rho \le I$. This means that $I - M_\rho$ is a positive semi-definite matrix, or equivalently, all eigenvalues $\lambda_i$ of $M_\rho$ satisfy $\lambda_i \le 1$.

For any two quantum mixed states $\rho$ and $\sigma$ in a Hilbert space of dimension $d$, their inner product $\langle \rho, \sigma \rangle_{\text{Prob}}$ is defined as the Hilbert-Schmidt inner product of their corresponding density matrices $M_\rho$ and $M_\sigma$, given by $\text{Tr}(M_\rho^\dagger M_\sigma)$. This value is a real number in the interval $[0, 1]$, where the non-negativity $\langle \rho, \sigma \rangle \ge 0$ follows from the positive semi-definiteness of the states, and the upper bound follows from the fact that for mixed states, $\text{Tr}(M_\rho M_\sigma) \le \text{Tr}(M_\rho)\text{Tr}(M_\sigma) = 1 \cdot 1 = 1$.

The inner product between two mixed states $\rho$ and $\sigma$ in the probability sense, denoted $\langle \rho, \sigma \rangle_{Prob}$, is defined as the inner product of their underlying matrices $\langle \rho.M, \sigma.M \rangle$. This value is guaranteed to be non-negative because the state matrices are positive semi-definite ($\rho.nonneg$ and $\sigma.nonneg$), and it is bounded above by $1$, as shown by the transition from the inequality $\langle \rho.M, \sigma.M \rangle \leq \text{Tr}(\rho.M)\text{Tr}(\sigma.M)$ to $1 \times 1$ since mixed states have unit trace.

Let $\rho$ and $\sigma$ be mixed states of dimension $d$. Let $\mathbf{M}_\rho$ and $\mathbf{M}_\sigma$ denote their corresponding density matrices in $\text{Mat}_{d \times d}(\mathbb{C})$. The real-valued inner product of the states $\rho$ and $\sigma$ in the probability inner product space, denoted by $\langle \rho, \sigma \rangle_{\text{Prob}}$, is equal to the Frobenius inner product of their underlying matrices, $\langle \mathbf{M}_\rho, \mathbf{M}_\sigma \rangle = \text{Tr}(\mathbf{M}_\rho^\dagger \mathbf{M}_\sigma)$.

Given a mixed state $\rho$ with an underlying density matrix $M_\rho \in \text{Mat}_{d \times d}(\mathbb{C})$ and a complex matrix $T \in \text{Mat}_{d \times d}(\mathbb{C})$, the complex-valued expectation value of $T$ with respect to $\rho$ is defined as the trace of the product of $T$ and $M_\rho$: \[ \text{Tr}(T M_\rho) \]

For a quantum mixed state $\rho$ with density matrix $M_\rho \in \text{Mat}_{d \times d}(\mathbb{C})$ and a Hermitian operator $T$ (represented by a Hermitian matrix in $\text{Mat}_{d \times d}(\mathbb{C})$), the expectation value of $T$ in state $\rho$ is the real number defined by the Frobenius inner product of $M_\rho$ and $T$: \[ \langle M_\rho, T \rangle_F = \text{Tr}(M_\rho^\dagger T) \] Since $M_\rho$ and $T$ are Hermitian, this is equivalent to $\text{Tr}(M_\rho T)$.

Let $\rho$ be a finite-dimensional quantum mixed state and let $T \in \text{Mat}_{d \times d}(\mathbb{C})$ be a Hermitian matrix. If $T$ is positive semi-definite (i.e., $T \geq 0$), then the expectation value of $T$ with respect to $\rho$, denoted by $\text{Tr}(T M_\rho)$, is a non-negative real number ($\geq 0$).

For a quantum mixed state $\rho$, the expectation value of the zero operator is $0$. That is, $\rho.\text{exp\_val}(0) = 0$.

Let $\rho$ be a finite-dimensional quantum mixed state. The expectation value of the identity matrix $I$ with respect to $\rho$, denoted as $\text{Tr}(\rho I)$, is equal to $1$.

Let $\rho$ be a finite-dimensional quantum mixed state and let $T$ be a Hermitian matrix of dimension $d$ over $\mathbb{C}$. If $T$ satisfies the operator inequality $T \le I$, where $I$ is the identity matrix, then the expectation value of $T$ with respect to $\rho$ is less than or equal to 1, i.e., $\text{Tr}(\rho T) \le 1$.

Let $\rho$ be a finite-dimensional quantum mixed state and let $T$ be a Hermitian matrix of dimension $d$ over $\mathbb{C}$. If $T$ satisfies the operator inequality $0 \le T \le I$ (meaning $T$ is a positive semidefinite operator bounded above by the identity matrix), then the expectation value of $T$ with respect to $\rho$, denoted $\text{Tr}(\rho T)$, lies in the unit interval $[0, 1]$, i.e., $0 \le \rho.\text{exp\_val } T \le 1$.

Let $\rho$ be a finite-dimensional quantum mixed state and let $A$ and $B$ be Hermitian matrices of dimension $d$ over $\mathbb{C}$. The expectation value of the difference $A - B$ with respect to the state $\rho$ is equal to the difference of their individual expectation values: \[ \text{Tr}(\rho(A - B)) = \text{Tr}(\rho A) - \text{Tr}(\rho B) \] where $\text{Tr}(\rho M)$ denotes the expectation value of an operator $M$ in state $\rho$.

Let $\rho$ be a quantum mixed state with density matrix $M_\rho$, and let $A$ be a positive semidefinite (PSD) Hermitian matrix of dimension $d$ over $\mathbb{C}$ (i.e., $A \ge 0$). The expectation value of $A$ in the state $\rho$, defined as $\langle A \rangle_\rho = \text{Tr}(M_\rho A)$, is equal to $0$ if and only if the support of the density matrix $M_\rho$ is a subspace of the kernel of $A$, denoted $\text{supp}(M_\rho) \subseteq \ker(A)$.

Let $\rho$ be a quantum mixed state and $A$ be a Hermitian matrix acting on a $d$-dimensional complex Hilbert space such that $A \le I$, where $I$ denotes the identity matrix. The expectation value of $A$ on the state $\rho$, denoted by $\langle A \rangle_\rho$, is equal to $1$ if and only if the support of the density matrix $\rho$ is contained within the kernel of $I - A$. In other words, $\rho$ must be entirely supported on the $1$-eigenspace of $A$.

Let $\rho$ be a mixed state of a finite-dimensional quantum system and let $A$ and $B$ be Hermitian matrices. The expectation value of the sum of the matrices is equal to the sum of their individual expectation values, such that $\langle A + B \rangle_\rho = \langle A \rangle_\rho + \langle B \rangle_\rho$.

Let $\rho$ be a quantum mixed state of dimension $d$. For any real number $r \in \mathbb{R}$ and any Hermitian matrix $A \in \mathbb{C}^{d \times d}$, the expectation value of the scalar multiple of the matrix $r A$ is given by $r$ times the expectation value of $A$. That is, $\langle r A \rangle_\rho = r \langle A \rangle_\rho$.

Let $\rho$ be a quantum mixed state of dimension $d$. For any two Hermitian matrices $A, B \in \mathbb{C}^{d \times d}$, if $A \le B$ (meaning $B - A$ is a positive semi-definite matrix), then the expectation value of $A$ with respect to $\rho$ is less than or equal to the expectation value of $B$ with respect to $\rho$, denoted as $\langle A \rangle_\rho \le \langle B \rangle_\rho$.

Let $d$ be a finite index set and $|\psi\rangle$ be a ket in the $d$-dimensional Hilbert space (represented as `Ket d`). A pure mixed state $\rho$ can be constructed from $|\psi\rangle$ as the density matrix defined by the outer product $|\psi\rangle \langle\psi|$. Formally, its matrix elements are given by $\rho_{ij} = \psi_i \overline{\psi_j}$. This state is positive semi-definite and has a trace of 1, provided that $|\psi\rangle$ is normalized.

Let $d$ be a finite index set and $\psi \in \text{Ket } d$ be a quantum state vector (represented as a function from $d$ to $\mathbb{C}$). The density matrix $M$ corresponding to the pure state $|\psi\rangle$, denoted by $\text{pure}(\psi)$, has elements defined for any indices $i, j \in d$ as $$(M)_{ij} = \psi(i) \cdot \overline{\psi(j)}$$ where $\overline{\psi(j)}$ denotes the complex conjugate of the component $\psi(j)$. This corresponds to the standard definition of the pure state density matrix $\rho = |\psi\rangle\langle\psi|$.

Let $d$ be a finite index set and $|\psi\rangle$ be a quantum state vector in $\text{Ket } d$. Let $\rho = |\psi\rangle\langle\psi|$ be the density matrix corresponding to the pure state of $|\psi \rangle$, denoted formally as `(pure ψ).m`. Then the square of this density matrix is equal to itself: $$\rho^2 = \rho$$ In other words, the density matrix of any pure state is idempotent.

The purity of a finite-dimensional quantum mixed state $\rho$, represented as a matrix in $\text{MState}_d$, is defined as the trace of the square of the density matrix, $\text{Tr}(\rho^2)$. This value is returned as a probability $\text{Prob}$, reflecting that $0 \leq \text{Tr}(\rho^2) \leq 1$. In the formal implementation, this is calculated via the inner product $\langle \rho, \rho \rangle_{\text{Prob}}$ defined on the space of mixed states.

Given a mixed quantum state $\rho$, represented as a density matrix in $\mathbb{C}^{d \times d}$, its spectrum is defined as the probability distribution on the set of indices $\{1, \dots, d\}$ formed by the eigenvalues of the underlying Hermitian matrix. Specifically, for a state $\rho$, the spectrum is the distribution whose mass at each point corresponds to an eigenvalue $\lambda_i$ of the matrix $\rho$, where the non-negativity of the probabilities is guaranteed by the positive semi-definiteness of $\rho$, and the normalization to unity is guaranteed by the property $\text{Tr}(\rho) = 1$.

For any normalized quantum state vector $|\psi\rangle$ (represented as a `Ket d`), the eigenvalue spectrum of the corresponding pure mixed state $\rho = |\psi\rangle\langle\psi|$ is a constant probability distribution. That is, there exists an index $i$ such that the spectrum of $\text{pure } \psi$ is equal to the distribution $\delta_i$, where all probability mass is concentrated at a single outcome.

Let $\rho$ be a quantum mixed state of dimension $d$. If the eigenvalue spectrum of $\rho$ is a constant distribution (meaning there exists an index $i$ such that the spectrum assigns probability 1 to $i$ and 0 to all other indices), then $\rho$ is a pure state, i.e., there exists a state vector $|\psi\rangle$ such that $\rho = |\psi\rangle\langle\psi|$.

Let $\rho$ be a mixed quantum state in a $d$-dimensional Hilbert space. The state $\rho$ is a pure state (i.e., there exists a unit vector $|\psi\rangle$ such that $\rho = |\psi\rangle\langle\psi|$) if and only if its eigenvalue spectrum is a constant distribution, meaning there exists an index $i$ such that the spectrum of $\rho$ is equal to the distribution $\delta_i$ which assigns probability 1 to $i$ and 0 elsewhere.

Let $\rho$ be a finite-dimensional quantum mixed state of dimension $d$. Then $\rho$ is a pure state (i.e., there exists a ket vector $|\psi\rangle$ such that $\rho = |\psi\rangle\langle\psi|$) if and only if its purity, defined as $\text{Tr}(\rho^2)$, is equal to $1$.

For any finite-dimensional quantum mixed state $\rho$ of dimension $d$, there exists an orthonormal basis of ket vectors $\{|\psi_i\rangle\}_{i \in d}$ such that the Hermitian operator $M$ associated with $\rho$ can be written as the weighted sum of pure state operators: $$\rho.M = \sum_{i \in d} \lambda_i (|\psi_i\rangle\langle\psi_i|).M$$ where $\lambda_i$ are the probabilities given by the spectrum of the state (i.e., $\lambda_i = \rho.\text{spectrum } i$).

Given two quantum mixed states $\rho_1$ and $\rho_2$ acting on Hilbert spaces of dimensions $d_1$ and $d_2$ respectively, their product state $\rho_1 \otimes \rho_2$ is a mixed state acting on the tensor product space of dimension $d_1 \times d_2$. The density matrix of the product state is defined by the Kronecker product of the individual density matrices, $M = \rho_1.M \otimes \rho_2.M$, which is shown to be positive semi-definite and have unit trace.

An infix notation $\otimes^M$ used to represent the tensor product of two quantum mixed states, corresponding to the operation `MState.prod`. Given two mixed states $\rho_1$ and $\rho_2$, the expression $\rho_1 \otimes^M \rho_2$ denotes the resulting mixed state on the product space, where the underlying density matrix is the Kronecker product of the individual density matrices.

For any quantum mixed states $\xi_1$ and $\psi_1$ in a Hilbert space of dimension $d_1$, and mixed states $\xi_2$ and $\psi_2$ in a Hilbert space of dimension $d_2$, the inner product of their tensor products is the product of their individual inner products: $$\langle \xi_1 \otimes \xi_2, \psi_1 \otimes \psi_2 \rangle_{\text{Prob}} = \langle \xi_1, \psi_1 \rangle_{\text{Prob}} \cdot \langle \xi_2, \psi_2 \rangle_{\text{Prob}}$$ where $\otimes$ denotes the tensor product of mixed states and $\langle \cdot, \cdot \rangle_{\text{Prob}}$ denotes the Hilbert-Schmidt inner product $\text{Tr}(A^\dagger B)$ scaled to the interval $[0, 1]$.

Let $|\psi_1\rangle$ and $|\psi_2\rangle$ be quantum state vectors (kets) in Hilbert spaces of dimensions $d_1$ and $d_2$ respectively. The pure mixed state formed from their tensor product $|\psi_1 \otimes \psi_2\rangle$, denoted as $\text{pure}(\psi_1 \otimes \psi_2)$, is equal to the tensor product of the individual pure mixed states $\text{pure}(\psi_1) \otimes \text{pure}(\psi_2)$. In terms of density matrices, this expresses that $|\psi_1 \otimes \psi_2\rangle\langle\psi_1 \otimes \psi_2| = (|\psi_1\rangle\langle\psi_1|) \otimes (|\psi_2\rangle\langle\psi_2|)$.

Given a finite set of outcomes $d$ and a probability distribution $dist$ over $d$, the function `ofClassical` constructs a quantum mixed state (density matrix) $\rho \in \text{MState } d$. The resulting density matrix $\rho$ is a diagonal matrix in the computational basis, where each diagonal entry $\rho_{ii}$ is equal to the probability $dist(i)$ of the corresponding classical outcome $i$, and all off-diagonal entries $\rho_{ij}$ are zero for $i \neq j$.

Let $d$ be a finite set of states and $\text{dist}$ be a probability distribution over $d$, where $\text{dist}(i)$ denotes the probability of outcome $i$. The density matrix $M$ associated with the classical mixed state $W = \text{ofClassical}(\text{dist})$ is equal to the diagonal matrix over the complex numbers $\mathbb{C}$ whose diagonal entries are given by the probabilities $\text{dist}(i)$. That is, $M_{ii} = \text{dist}(i)$ and $M_{ij} = 0$ for $i \neq j$.

Let $d$ be a finite set of states and $\text{dist}$ be a probability distribution over $d$, where $\text{dist}(i)$ denotes the probability of outcome $i$. For the density matrix $M$ associated with the classical mixed state $W = \text{ofClassical}(\text{dist})$ and any real power $p \in \mathbb{R}$, the matrix power $M^p$ is equal to the diagonal matrix over the complex numbers $\mathbb{C}$ whose diagonal entries are the probabilities raised to the power $p$. That is, $(M^p)_{ii} = (\text{dist}(i))^p$ and $(M^p)_{ij} = 0$ for $i \neq j$.

For a finite-dimensional quantum system with basis index set $d$, where $d$ is non-empty, the maximally mixed state $\rho_{\text{unif}}$ is defined as the mixed state corresponding to the uniform classical probability distribution over $d$. In this state, the density matrix $M$ is given by $M = \frac{1}{|d|} I$, where $I$ is the identity matrix and $|d|$ is the cardinality of the set $d$.

For a quantum system whose underlying basis type $d$ has exactly one element (representing a 1-dimensional Hilbert space), there exists exactly one mixed state $\rho \in \text{MState } d$. In this case, the unique state is the maximally mixed (uniform) state.

For a finite-dimensional Hilbert space (or index set) $d$, if $d$ is non-empty, there exists a default mixed state $\rho \in \text{MState } d$. In this case, the default state is defined to be the maximally mixed state $\rho_{\text{unif}}$.

For a finite-dimensional quantum system with basis index set $d$, if $d$ is non-empty, the default mixed state $\rho \in \text{MState } d$ provided by the `Inhabited` instance is equal to the maximally mixed state $\rho_{\text{unif}}$.

Let $d$ be a finite type with exactly one element (i.e., $d$ is a singleton set). Let $\text{default}$ denote the default mixed quantum state in $\text{MState } d$, which is defined as the maximally mixed state. Then the matrix representation $M$ of this default state is equal to the scalar $1$ (identifying the $1 \times 1$ matrix with its unique entry).

Given a quantum mixed state $\rho$ of a composite system with state space $d_1 \times d_2$, the partial trace operation $\text{traceLeft}$ maps $\rho$ to a reduced mixed state in $d_2$. This is defined by taking the partial trace over the first ("left") subsystem, such that the resulting density matrix $M$ is $\text{Tr}_1(\rho)$. The operation ensures the resulting matrix remains positive semi-definite and has a trace of $1$.

Given a mixed state $\rho$ of a composite system with dimensions $d_1 \times d_2$, represented as a density matrix in $\text{MState}(d_1 \times d_2)$, the operation $\text{traceRight}$ maps $\rho$ to a mixed state in $\text{MState}(d_1)$. This is achieved by taking the partial trace over the second subsystem (the "right" half), resulting in the reduced density matrix $\rho_1 = \text{Tr}_2(\rho)$. The resulting matrix preserves the properties of a mixed state, specifically being positive semi-definite and having a trace of 1.

Given two quantum mixed states $\rho_1$ and $\rho_2$ associated with Hilbert spaces of dimensions $d_1$ and $d_2$ respectively, then taking the partial trace over the first subsystem of their tensor product $\rho_1 \otimes \rho_2$ recovers the state $\rho_2$. That is, $\text{Tr}_1(\rho_1 \otimes \rho_2) = \rho_2$.

Given two quantum mixed states $\rho_1$ and $\rho_2$ associated with Hilbert spaces of dimensions $d_1$ and $d_2$ respectively, taking the partial trace over the second (right) subsystem of their tensor product $\rho_1 \otimes \rho_2$ recovers the state $\rho_1$. That is, $\text{Tr}_2(\rho_1 \otimes \rho_2) = \rho_1$.

For any two finite-dimensional quantum mixed states $\rho_1$ and $\rho_2$ with dimensions $d_1$ and $d_2$ respectively, there exists a permutation $\sigma$ of the index set $d_1 \times d_2$ such that for all $i \in d_1$ and $j \in d_2$, the spectrum of the tensor product state $\rho_1 \otimes \rho_2$ satisfies $(\rho_1 \otimes \rho_2).\text{spectrum}(\sigma(i, j)) = \rho_1.\text{spectrum}(i) \cdot \rho_2.\text{spectrum}(j)$. Here, the spectrum of a mixed state refers to the probability distribution formed by the eigenvalues of its density matrix.

For any two finite-dimensional quantum mixed states $\rho$ and $\sigma$ represented as matrices, the infimum of the spectrum of their tensor product $\rho \otimes \sigma$ is equal to the product of the infimum of the spectrum of $\rho$ and the infimum of the spectrum of $\sigma$. Here, $\text{sInf}(\text{spectrum}(\cdot))$ denotes the smallest eigenvalue of the density matrix.

Let $\rho$ be a mixed quantum state on a composite system $d_1 \times d_2$, represented by a matrix $\rho.M$. The state $\rho$ is said to be separable if there exists a finite ensemble of pairs of mixed states $(\rho_{L,i}, \rho_{R,i}) \in \text{MState } d_1 \times \text{MState } d_2$ and a probability distribution $p_i$ such that the matrix $\rho.M$ can be written as the convex combination: $$\rho.M = \sum_{i} p_i (\rho_{L,i}.M \otimes \rho_{R,i}.M)$$ where $\otimes$ denotes the Kronecker product of the individual state matrices.

For any two finite-dimensional quantum mixed states $\rho_1$ and $\rho_2$, their product state $\rho_1 \otimes \rho_2$ is separable. A mixed state $\rho$ on a composite system $d_1 \times d_2$ is defined as separable if its density matrix can be expressed as a convex combination of product states, $\rho.M = \sum_{i} p_i (\rho_{L,i}.M \otimes \rho_{R,i}.M)$, where $p_i$ is a probability distribution.

For any two finite-dimensional quantum mixed states $\rho_1$ and $\rho_2$ defined on Hilbert spaces with finite dimensions $d_1$ and $d_2$ respectively, the purity of their tensor product $\rho_1 \otimes \rho_2$ is equal to the product of their individual purities: $$\text{purity}(\rho_1 \otimes \rho_2) = \text{purity}(\rho_1) \cdot \text{purity}(\rho_2)$$ where the purity is defined as the trace of the square of the density matrix, $\text{Tr}(\rho^2)$.

Let $d$ be a finite index set and let $|\psi\rangle, |\phi\rangle$ be quantum state vectors (kets) in the Hilbert space $\mathbb{C}^d$. The pure states defined by these vectors are equal, $\text{pure}(|\psi\rangle) = \text{pure}(|\phi\rangle)$, if and only if there exists a complex phase $z \in \mathbb{C}$ with unit norm $\|z\| = 1$ such that $|\psi\rangle = z |\phi\rangle$.

Let $d$ be a finite index set and let $|\psi\rangle$ and $|\phi\rangle$ be kets (state vectors) in the $d$-dimensional Hilbert space. The kets $|\psi\rangle$ and $|\phi\rangle$ are phase-equivalent if and only if their corresponding pure mixed states (density matrices) are equal, i.e., $|\psi\rangle \langle\psi| = |\phi\rangle \langle\phi|$.

Given a finite-dimensional Hilbert space with basis $d$, let $\text{Ket } d$ denote the space of pure state vectors. Define an equivalence relation on these vectors such that $\psi \sim \phi$ if $\psi = e^{i\theta} \phi$ (i.e., they differ only by a global phase). Let $\text{KetUpToPhase } d$ be the quotient space under this relation. The function maps an equivalence class of kets $[\psi]$ to its corresponding mixed state $\rho = |\psi\rangle\langle\psi|$ in the space of density matrices $\text{MState } d$. This is well-defined because the map from a ket to its projection operator is invariant under global phase shifts.