QuantumInfo.ForMathlib.Matrix

Let $A$ be an $n \times n$ matrix over a field $\mathbb{k}$, where the index set $n$ is finite. If the rank of the matrix $A$ is 0, then $A$ is the zero matrix.

Let $A$ be a Hermitian matrix and $c$ be a scalar in a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$). If $c$ is self-adjoint (meaning $c = \bar{c}$, or equivalently, $c$ is real-valued), then the scalar product $c \cdot A$ is also a Hermitian matrix.

Let $A$ be a Hermitian matrix and $c$ be a scalar in a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$). If the imaginary part of $c$ is zero, then the scalar product $c \cdot A$ is also a Hermitian matrix.

Let $A$ be a Hermitian matrix and $c$ be a real number. Then the scalar product $c \cdot A$ is also a Hermitian matrix. Here, a matrix $A$ is Hermitian if it equals its conjugate transpose ($A = A^*$), and $c \cdot A$ denotes the multiplication of each entry of $A$ by the real scalar $c$.

Given a finite set $n$ and a field $\mathbb{k}$ that is either the real numbers $\mathbb{R}$ or the complex numbers $\mathbb{C}$ (an `RCLike` field), the set of all $n \times n$ Hermitian matrices $A$ (where $A = A^*$) forms a subspace of the vector space of all $n \times n$ matrices over $\mathbb{k}$, when considered as a vector space over the real numbers $\mathbb{R}$.

Let $A$ be a Hermitian matrix. Then the real part of the trace of $A$ is equal to the trace of $A$, implying that the trace of $A$ is a real number: $\operatorname{Re}(\operatorname{Tr}(A)) = \operatorname{Tr}(A)$.

Let $A$ be a Hermitian matrix. The sum of the eigenvalues of $A$, denoted as $\sum_{i} \lambda_i$, is equal to the trace of the matrix, $\text{tr}(A)$. Here, $i$ ranges over the index set of the matrix dimensions.

Let $A$ be a Hermitian matrix. If all the eigenvalues $\lambda_i$ of $A$ are equal to zero for all $i$, then $A$ is the zero matrix ($A = 0$).

Let $A$ and $B$ be two matrices. The conjugate transpose (Hermitian conjugate) of the Kronecker product of $A$ and $B$, denoted $(A \otimes B)^\text{H}$, is equal to the Kronecker product of their respective conjugate transposes, $A^\text{H} \otimes B^\text{H}$.

Let $A$ and $B$ be Hermitian matrices. Then their Kronecker product $A \otimes B$ is also a Hermitian matrix.

Let $A$ be a positive semidefinite matrix. If the trace of $A$ is zero ($\text{tr}(A) = 0$), then $A$ must be the zero matrix ($A = 0$).

Let $A$ be a positive semidefinite matrix. Then the trace of $A$ is zero if and only if $A$ is the zero matrix, i.e., $\text{Tr}(A) = 0 \iff A = 0$.

Let $z$ be an element of a field $\mathbb{K}$ that is either the real numbers $\mathbb{R}$ or the complex numbers $\mathbb{C}$. The squared norm of $z$, denoted as $|z|^2$ (or `normSq z`), is equal to the product of its complex conjugate and itself, i.e., $|z|^2 = \bar{z} z$.

Let $\alpha$ be a finite set and $M, N$ be types such that $M$ has a zero element and $N$ is an additive commutative monoid. For any finitely supported function $f: \alpha \to M$ (denoted by `f : α →₀ M`) and any function $g: \alpha \to M \to N$, the sum of $g$ over the support of $f$ is equal to the sum over all $i \in \alpha$ of the conditional expression: if $f(i) \neq 0$ then $g(i, f(i))$, otherwise $0$. That is, $$\sum_{i \in \text{supp}(f)} g(i, f(i)) = \sum_{i \in \alpha} \begin{cases} g(i, f(i)) & \text{if } f(i) \neq 0 \\ 0 & \text{if } f(i) = 0 \end{cases}$$

Let $v$ be a vector in $\mathbb{K}^n$, where $\mathbb{K}$ is either the real or complex numbers. Let $v^*$ denote the complex conjugate vector of $v$ (given by $\text{conj } v$). Then the outer product of $v$ and its conjugate, defined as the matrix $v \otimes v^*$ (represented by `vecMulVec v (conj v)`), is a positive semidefinite matrix.

Let $A$ and $B$ be positive semidefinite matrices and let $c_1, c_2 \in \mathbb{K}$ be scalars such that $0 \le c_1$ and $0 \le c_2$. Then the linear combination $c_1 A + c_2 B$ is also a positive semidefinite matrix.

Let $M$ be a matrix defined such that the entry at row $i$ and column $j$ is $c$, where $c$ is a positive constant ($0 < c$), and all other entries are zero. Then $M$ is positive semidefinite if and only if $i = j$.

Let $A$ and $B$ be positive semidefinite matrices. Then their Kronecker product $A \otimes_k B$ is also a positive semidefinite matrix.

Let $A$ be a positive semidefinite matrix. Then for all vectors $x$, the quadratic form $x^* A x = 0$ if and only if $A = 0$, where $x^*$ denotes the conjugate transpose of $x$.

Let $A$ be a matrix and $c$ be a scalar in a field $\mathbb{k}$. If the scalar product $c \cdot A$ is a positive semidefinite matrix and $c > 0$, then $A$ is also a positive semidefinite matrix.

Let $A$ be a matrix. Then $A$ is positive semidefinite and its negation $-A$ is also positive semidefinite if and only if $A$ is the zero matrix ($A = 0$).

Let $A$ be a positive definite matrix. Then the kernel of the linear map $A. \text{toLin}'$ associated with $A$ is trivial, i.e., $\ker(A) = \{0\}$ (represented as $\text{ker } A = \bot$).

Let $A$ be a matrix. If the kernel of the linear map defined by $A$ is trivial (i.e., $\ker(A) = \{0\}$) and $A$ is positive semidefinite, then $A$ is positive definite.

Let $d$ be a finite type with decidable equality, and let $A$ and $B$ be $d \times d$ Hermitian matrices over the complex numbers $\mathbb{C}$. The kernel of the linear map associated with $A$ is a subspace of the kernel of the linear map associated with $B$ if and only if the range of the linear map associated with $B$ is a subspace of the range of the linear map associated with $A$. That is, $\ker(A) \subseteq \ker(B)$ if and only if $\text{range}(B) \subseteq \text{range}(A)$.

Let $R$ be a type that forms an ordered additive abelian group (specifically, an `AddCommGroup` with a `PartialOrder` such that addition is monotonic). Let $f: \text{Matrix}_{n \times n}(\mathbb{k}) \to R$ be an additive group homomorphism. If $f$ maps every positive semidefinite matrix $A$ to a non-negative element in $R$ (i.e., $A \ge 0 \implies f(A) \ge 0$), then $f$ is monotonic with respect to the Loewner order: for any $n \times n$ matrices $A$ and $B$, if $A \le B$, then $f(A) \le f(B)$.

Let $R$ be an ordered additive abelian group and let $f: R \to \text{Mat}_{n \times n}(\mathbb{k})$ be an additive group homomorphism. Suppose that for every $x \in R$, if $0 \le x$, then the matrix $f(x)$ is positive semidefinite. Then for any $x, y \in R$ such that $x \le y$, it follows that $f(x) \le f(y)$ in the Loewner order (i.e., $f(y) - f(x)$ is positive semidefinite).

Let $A, B \in \text{Mat}_{n \times n}(\mathbb{k})$ be Hermitian matrices and $C \in \text{Mat}_{m \times n}(\mathbb{k})$ be an arbitrary matrix. If $A \le B$ in the Loewner order (meaning $B - A$ is a positive semidefinite matrix), then it holds that $CAC^* \le CBC^*$, where $C^*$ denotes the conjugate transpose of $C$.

Let $A, B \in \text{Mat}_{n \times n}(\mathbb{k})$ be Hermitian matrices and $C \in \text{Mat}_{n \times m}(\mathbb{k})$ be an arbitrary matrix. If $A \le B$ in the Loewner order (meaning $B - A$ is a positive semidefinite matrix), then it holds that $C^* A C \le C^* B C$, where $C^*$ denotes the conjugate transpose of $C$.

Let $A$ be a Hermitian matrix in $\text{Mat}_{n \times n}(\mathbb{k})$ and let $hA$ be the proof of its Hermiticity. The matrix $A$ is positive semidefinite ($0 \le A$) if and only if all of its eigenvalues are non-negative, i.e., $0 \le \lambda_i$ for all $i \in \{1, \dots, n\}$, where $\lambda_i$ denotes the eigenvalues of $A$ provided by $hA$.

Let $\mathbb{k}$ be a field with a partial order (specifically one where matrices can be positive semidefinite, such as $\mathbb{R}$ or $\mathbb{C}$). The diagonal map $\text{diag} : M_n(\mathbb{k}) \to \mathbb{k}^n$, which associates a square matrix $A$ with the vector of its diagonal entries $A_{ii}$, is monotone with respect to the Loewner order on matrices and the entrywise order on vectors. That is, if $A \le B$ in the sense that $B - A$ is a positive semidefinite matrix, then for every index $i$, the diagonal entries satisfy $A_{ii} \le B_{ii}$.

Let $A$ and $B$ be square matrices. If $A \le B$ with respect to the Loewner order (meaning $B - A$ is a positive semidefinite matrix), then for every index $i$, the diagonal entries satisfy $A_{ii} \le B_{ii}$, where $A_{ii}$ and $B_{ii}$ denote the $i$-th elements of the diagonal vectors of $A$ and $B$ respectively.

The trace function $\text{tr}: \text{Mat}_{n \times n}(\mathbb{k}) \to \mathbb{k}$ is monotone with respect to the Loewner order. Specifically, if $A$ and $B$ are square matrices over $\mathbb{k}$ such that $A \le B$ (meaning $B - A$ is positive semidefinite), then $\text{tr}(A) \le \text{tr}(B)$.

Let $A$ and $B$ be positive semidefinite matrices of the same size with entries in a field $\mathbb{k}$. If $A \le B$ with respect to the Loewner order (meaning $B - A$ is positive semidefinite), then the trace of $A$ is less than or equal to the trace of $B$, i.e., $\text{tr}(A) \le \text{tr}(B)$.

The function `diagonal`, which maps a vector $d \in \mathbb{K}^n$ to a diagonal matrix with entries $d$, is monotone. That is, for any vectors $d_1, d_2 \in \mathbb{K}^n$, if $d_1 \le d_2$ component-wise, then the corresponding diagonal matrices satisfy $\text{diag}(d_1) \le \text{diag}(d_2)$ in the Loewner order (i.e., their difference $\text{diag}(d_2) - \text{diag}(d_1)$ is positive semidefinite).

Let $d_1$ and $d_2$ be vectors of length $n$ with entries in a field $\mathbb{k}$. If $d_1 \le d_2$ (entrywise), then the diagonal matrix formed from $d_1$ is less than or equal to the diagonal matrix formed from $d_2$ in the Loewner order (i.e., $\text{diag}(d_2) - \text{diag}(d_1)$ is a positive semidefinite matrix).

For any two vectors $d_1, d_2 \in \mathbb{k}^n$, the inequality $d_1 \leq d_2$ holds component-wise if and only if the corresponding diagonal matrices satisfy the Loewner order partial regulation, denoted by $\text{diag}(d_1) \leq \text{diag}(d_2)$. Here, $\text{diag}(d)$ represents the square matrix with elements of $d$ on the main diagonal and zeros elsewhere, and the inequality between matrices refers to the positive semidefiniteness of their difference.

Let $A \in \text{Mat}_{n \times n}(\mathbb{k})$ be a Hermitian matrix and $c \in \mathbb{R}$ be a scalar. Then all the eigenvalues $\lambda_i$ of $A$ satisfy $\lambda_i \le c$ if and only if $A \le cI$ in the Loewner order, where $I$ is the $n \times n$ identity matrix and $A \le cI$ means that $cI - A$ is a positive semidefinite matrix.

Let $A$ be an $n \times n$ Hermitian matrix over a field $\mathbb{k}$, and let $c$ be a real number. Then $c \le \lambda_i$ for all eigenvalues $\lambda_i$ of $A$ if and only if $c I \le A$ in the Loewner order, where $I$ is the $n \times n$ identity matrix and the inequality $c I \le A$ indicates that $A - c I$ is a positive semidefinite matrix.

Given a matrix $m$ with row indices in $d \times d_1$ and column indices in $d \times d_2$ over a ring $R$, the left partial trace $\text{traceLeft}(m)$ is a matrix in $M_{d_1 \times d_2}(R)$. Each entry of the resulting matrix at position $(i_1, j_1)$ is defined as the sum over the common first index $i_2 \in d$: $$(\text{traceLeft}(m))_{i_1, j_1} = \sum_{i_2 \in d} m_{(i_2, i_1), (i_2, j_1)}$$ This operation corresponds to taking the partial trace over the first subsystem in a tensor product space.

Given a matrix $m$ with row indices in $d_1 \times d$ and column indices in $d_2 \times d$ over a ring $R$, the right partial trace $\text{traceRight}(m)$ is a matrix in $M_{d_1 \times d_2}(R)$. Each entry of the resulting matrix at position $(i_2, j_2)$ is defined as the sum over the common second index $i_1 \in d$: $$(\text{traceRight}(m))_{i_2, j_2} = \sum_{i_1 \in d} m_{(i_2, i_1), (j_2, i_1)}$$ This operation corresponds to taking the partial trace over the second subsystem in a tensor product space.

Let $A$ be a matrix with row and column indices in $d_1 \times d_2$ over a ring $R$. The trace of the left partial trace of $A$ is equal to the trace of $A$: $$\text{tr}(\text{traceLeft}(A)) = \text{tr}(A)$$ where $\text{traceLeft}(A)$ is the partial trace over the first subsystem.

Let $A$ be a matrix with row and column indices in $d_1 \times d_2$ over a ring $R$. The trace of the right partial trace of $A$ is equal to the trace of $A$, i.e., $$\text{tr}(\text{traceRight}(A)) = \text{tr}(A)$$ where $\text{traceRight}(A)$ is the partial trace over the second subsystem.

Let $A$ be a matrix of shape $(d \times d_1) \times (d \times d_1)$ over a ring $R$ with an involution. If $A$ is a Hermitian matrix, then its partial trace over the left subsystem, denoted by $A.\text{traceLeft}$, is also a Hermitian matrix.

Let $A$ be a matrix of shape $(d_1 \times d) \times (d_1 \times d)$ over a ring $R$. If $A$ is a Hermitian matrix, then its partial trace over the right subsystem, denoted by $A.\text{traceRight}$, is also a Hermitian matrix.

Let $R$ be a ring, and let $M \in \text{Mat}_{d_A \times d_B, d_A \times d_B}(R)$ be a block matrix. For any matrix $A \in \text{Mat}_{d_A, d_A}(R)$, the trace of the product of $M$ and the Kronecker product of $A$ with the identity matrix $I_{d_B}$ is equal to the trace of the product of the partial trace of $M$ over the second subsystem and $A$. That is, $\text{Tr}(M(A \otimes I)) = \text{Tr}(\text{Tr}_B(M)A)$, where $\text{Tr}_B$ denotes the partial trace `traceRight`.

Let $R$ be a ring, and let $M$ be a matrix of shape $(d_A \times d_B) \times (d_A \times d_B)$ over $R$. For any matrix $B$ of shape $d_B \times d_B$, the trace of the product of $M$ and the Kronecker product of the identity matrix $I_{d_A}$ and $B$ is equal to the trace of the product of the partial trace of $M$ over the first system and $B$. That is, $$\text{Tr}(M (I_{d_A} \otimes B)) = \text{Tr}(\text{Tr}_A(M) B)$$ where $\text{Tr}_A$ denotes the partial trace over the left subsystem (`traceLeft`).

Let $A$ be a positive semidefinite block matrix in $\text{Mat}_{d \times d_1, d \times d_1}(R)$. Then its partial trace over the first subsystem, denoted by $A.\text{traceLeft} \in \text{Mat}_{d_1, d_1}(R)$, is also positive semidefinite.

Let $A$ be a matrix with row and column indices in $d_1 \times d$ over a field $\mathbb{k}$. If $A$ is positive semidefinite, then its right partial trace $\text{traceRight}(A)$, which is a matrix of size $d_1 \times d_1$ defined by $(\text{traceRight}(A))_{i, j} = \sum_{k \in d} A_{(i, k), (j, k)}$, is also positive semidefinite.

Let $d_1$ and $d_2$ be finite types with decidable equality, and let $\mathbb{k}$ be a field with a structure of a conjugate-closed field (such as $\mathbb{R}$ or $\mathbb{C}$). For any two square matrices $A \in \text{Mat}_{d_1 \times d_1}(\mathbb{k})$ and $B \in \text{Mat}_{d_2 \times d_2}(\mathbb{k})$, if $A$ is positive definite and $B$ is positive definite, then their Kronecker product $A \otimes_k B$ is also positive definite.

Let $\mathbb{k}$ be a field which is either the real numbers $\mathbb{R}$ or the complex numbers $\mathbb{C}$. Let $d_1$ and $d_2$ be finite types. Let $M \in \text{Matrix}(d_1, d_1, \mathbb{k})$ be a square matrix. If $M$ is positive definite and $e : d_2 \to d_1$ is an injective function, then the submatrix $(M_{e(i), e(j)})_{i, j \in d_2}$ is also positive definite.

Let $\mathbb{k}$ be a field which is either the real numbers $\mathbb{R}$ or the complex numbers $\mathbb{C}$. Let $d_1$ and $d_2$ be finite types with decidable equality. For any square matrix $M \in \text{Matrix}(d_1, d_1, \mathbb{k})$ and any equivalence (bijection) $e : d_1 \simeq d_2$, if $M$ is positive definite, then the reindexed matrix $(M \circ (e^{-1} \times e^{-1})) \in \text{Matrix}(d_2, d_2, \mathbb{k})$ is also positive definite.

Let $\mathbb{k}$ be a field which is either the real numbers $\mathbb{R}$ or the complex numbers $\mathbb{C}$. Let $d_1$ and $d_2$ be finite types. For any square matrix $M \in \text{Matrix}(d_1, d_1, \mathbb{k})$ and any equivalence (bijection) $e : d_1 \simeq d_2$, the matrix $M$ is positive definite if and only if the reindexed matrix $(M \circ (e^{-1} \times e^{-1})) \in \text{Matrix}(d_2, d_2, \mathbb{k})$ is positive definite.

Let $M$ be a complex matrix of size $n \times n$ indexed by a finite type. If $M$ is positive semidefinite ($M \succeq 0$) and $c$ is a non-negative real number ($c \ge 0$), then the scalar product $cM$ is also positive semidefinite.

Let $\mathbb{k}$ be either the real numbers $\mathbb{R}$ or the complex numbers $\mathbb{C}$, and let $n$ be a finite indexing type. The set of positive definite square matrices of size $n \times n$ over $\mathbb{k}$ is a convex set over the real numbers. That is, for any two positive definite matrices $M_1, M_2$ and any $t \in [0, 1]$, the linear combination $(1 - t)M_1 + tM_2$ is also positive definite.

Let $M$ be a square matrix of size $d \times d$ over a field $\mathbb{k}$ (where $\mathbb{k}$ is either $\mathbb{R}$ or $\mathbb{C}$). $M$ is positive definite ($M \succ 0$) if and only if $M$ is Hermitian and all of its eigenvalues are strictly positive.

Let $M$ be a Hermitian matrix in $\text{Mat}_{d \times d}(\mathbf{k})$, where $\mathbf{k}$ is a conjugate-reals-like field (such as $\mathbb{R}$ or $\mathbb{C}$), and let $f: \mathbb{R} \to \mathbb{R}$ be a function. Let $f(M)$ denote the matrix obtained by applying the continuous functional calculus to $M$ with respect to $f$. Then there exists a permutation $\sigma$ of the indices $d$ such that the eigenvalues of $f(M)$ are given by the composition $f \circ \lambda \circ \sigma$, where $\lambda$ represents the eigenvalues of $M$. In other words, the set of eigenvalues of $f(M)$ is $\{f(\lambda_i) \mid i \in d\}$.

Let $d$ be a finite index set and $\mathbb{k}$ be a field $(\mathbb{R}$ or $\mathbb{C})$. Let $A$ be a Hermitian $d \times d$ matrix over $\mathbb{k}$. If there exists a unitary matrix $U$ and a diagonal matrix $D = \text{diag}(f_i)$ with real entries $f: d \to \mathbb{R}$ such that $A$ is unitarily similar to $D$, i.e., $$A = U \text{diag}(f_i) U^*$$ then there exists a permutation $\sigma$ of the index set $d$ such that the eigenvalues of $A$ are given by the entries of $f$ permuted by $\sigma$, specifically: $$\text{eigenvalues}(A) \circ \sigma = f$$

Let $I$ be the $n \times n$ identity matrix over a ring $\alpha$. Then the linear map associated with $I$ acting on the Euclidean space $\alpha^n$, denoted by $\text{Matrix.toEuclideanLin}(I)$, is the identity linear operator $\text{id}$.

Let $d$ be a finite index set and $\mathbf{k}$ be either $\mathbb{R}$ or $\mathbb{C}$. Given a function $g: d \to \mathbb{R}$ and a real-valued function $f: \mathbb{R} \to \mathbb{R}$, let $D = \text{diag}(g(x))$ be the diagonal matrix whose entries are the values of $g$ cast into $\mathbf{k}$. Then the continuous functional calculus (cfc) of $f$ applied to $D$ is equal to the diagonal matrix whose entries are the values of $(f \circ g)$, specifically: $$\text{cfc}(f, \text{diag}(g(x))) = \text{diag}(f(g(x)))$$

Let $A$ be a $d \times d$ matrix over a field $\mathbb{K}$ (where $\mathbb{K}$ is $\mathbb{R}$ or $\mathbb{C}$). If $A$ is a positive semidefinite matrix, then every element $r$ in the spectrum of $A$—that is, every eigenvalue $r \in \mathbb{R}$—satisfies $r \ge 0$.

Let $A$ be a $d \times d$ positive semidefinite matrix over $\mathbb{K}$ (where $\mathbb{K}$ is either $\mathbb{R}$ or $\mathbb{C}$). For any real numbers $x$ and $y$ such that their sum is non-zero ($x + y \neq 0$), the continuous functional calculus of the power function $r \mapsto r^{x+y}$ applied to $A$ is equal to the continuous functional calculus of the product of power functions $r \mapsto r^x \cdot r^y$ applied to $A$. That is, $$\text{cfc}(r \mapsto r^{x+y}, A) = \text{cfc}(r \mapsto r^x \cdot r^y, A)$$

Let $A$ be a positive semidefinite $d \times d$ matrix over a field $\mathbb{K}$ (where $\mathbb{K}$ is $\mathbb{R}$ or $\mathbb{C}$). For any real numbers $x$ and $y$, the matrix constructed via the continuous functional calculus (cfc) using the function $f(r) = r^{xy}$ is equal to the matrix constructed using the function $g(r) = (r^x)^y$. That is, $$\text{cfc}(r \mapsto r^{xy}, A) = \text{cfc}(r \mapsto (r^x)^y, A)$$