QuantumInfo.Finite.MState
Finite dimensional quantum mixed states, ρ.
The same comments apply as in `Braket`:
These could be done with a Hilbert space of Fintype, which would look like ```lean4 (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [FiniteDimensional ℂ H] ``` or by choosing a particular `Basis` and asserting it is `Fintype`. But frankly it seems easier to mostly focus on the basis-dependent notion of `Matrix`, which has the added benefit of an obvious "classical" interpretation (as the basis elements, or diagonal elements of a mixed state). In that sense, this quantum theory comes with the a particular classical theory always preferred.
Important definitions: * `instMixable`: the `Mixable` instance allowing convex combinations of `MState`s * `ofClassical`: Mixed states representing classical distributions * `purity`: The purity `Tr[ρ^2]` of a state * `spectrum`: The spectrum of the matrix * `uniform`: The maximally mixed state * `mix`: The total state corresponding to an ensemble * `average`: Averages a function over an ensemble, with appropriate weights
126 declarations
Coercion from `MState d` to `HermitianMat d ℂ`
For a finite index set , there exists a coercion that maps a quantum mixed state of type `MState d` to its underlying representation as a complex Hermitian matrix . This allows a mixed state to be treated as a Hermitian matrix in mathematical contexts.
The underlying matrix of a mixed state
For a quantum mixed state of finite dimension , the function returns the underlying complex matrix representation of the state. It is defined as the matrix component of the Hermitian operator associated with .
The matrix of the Hermitian operator of a mixed state equals
For a quantum mixed state of dimension , the underlying matrix of the Hermitian operator associated with is equal to the matrix representation of the state . Specifically, let ; then the identity holds.
The Hermitian operator of a mixed state is strictly positive ()
Let be a quantum mixed state of finite dimension . Let be the Hermitian operator associated with . Then is strictly positive-definite, denoted by .
Positivity extension for mixed state operator
The definition provides a tactic extension for the `positivity` framework to automatically prove that the Hermitian operator associated with a finite-dimensional quantum mixed state is strictly positive-definite (). By analyzing the expression representing the operator projection , the tactic extracts the state and constructs a proof of its positivity using the lemma `MState.pos`.
Mixed States are Positive Semidefinite
For a finite-dimensional quantum mixed state , its associated matrix implementation is positive semidefinite.
Mixed States are Hermitian
Let be a finite-dimensional quantum mixed state of dimension . Let denote the density matrix in associated with the state. The matrix is Hermitian, meaning it is equal to its own conjugate transpose, .
The Trace of a Mixed State Density Matrix is 1
Let be a finite-dimensional quantum mixed state of dimension . Let denote the density matrix in associated with the state. The trace of the density matrix is equal to 1, i.e., .
Equality of Mixed States is Determined by Their Density Matrices
Let and be finite-dimensional quantum mixed states of dimension . If the density matrices associated with these states are equal, i.e., , then the mixed states themselves are equal, .
The map is injective
Let be a finite dimension associated with a quantum system. Let be quantum mixed states in , and let denote the density matrix in associated with a mixed state . The mapping is injective; that is, if , then .
Injectivity of the density matrix mapping for mixed states
For a finite-dimensional quantum system of dimension , the map that assigns a density matrix to each mixed state is injective. That is, for any two mixed states and , if , then .
The set of mixed states is convex
The set of all matrices corresponding to finite-dimensional mixed states of dimension (the range of the map `MState.M`) is a convex set over the real numbers .
`MState d` is mixable over Hermitian matrices
The type `MState d`, representing mixed states of a -dimensional quantum system, is an instance of a `Mixable` structure over the space of Hermitian matrices . 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 .
The dimension index of a mixed state must be non-empty
For a finite-dimensional quantum mixed state of dimension to exist, the underlying index type must be non-empty (i.e., must have at least one element).
Eigenvalues of a Mixed State are Non-negative
For any finite dimensional quantum mixed state and any index of its basis, the -th eigenvalue of the Hermitian matrix associated with is non-negative, i.e., .
Eigenvalues of a Mixed State are at most 1
For any finite-dimensional quantum mixed state and any index , the -th eigenvalue of the Hermitian matrix associated with is less than or equal to 1, i.e., .
Density Matrix of a Mixed State is Bound by the Identity
For any finite dimensional quantum mixed state with associated density matrix , the matrix is less than or equal to the identity matrix in the Loewner order, denoted as . This means that is a positive semi-definite matrix, or equivalently, all eigenvalues of satisfy .
Inner product of mixed states
For any two quantum mixed states and in a Hilbert space of dimension , their inner product is defined as the Hilbert-Schmidt inner product of their corresponding density matrices and , given by . This value is a real number in the interval , where the non-negativity follows from the positive semi-definiteness of the states, and the upper bound follows from the fact that for mixed states, .
Definition of the inner product for mixed states
The inner product between two mixed states and in the probability sense, denoted , is defined as the inner product of their underlying matrices . This value is guaranteed to be non-negative because the state matrices are positive semi-definite ( and ), and it is bounded above by , as shown by the transition from the inequality to since mixed states have unit trace.
The probability inner product of mixed states and equals the Frobenius inner product of their density matrices and .
Let and be mixed states of dimension . Let and denote their corresponding density matrices in . The real-valued inner product of the states and in the probability inner product space, denoted by , is equal to the Frobenius inner product of their underlying matrices, .
Complex expectation value of a matrix in state
Given a mixed state with an underlying density matrix and a complex matrix , the complex-valued expectation value of with respect to is defined as the trace of the product of and :
Expectation value of a Hermitian operator in state
For a quantum mixed state with density matrix and a Hermitian operator (represented by a Hermitian matrix in ), the expectation value of in state is the real number defined by the Frobenius inner product of and : Since and are Hermitian, this is equivalent to .
The expectation value of a positive semi-definite operator in a mixed state is non-negative.
Let be a finite-dimensional quantum mixed state and let be a Hermitian matrix. If is positive semi-definite (i.e., ), then the expectation value of with respect to , denoted by , is a non-negative real number ().
The expectation value of the zero operator is
For a quantum mixed state , the expectation value of the zero operator is . That is, .
The expectation value of the identity operator is
Let be a finite-dimensional quantum mixed state. The expectation value of the identity matrix with respect to , denoted as , is equal to .
If , then the expectation value of is .
Let be a finite-dimensional quantum mixed state and let be a Hermitian matrix of dimension over . If satisfies the operator inequality , where is the identity matrix, then the expectation value of with respect to is less than or equal to 1, i.e., .
Expectation value of an operator is in
Let be a finite-dimensional quantum mixed state and let be a Hermitian matrix of dimension over . If satisfies the operator inequality (meaning is a positive semidefinite operator bounded above by the identity matrix), then the expectation value of with respect to , denoted , lies in the unit interval , i.e., .
Linearity of expectation value under subtraction:
Let be a finite-dimensional quantum mixed state and let and be Hermitian matrices of dimension over . The expectation value of the difference with respect to the state is equal to the difference of their individual expectation values: where denotes the expectation value of an operator in state .
for
Let be a quantum mixed state with density matrix , and let be a positive semidefinite (PSD) Hermitian matrix of dimension over (i.e., ). The expectation value of in the state , defined as , is equal to if and only if the support of the density matrix is a subspace of the kernel of , denoted .
for
Let be a quantum mixed state and be a Hermitian matrix acting on a -dimensional complex Hilbert space such that , where denotes the identity matrix. The expectation value of on the state , denoted by , is equal to if and only if the support of the density matrix is contained within the kernel of . In other words, must be entirely supported on the -eigenspace of .
Linearity of Expectation:
Let be a mixed state of a finite-dimensional quantum system and let and be Hermitian matrices. The expectation value of the sum of the matrices is equal to the sum of their individual expectation values, such that .
Linearity of Quantum Expectation:
Let be a quantum mixed state of dimension . For any real number and any Hermitian matrix , the expectation value of the scalar multiple of the matrix is given by times the expectation value of . That is, .
Monotonicity of Quantum Expectation Values with respect to
Let be a quantum mixed state of dimension . For any two Hermitian matrices , if (meaning is a positive semi-definite matrix), then the expectation value of with respect to is less than or equal to the expectation value of with respect to , denoted as .
Pure state density matrix
Let be a finite index set and be a ket in the -dimensional Hilbert space (represented as `Ket d`). A pure mixed state can be constructed from as the density matrix defined by the outer product . Formally, its matrix elements are given by . This state is positive semi-definite and has a trace of 1, provided that is normalized.
Matrix elements of a pure state
Let be a finite index set and be a quantum state vector (represented as a function from to ). The density matrix corresponding to the pure state , denoted by , has elements defined for any indices as where denotes the complex conjugate of the component . This corresponds to the standard definition of the pure state density matrix .
The density matrix of a pure state is idempotent ()
Let be a finite index set and be a quantum state vector in . Let be the density matrix corresponding to the pure state of , denoted formally as `(pure ψ).m`. Then the square of this density matrix is equal to itself: In other words, the density matrix of any pure state is idempotent.
Purity of a mixed state
The purity of a finite-dimensional quantum mixed state , represented as a matrix in , is defined as the trace of the square of the density matrix, . This value is returned as a probability , reflecting that . In the formal implementation, this is calculated via the inner product defined on the space of mixed states.
Eigenvalue spectrum of a mixed state
Given a mixed quantum state , represented as a density matrix in , its spectrum is defined as the probability distribution on the set of indices formed by the eigenvalues of the underlying Hermitian matrix. Specifically, for a state , the spectrum is the distribution whose mass at each point corresponds to an eigenvalue of the matrix , where the non-negativity of the probabilities is guaranteed by the positive semi-definiteness of , and the normalization to unity is guaranteed by the property .
The spectrum of a pure state is a constant distribution
For any normalized quantum state vector (represented as a `Ket d`), the eigenvalue spectrum of the corresponding pure mixed state is a constant probability distribution. That is, there exists an index such that the spectrum of is equal to the distribution , where all probability mass is concentrated at a single outcome.
If the spectrum of is a constant distribution, then is a pure state
Let be a quantum mixed state of dimension . If the eigenvalue spectrum of is a constant distribution (meaning there exists an index such that the spectrum assigns probability 1 to and 0 to all other indices), then is a pure state, i.e., there exists a state vector such that .
A mixed state is pure if and only if its spectrum is a constant distribution
Let be a mixed quantum state in a -dimensional Hilbert space. The state is a pure state (i.e., there exists a unit vector such that ) if and only if its eigenvalue spectrum is a constant distribution, meaning there exists an index such that the spectrum of is equal to the distribution which assigns probability 1 to and 0 elsewhere.
is a Pure State if and only if its Purity
Let be a finite-dimensional quantum mixed state of dimension . Then is a pure state (i.e., there exists a ket vector such that ) if and only if its purity, defined as , is equal to .
Spectral Decomposition of a Mixed State into Pure States
For any finite-dimensional quantum mixed state of dimension , there exists an orthonormal basis of ket vectors such that the Hermitian operator associated with can be written as the weighted sum of pure state operators: where are the probabilities given by the spectrum of the state (i.e., ).
Tensor product of mixed states
Given two quantum mixed states and acting on Hilbert spaces of dimensions and respectively, their product state is a mixed state acting on the tensor product space of dimension . The density matrix of the product state is defined by the Kronecker product of the individual density matrices, , which is shown to be positive semi-definite and have unit trace.
Infix operator for Mixed State Tensor Product
An infix notation used to represent the tensor product of two quantum mixed states, corresponding to the operation `MState.prod`. Given two mixed states and , the expression denotes the resulting mixed state on the product space, where the underlying density matrix is the Kronecker product of the individual density matrices.
Inner Product of Tensor Product States
For any quantum mixed states and in a Hilbert space of dimension , and mixed states and in a Hilbert space of dimension , the inner product of their tensor products is the product of their individual inner products: where denotes the tensor product of mixed states and denotes the Hilbert-Schmidt inner product scaled to the interval .
Let and be quantum state vectors (kets) in Hilbert spaces of dimensions and respectively. The pure mixed state formed from their tensor product , denoted as , is equal to the tensor product of the individual pure mixed states . In terms of density matrices, this expresses that .
Quantum representation of a classical probability distribution as a diagonal density matrix
Given a finite set of outcomes and a probability distribution over , the function `ofClassical` constructs a quantum mixed state (density matrix) . The resulting density matrix is a diagonal matrix in the computational basis, where each diagonal entry is equal to the probability of the corresponding classical outcome , and all off-diagonal entries are zero for .
The density matrix of a classical distribution is diagonal
Let be a finite set of states and be a probability distribution over , where denotes the probability of outcome . The density matrix associated with the classical mixed state is equal to the diagonal matrix over the complex numbers whose diagonal entries are given by the probabilities . That is, and for .
Real Power of the Density Matrix of a Classical Distribution is Diagonal with Entries
Let be a finite set of states and be a probability distribution over , where denotes the probability of outcome . For the density matrix associated with the classical mixed state and any real power , the matrix power is equal to the diagonal matrix over the complex numbers whose diagonal entries are the probabilities raised to the power . That is, and for .
The maximally mixed state over
For a finite-dimensional quantum system with basis index set , where is non-empty, the maximally mixed state is defined as the mixed state corresponding to the uniform classical probability distribution over . In this state, the density matrix is given by , where is the identity matrix and is the cardinality of the set .
The mixed state on a 1D system is unique
For a quantum system whose underlying basis type has exactly one element (representing a 1-dimensional Hilbert space), there exists exactly one mixed state . In this case, the unique state is the maximally mixed (uniform) state.
The maximally mixed state is the default `Inhabited` instance for `MState d` when
For a finite-dimensional Hilbert space (or index set) , if is non-empty, there exists a default mixed state . In this case, the default state is defined to be the maximally mixed state .
The default mixed state is the maximally mixed state
For a finite-dimensional quantum system with basis index set , if is non-empty, the default mixed state provided by the `Inhabited` instance is equal to the maximally mixed state .
The matrix of the default state on a unique basis is 1
Let be a finite type with exactly one element (i.e., is a singleton set). Let denote the default mixed quantum state in , which is defined as the maximally mixed state. Then the matrix representation of this default state is equal to the scalar (identifying the matrix with its unique entry).
Partial trace over the left subsystem
Given a quantum mixed state of a composite system with state space , the partial trace operation maps to a reduced mixed state in . This is defined by taking the partial trace over the first ("left") subsystem, such that the resulting density matrix is . The operation ensures the resulting matrix remains positive semi-definite and has a trace of .
Partial trace over the right subsystem
Given a mixed state of a composite system with dimensions , represented as a density matrix in , the operation maps to a mixed state in . This is achieved by taking the partial trace over the second subsystem (the "right" half), resulting in the reduced density matrix . 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 and associated with Hilbert spaces of dimensions and respectively, then taking the partial trace over the first subsystem of their tensor product recovers the state . That is, .
Given two quantum mixed states and associated with Hilbert spaces of dimensions and respectively, taking the partial trace over the second (right) subsystem of their tensor product recovers the state . That is, .
The spectrum of is the pairwise product of the spectra of and up to a permutation
For any two finite-dimensional quantum mixed states and with dimensions and respectively, there exists a permutation of the index set such that for all and , the spectrum of the tensor product state satisfies . Here, the spectrum of a mixed state refers to the probability distribution formed by the eigenvalues of its density matrix.
The Smallest Eigenvalue of a Tensor Product equals the Product of Smallest Eigenvalues
For any two finite-dimensional quantum mixed states and represented as matrices, the infimum of the spectrum of their tensor product is equal to the product of the infimum of the spectrum of and the infimum of the spectrum of . Here, denotes the smallest eigenvalue of the density matrix.
Separability of a Mixed State
Let be a mixed quantum state on a composite system , represented by a matrix . The state is said to be separable if there exists a finite ensemble of pairs of mixed states and a probability distribution such that the matrix can be written as the convex combination: where denotes the Kronecker product of the individual state matrices.
Product States are Separable
For any two finite-dimensional quantum mixed states and , their product state is separable. A mixed state on a composite system is defined as separable if its density matrix can be expressed as a convex combination of product states, , where is a probability distribution.
Purity of Tensor Product is the Product of Purities
For any two finite-dimensional quantum mixed states and defined on Hilbert spaces with finite dimensions and respectively, the purity of their tensor product is equal to the product of their individual purities: where the purity is defined as the trace of the square of the density matrix, .
Equality of pure states iff and differ by a phase
Let be a finite index set and let be quantum state vectors (kets) in the Hilbert space . The pure states defined by these vectors are equal, , if and only if there exists a complex phase with unit norm such that .
Phase Equivalence of Kets iff
Let be a finite index set and let and be kets (state vectors) in the -dimensional Hilbert space. The kets and are phase-equivalent if and only if their corresponding pure mixed states (density matrices) are equal, i.e., .
Map from kets modulo phase to pure mixed states
Given a finite-dimensional Hilbert space with basis , let denote the space of pure state vectors. Define an equivalence relation on these vectors such that if (i.e., they differ only by a global phase). Let be the quotient space under this relation. The function maps an equivalence class of kets to its corresponding mixed state in the space of density matrices . This is well-defined because the map from a ket to its projection operator is invariant under global phase shifts.
The mixed state of a ket up to phase equals the pure state of that ket
Let be a finite type with decidable equality. For any state vector in the Hilbert space , the mixed state associated with the equivalence class of under phase equivalence (denoted as ) is equal to the pure state density matrix (denoted as ).
The Map from Kets Modulo Phase to Pure Mixed States is Injective
Let be a finite type with decidable equality. Let be the map that takes an equivalence class of kets under global phase equivalence (an element of ) to its corresponding pure mixed state (an element of ). Then the function is injective.
If the Pure Mixed State is Separable, then is a Product State
Let and be finite types. For any state vector (represented as a ) in the composite Hilbert space of dimension , if the corresponding pure mixed state (denoted `pure ψ`) is separable, then the state vector is a product state (i.e., can be written as for some and ).
A pure state is separable iff is a product state
Let be a ket in the composite Hilbert space . The pure state density matrix (represented as `pure ψ`) is separable if and only if the state vector is a product state (i.e., there exist and such that ).
A mixed state is pure
Let be a finite type. For a quantum mixed state of dimension with associated density matrix , is a pure state (i.e., there exists a state vector such that ) if and only if the rank of its density matrix is equal to , denoted .
is a product state iff its coefficient matrix has rank 1
Let and be finite types. Let be a ket in the product space , where is represented as a function mapping pairs to complex numbers . is a product state if and only if the rank of its coefficient matrix , defined by , is equal to .
A pure state is separable iff its partial trace is pure
Let be a quantum state (ket) in a composite Hilbert space , where and are finite dimensions. The pure mixed state is separable if and only if the partial trace over the first subsystem, , is a pure state.
The purification of a mixed state
Given a mixed state (represented as a density matrix ), its purification is a pure state (a ket) in the doubled Hilbert space . The vector components are defined by , where is the unitary matrix of eigenvectors and are the eigenvalues of the Hermitian matrix representing . This construction ensures that the partial trace of the resulting pure state density matrix over the second subsystem recovers original state, i.e., .
Partial Trace of Purification Recovers the Original Mixed State
Let be a quantum mixed state of dimension . Let be the purification of , which is a pure state (ket) in the composite Hilbert space of dimension . Then, taking the partial trace of the pure state density matrix over the second subsystem recovers the original mixed state . That is,
The purification of a mixed state as a subtype with
Given a mixed state in a -dimensional Hilbert space, this definition provides a pure state (represented as a `Ket`) in the product space of dimension such that the partial trace over the second subsystem of the pure state density matrix recovers the original mixed state . Specifically, it returns a subtype consisting of a state vector and a proof that .
Relabeling of a mixed state via bijection
Given a quantum mixed state on a system with basis , and a bijection (equivalence) , the function returns a new mixed state on a system with basis . The resulting state is defined by reindexing the underlying density matrix such that the matrix elements satisfy for .
The matrix of a relabeled mixed state is the reindexed submatrix of the original state's matrix.
Let be a mixed state on a -dimensional Hilbert space, represented by the matrix . Given a bijection between index sets, the matrix of the relabeled state is equal to the submatrix of formed by reindexing both rows and columns by . That is, .
For any finite dimensional quantum mixed state indexed by a set , relabeling the state by the identity bijection results in the original mixed state , i.e., .
Relabeling a pure state yields a pure state
Given a pure state associated with a state vector in a Hilbert space indexed by , and a bijection between index sets, there exists a state vector in the Hilbert space indexed by such that the relabeled mixed state is the pure state .
Let be finite types with decidable equality. For any quantum mixed state on and any two bijections and , relabeling the state by and then relabeling the result by is equivalent to relabeling by the composition of the bijections (denoted ).
Composition of mixed state relabeling
Let be finite types with decidable equality. For a quantum mixed state on and two equivalences (bijections) and , relabeling by and then by is equivalent to relabeling by the composite equivalence (denoted as ).
Relabeling a mixed state by an equality is equivalent to type casting
Let and be finite types with decidable equality. For any quantum mixed state defined over the index set and any equality , the state obtained by relabeling using the equivalence induced by is equal to the state obtained by casting along the equality of their types.
The spectrum of a mixed state is invariant under relabeling
Let and be finite types. For a quantum mixed state defined on the index set and an equivalence (bijection) , the spectrum of the density matrix of the relabeled state is equal to the spectrum of the density matrix of the original state .
Purity is Invariant Under Relabeling of Basis
Let and be finite types. For any quantum mixed state on the index set and any bijection , the purity of the relabeled state, , is equal to the purity of the original state, . Here, purity is defined as .
Heterogeneous SWAP gate for mixed states
Given a quantum mixed state defined on a composite system with index set , the SWAP operation produces a new mixed state on the index set by relabeling the basis elements using the symmetry of the Cartesian product (i.e., mapping to ). This heterogeneous gate effectively exchanges the left and right halves of the quantum system, even if the dimensions of and differ.
Spectrum of a Mixed State is Invariant Under Relabeling
Let and be finite types with decidable equality. For any mixed state on and any equivalence used to relabel the state, the multiset of values in the spectrum of the relabeled state is equal to the multiset of values in the spectrum of the original state .
The spectrum of a mixed state is invariant under up to a relabeling .
Let and be finite types. For any bipartite mixed quantum state , represented as a density matrix on the tensor product space , there exists an equivalence (relabeling) such that the eigenvalue spectrum of the swapped state is equal to the spectrum of the original state after relabeling. This captures the fact that the spectrum of a density matrix is invariant under the swapping of its subsystems, up to a permutation of the index set.
The Operation on Mixed States is an Involution
Let and be finite types representing the dimensions of a bipartite quantum system. For any mixed state defined on the product space , applying the operation twice returns the state to its original form, i.e., .
Let be a mixed state of a bipartite system with dimensions . Let denote the state obtained by swapping the two subsystems. Then, the partial trace of the swapped state over its left subsystem (formerly the second subsystem) is equal to the partial trace of the original state over its right subsystem, i.e., .
Let be a mixed state of a bipartite quantum system with dimensions . Let denote the state where the two subsystems are interchanged, resulting in a state on . Then, the partial trace of over the right subsystem (the second subsystem of the swapped state, which corresponds to ) is equal to the partial trace of the original state over the left subsystem (the first subsystem, ), such that .
Quantum state associator from to
Given a quantum mixed state on a tripartite system structured as , the function `MState.assoc` is the associator that maps to a mixed state on the re-clustered system . This is achieved by relabeling the basis elements of the density matrix using the inverse of the standard product associativity equivalence .
Quantum state associator from to
Given a quantum mixed state on a tripartite system with dimensions , the function `MState.assoc'` is the associator that maps to a mixed state on the re-clustered system . This operation re-groups the components of the quantum system while preserving the underlying state.
for quantum mixed states
Let be a quantum mixed state on a tripartite system with dimensions . Let be the associator that maps the state to the re-grouped system , and let be the inverse associator mapping back to . Then, applying followed by to the state results in the original state .
and are inverses for quantum mixed states
Let be a quantum mixed state on the tensor product space indexed by . Let denote the isomorphism that reassociates the state into the space , and let be its inverse operation. Then applying followed by to the state returns the original state .
Compatibility of Partial Traces and Associativity for Tripartite Mixed States
Let be a mixed state on the tripartite system . Let be the state reassociated into the system . Then the partial trace of over , followed by a partial trace over to leave a state on , is equal to the partial trace of over , followed by a partial trace over . In short, .
for tripartite mixed states
Let be a quantum mixed state on a tripartite system with dimensions . Let be the state reassociated into the system . Then the partial trace of over the third subsystem , followed by the partial trace over the first subsystem to leave a state on , is equal to the partial trace of over the first subsystem , followed by the partial trace over the third subsystem . Mathematically, .
Let be a mixed state on the tripartite system . Let denote the state reassociated into the system . Then the partial trace of over the third subsystem is equal to the partial trace of over followed by the partial trace over . Mathematically, .
Left Partial Trace is Consistent under Reassociation
Let be a mixed state on a tripartite system. Let denote the natural reassociator of the tensor products shifting from to . Then, the partial trace over the first two subsystems of is equivalent to taking the partial trace over the first subsystem of the reassociated state. That is, where refers to tracing out the leftmost subsystem in the current grouping.
Nested Left Partial Traces of Reassociated Mixed State Equals Left Partial Trace of Original State
Let be a mixed state on the tripartite system . Let be the map that reassociates the state to the system . Then, taking the partial trace over the first two subsystems of the reassociated state (i.e., tracing over and then ) is equivalent to taking the partial trace over the first subsystem of the original state (i.e., tracing over ). Mathematically, .
Nested Right Partial Traces of Reassociated Mixed State Equals Right Partial Trace of Original State
Let be a mixed state on the tripartite system . Let denote the associator that re-clusters the system into . Then, taking the partial trace over the third and then the second subsystem of (the rightmost subsystems in the re-clustered grouping) is equivalent to taking the partial trace over the entire rightmost composite subsystem of the original state . Mathematically, this is expressed as: where denotes the partial trace over the right-hand component of the current bipartite grouping.
The Trace Norm of a Mixed State Density Matrix is 1
Let be a finite-dimensional quantum mixed state of dimension . Let denote the density matrix in associated with the state. The trace norm of the density matrix is equal to 1, i.e., .
Left-side relabeling commutes with the tensor product of mixed states:
Let be a mixed quantum state on a Hilbert space with basis , and be a mixed quantum state on a Hilbert space with basis . Let be an equivalence (relabeling) of basis indices. Then the tensor product of the relabeled state and is equal to the relabeled tensor product of and , specifically: where is the product congruence of the equivalence and the identity on .
Let and be quantum mixed states on Hilbert spaces with basis sets and respectively. Let be an equivalence (relabeling) of basis indices. Then the tensor product of with the relabeled state is equal to the relabeled tensor product of and , such that , where is the identity map on and denotes the product congruence of the index sets.
For any three quantum mixed states , , and with dimensions and respectively, the tensor product follows an associative property up to a relabeling of the basis. Specifically, the state is equal to the state after applying a relabeling defined by the inverse of the natural associativity equivalence of the underlying index sets .
Subspace topology for mixed states
The type of mixed states is equipped with the induced topology (subspace topology) from the space of complex-valued matrices . Under this topology, is treated as a topological space where the open sets are the intersections of the open sets of the matrix space with the set of density matrices.
The map from to matrices is a topological embedding
The map which assigns to each quantum mixed state in its corresponding complex Hermitian matrix is a topological embedding. This means that the map is injective and that the topology on the space of mixed states is the subspace topology induced by the space of matrices .
is a Space
The space of finite-dimensional quantum mixed states (represented as density matrices) is a space (a regular Hausdorff space). This topological property is inherited from the embedding of mixed states into the space of complex matrices.
The space of mixed states is compact
For any finite dimension , the space of quantum mixed states (represented as the set of density matrices) is a compact topological space.
Metric space structure on
The space of finite-dimensional quantum mixed states (represented by density matrices) is equipped with a metric space structure. This metric is induced by the injective mapping from the space of mixed states into the space of complex matrices , inheriting the standard metric from the latter.
Distance between mixed states equals distance between density matrices
For any two quantum mixed states and in a -dimensional Hilbert space, the distance between them is equal to the distance between their underlying density matrices and , i.e., . Here, the distance on the right-hand side is the standard metric on the space of complex matrices.
The space of -dimensional mixed states is bounded.
For any finite dimension , the space of quantum mixed states (density matrices) of dimension , denoted by , is a bounded metric space.
Continuity of the Mixed State to Hermitian Matrix Mapping
The mapping that assigns to each quantum mixed state in a -dimensional Hilbert space its underlying Hermitian density matrix is continuous with respect to the subspace topology on the space of mixed states and the standard topology on the space of complex-valued matrices.
Continuity of the Mixed State to Matrix Mapping
The function , which maps a mixed state in a -dimensional Hilbert space to its corresponding matrix representation in , is continuous.
The set of matrices representing any collection of mixed states is bounded.
For any set of mixed states in a -dimensional Hilbert space, the image of under the mapping (which associates a mixed state with its underlying Hermitian matrix) is a bounded set in the space of matrices.
Tensor product of mixed states
Given a family of mixed states indexed by , where each is a mixed state on a Hilbert space with basis , the function constructs the product mixed state on the tensor product space with basis . The resulting mixed state is represented by the matrix , which is the Kronecker product (tensor product) of the individual density matrices. This construction preserves the properties of being a mixed state: it is Hermitian, positive semi-definite, and has a trace of 1.
-fold tensor power of a mixed state
Given a mixed state on a Hilbert space with basis and a natural number , the -copy power function constructs the product state . This is defined as the tensor product of copies of , resulting in a mixed state on the tensor product space with the standard basis indexed by the type . The resulting state is represented by the matrix formed by the -fold Kronecker power of the density matrix of .
-fold tensor power operator for mixed states
The infix operator denotes the -fold tensor power of a mixed state. Given a mixed state of dimension and a natural number , produces a mixed state on the -fold product space (represented as the type ).
The Kronecker product of positive definite mixed states is positive definite
Let and be finite types with decidable equality. For any two finite-dimensional quantum mixed states (on the space indexed by ) and (on the space indexed by ), if their underlying matrices and are positive definite, then the underlying matrix of their Kronecker product (tensor product state) is also positive definite.
Relabeling a Positive Definite Mixed State Preserves Positive Definiteness
Let and be finite types with decidable equality. Let be a quantum mixed state on , represented by the matrix . If the matrix is positive definite, then for any equivalence , the matrix representing the relabeled state is also positive definite.
Convex mixtures of positive definite mixed states are positive definite
Let be a finite set representing the dimensions of a quantum system. For any two mixed states (represented by their density matrices and ), if both and are positive definite, then for any probability , the matrix representation of their convex mixture is also positive definite.
If is positive definite and , then the mixture is positive definite
Let be a finite type with decidable equality. For any two quantum mixed states , if the matrix representation of is positive definite (i.e., ) and the probability is not equal to , then the matrix representation of the convex mixture is also positive definite.
Non-degenerate mixture with a positive definite state is positive definite
Let be a finite dimensional Hilbert space and let be quantum mixed states (density matrices) in . If is positive definite () and the probability is not equal to , then the convex mixture is also positive definite.
The maximally mixed state is positive definite
Let be a non-empty finite set. The density matrix associated with the maximally mixed state of dimension is positive definite.
Density matrices in a one-dimensional Hilbert space are positive definite
Let be a finite type with a unique element (). For any quantum mixed state of dimension , the corresponding density matrix is positive definite.
