QuantumInfo.Finite.Entropy.SSA

For a matrix $A \in M_{m \times n}(\mathbf{k})$ over a field $\mathbf{k}$ (where $\mathbf{k}$ is $\mathbb{R}$ or $\mathbb{C}$), let $L_A: \ell_2^n \to \ell_2^m$ be the associated linear map between Euclidean spaces. The operator norm $\|A\|_{\text{op}}$ is defined as the operator norm of $L_A$ viewed as a continuous linear map, which is given by $\|A\|_{\text{op}} = \sup_{\|x\|_2 \le 1} \|Ax\|_2$.

Let $A$ be an $n \times m$ matrix over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$). If $A$ is an isometry, then for any vector $x$ in the $m$-dimensional Euclidean space $\mathbb{k}^m$, the norm of the image of $x$ under the linear map defined by $A$ is equal to the norm of $x$, i.e., $\|Ax\| = \|x\|$.

Let $A$ be a matrix of size $n \times m$ over the field $\mathbb{K}$ (where $\mathbb{K}$ is $\mathbb{R}$ or $\mathbb{C}$), and suppose the column dimension $m$ is non-empty. If $A$ is an isometry, then its operator norm $\|A\|_{\text{op}}$ is equal to $1$.

Let $d_1$ and $d_2$ be dimensions. The matrix $M \in \mathbb{C}^{((d_1 \times d_2) \times d_2) \times d_1}$ is defined such that its entries are given by $$M_{((i, j), k), l} = \begin{cases} 1 & \text{if } i = l \text{ and } j = k \\ 0 & \text{otherwise} \end{cases}$$ for indices $i, l \in \{1, \dots, d_1\}$ and $j, k \in \{1, \dots, d_2\}$. This matrix represents the linear map $v \mapsto v \otimes \sum_k |k\rangle|k\rangle$, which maps a vector in $\mathbb{C}^{d_1}$ to a tensor product of itself and a maximally entangled state (MES) basis sum in $\mathbb{C}^{d_2} \otimes \mathbb{C}^{d_2}$.

Let $A$ be a complex matrix of size $(d_1 \times d_2) \times (d_1 \times d_2)$. Let $M$ be the matrix `map_to_tensor_MES` of size $((d_1 \times d_2) \times d_2) \times d_1$. Then the product $M^* (A \otimes I_{d_2}) M$ is equal to the partial trace of $A$ over the second system, denoted as $\text{Tr}_2(A)$, where $M^*$ denotes the conjugate transpose and $I_{d_2}$ is the $d_2 \times d_2$ identity matrix.

Let $\rho_{AB}$ be a Hermitian matrix acting on the Hilbert space $\mathcal{H}_A \otimes \mathcal{H}_B$, where $d_A$ and $d_B$ denote the dimensions of the respective subspaces. The isometry $V_{\rho}$ is the matrix in $\mathbb{C}^{(d_A \times d_B) \times d_B, d_A}$ defined by $$V_{\rho} = (\sqrt{\rho_{AB}} \otimes I_B) \cdot M \cdot \sqrt{\rho_A^{-1}}$$ where: - $\rho_A = \text{Tr}_B(\rho_{AB})$ is the partial trace of $\rho_{AB}$ over the system $B$. - $\sqrt{\rho_A^{-1}}$ is the principal square root of the inverse of $\rho_A$. - $I_B$ is the identity matrix of size $d_B$. - $\otimes$ denotes the Kronecker product (tensor product). - $M$ is the fixed linear map `map_to_tensor_MES` mapping $d_A \to (d_A \times d_B) \times d_B$ related to the maximally entangled state.

Given a Hermitian matrix $\sigma_{BC}$ acting on the Hilbert space $\mathcal{H}_B \otimes \mathcal{H}_C$, the map $V_\sigma$ is an operator (represented as a matrix) from $\mathcal{H}_C$ to $\mathcal{H}_B \otimes (\mathcal{H}_B \otimes \mathcal{H}_C)$. It is defined by applying the construction $V_\rho$ to the permuted matrix $\sigma_{CB}$ and reindexing the resulting components to match the tensor product structure $dB \times (dB \times dC)$. This isometry is a key component in the proofs of quantum relative entropy inequalities, specifically for establishing strong subadditivity (SSA).

Let $\rho_{AB}$ be a positive definite Hermitian matrix on the tensor product space $\mathbb{C}^{d_A} \otimes \mathbb{C}^{d_B}$. Let $\rho_A = \text{Tr}_B(\rho_{AB})$ be the partial trace of $\rho_{AB}$ over the system $B$, and let $\rho_A^{-1/2}$ denote the square root of the inverse of $\rho_A$. Then the product of the adjoint of the isometry-like matrix $V_\rho(\rho_{AB})$ with itself satisfies $V_\rho(\rho_{AB})^\dagger V_\rho(\rho_{AB}) = \rho_A^{-1/2} \text{Tr}_B(\rho_{AB}) \rho_A^{-1/2}$.

Let $A$ be a positive definite Hermitian matrix acting on the tensor product space $\mathbb{C}^{d_A} \otimes \mathbb{C}^{d_B}$, where the dimension $d_B$ is non-zero. Then its partial trace over the right system $B$, denoted as $\text{Tr}_B(A)$, is also a positive definite matrix.

Let $A$ be a Hermitian matrix acting on the tensor product space $\mathbb{C}^{d_A} \otimes \mathbb{C}^{d_B}$. If the dimension $d_A$ is non-zero (i.e., the type $d_A$ is `Nonempty`) and $A$ is positive definite ($A \succ 0$), then its partial trace over the first subsystem, denoted by $\text{Tr}_A(A)$, is also a positive definite matrix.

Let $\rho_{AB}$ be a positive definite Hermitian matrix acting on the bipartite Hilbert space $\mathcal{H}_A \otimes \mathcal{H}_B$, where the dimension of system $B$ is non-zero ($d_B > 0$). Let $V_{\rho}$ be the isometry operator associated with $\rho_{AB}$. Then, the product of the conjugate transpose of $V_{\rho}$ and itself is the identity matrix, i.e., $(V_{\rho})^\dagger V_{\rho} = I$.

Let $\mathcal{H}_B$ and $\mathcal{H}_C$ be finite-dimensional Hilbert spaces with dimensions $d_B$ and $d_C$ respectively, such that $d_B > 0$. For any positive definite Hermitian matrix $\sigma_{BC}$ acting on $\mathcal{H}_B \otimes \mathcal{H}_C$, the matrix $V_{\sigma}$ satisfies the isometry condition $(V_{\sigma})^\dagger V_{\sigma} = \mathbb{I}$, where $(V_{\sigma})^\dagger$ denotes the conjugate transpose and $\mathbb{I}$ is the identity matrix on $\mathcal{H}_C$.

Given two Hermitian matrices $\rho_{AB}$ acting on the Hilbert space $\mathcal{H}_A \otimes \mathcal{H}_B$ and $\sigma_{BC}$ acting on $\mathcal{H}_B \otimes \mathcal{H}_C$, the operator $W$ is defined as the square matrix of size $(d_A \times d_B \times d_C)$ given by the product: $$W = (\sqrt{\rho_{AB}} \otimes \sqrt{\sigma_{C}^{-1}}) \cdot (\sqrt{\rho_{A}^{-1}} \otimes \sqrt{\sigma_{BC}})$$ where: - $\rho_A = \text{Tr}_B(\rho_{AB})$ is the partial trace of $\rho_{AB}$ over system $B$. - $\sigma_C = \text{Tr}_B(\sigma_{BC})$ is the partial trace of $\sigma_{BC}$ over system $B$. - $\sqrt{\cdot}$ and $(\cdot)^{-1}$ denote the principal matrix square root and matrix inverse respectively. - The second term is reindexed to ensure compatibility with the tensor product structure of the first term on the composite space $\mathcal{H}_A \otimes \mathcal{H}_B \otimes \mathcal{H}_C$.

Let $A$ be an $l \times m$ matrix and $B$ be an $m \times n$ matrix over a field $\mathbb{K}$ (where $\mathbb{K}$ is either $\mathbb{R}$ or $\mathbb{C}$). The operator norm $\| \cdot \|_{\text{op}}$ satisfies the submultiplicative property: $$\|A \cdot B\|_{\text{op}} \le \|A\|_{\text{op}} \cdot \|B\|_{\text{op}}$$ where the operator norm is the induced norm from the Euclidean space.

Let $A$ be an $m \times n$ matrix over a field $\mathbb{K}$ (where $\mathbb{K}$ is $\mathbb{R}$ or $\mathbb{C}$). Given bijections (equivalences) $e: m \simeq l$ and $f: n \simeq p$, let $A'$ be the $l \times p$ matrix obtained by reindexing the rows and columns of $A$ according to $e$ and $f$ respectively. Then the operator norm of the reindexed matrix is equal to the operator norm of the original matrix, i.e., $\|A'\|_{\text{op}} = \|A\|_{\text{op}}$.

Let $\rho_{AB}$ be a Hermitian matrix acting on the Hilbert space $\mathcal{H}_A \otimes \mathcal{H}_B$ with dimensions $d_A \times d_B$. We define the operator $U_\rho$ as the Kronecker product (tensor product) of the matrix $V_\rho$ and the identity matrix $I_{d_C}$ of dimension $d_C \times d_C$: $$U_\rho = V_\rho \otimes I_{d_C}$$ where $V_\rho$ is a matrix of size $((d_A \times d_B) \times d_B) \times d_A$. The resulting matrix $U_\rho$ maps from the space of dimension $d_A \times d_C$ to the space of dimension $(d_A \times d_B \times d_B) \times d_C$.

Given a Hermitian matrix $\sigma_{BC}$ acting on the Hilbert space $\mathbb{C}^{d_B} \otimes \mathbb{C}^{d_C}$, we define the matrix $U_\sigma$ as the Kronecker product of the identity matrix $I_A$ (of dimension $d_A \times d_A$) and the matrix $V_\sigma(\sigma_{BC})$. Specifically, $U_\sigma = I_A \otimes V_\sigma$, resulting in a matrix of size $(d_A \cdot d_B \cdot d_B \cdot d_C) \times (d_A \cdot d_C)$. This construction serves as a helper operator for proving Strong Subadditivity (SSA) and operator inequalities in quantum information theory.

Let $A$ be an $m \times n$ matrix over a field $\mathbb{k}$ (where $\mathbb{k}$ is $\mathbb{R}$ or $\mathbb{C}$). The operator norm of the conjugate transpose of $A$, denoted as $\|A^{H}\|$, is equal to the operator norm of $A$, denoted as $\|A\|$.

Let $V$ be an $m \times n$ matrix over the complex numbers $\mathbb{C}$. If $V$ is an isometry, such that $V^\dagger V = I$ (where $V^\dagger$ denotes the conjugate transpose and $I$ is the identity matrix), then $V V^\dagger \le I$ in terms of the Loewner partial order (i.e., $I - V V^\dagger$ is a positive semi-definite matrix).

Let $A$ be a $k \times m$ complex matrix and $B$ be a $k \times n$ complex matrix. If both $A$ and $B$ are isometries (meaning $A^\dagger A = I_m$ and $B^\dagger B = I_n$, where $\dagger$ denotes the conjugate transpose), then the product of the conjugate transpose of $A^\dagger B$ with itself satisfies $(A^\dagger B)^\dagger (A^\dagger B) \le I_n$ in the sense of the Loewner partial order on positive semidefinite matrices.

Let $d$ and $d_2$ be finite types. For any equivalence $e : d \simeq d_2$ and any Hermitian matrices $A, B \in \text{HermitianMat}(d, \mathbb{C})$, the inequality $A.reindex(e) \le B.reindex(e)$ holds if and only if $A \le B$, where the inequality denotes the Loewner order (positivity of the difference) and the reindexing is the transformation of matrices under the coordinate change provided by $e$.

Let $A$ be a non-singular Hermitian matrix of size $m \times m$ and $B$ be a non-singular Hermitian matrix of size $n \times n$ over the complex numbers $\mathbb{C}$. The inverse of their Kronecker product is equal to the Kronecker product of their inverses, i.e., $(A \otimes B)^{-1} = A^{-1} \otimes B^{-1}$.

Let $A$ be a Hermitian matrix with complex entries indexed by a finite set $d$, and let $e: d \simeq d_2$ be a bijection to another finite index set $d_2$. The inverse of the reindexed matrix $A$ is equal to the reindexing of the inverse matrix $A^{-1}$ using the same bijection $e$. That is, $(A.reindex \ e)^{-1} = A^{-1}.reindex \ e$.

Let $A$ be a Hermitian matrix of size $m \times m$ and $B$ be a Hermitian matrix of size $n \times n$ over the complex numbers $\mathbb{C}$. If $A$ is positive definite and $B$ is positive definite, then their Kronecker product $A \otimes B$ is also positive definite.

Let $A$ be a Hermitian matrix of size $d \times d$ over the complex numbers $\mathbb{C}$. If $A$ is positive definite ($A \succ 0$) and $e: d \simeq d_2$ is an equivalence (reindexing) between the index sets $d$ and $d_2$, then the reindexed matrix $A'$ (where $A'_{i,j} = A_{e^{-1}(i), e^{-1}(j)}$) is also positive definite.

Given three types $d_A, d_B,$ and $d_C$, the type $\text{BigIdx}$ is defined as the product type $((d_A \times d_B) \times d_B) \times (d_B \times d_C)$. This structure represents a specific indexing set used in the context of quantum relative entropy and operator inequalities, notably for proving Strong Subadditivity (SSA).

Given three types $d_A, d_B,$ and $d_C$, which typically serve as the index sets for Hilbert spaces $\mathcal{H}_A, \mathcal{H}_B,$ and $\mathcal{H}_C$ in a tripartite quantum system, the type $\text{SmallIdx}$ is defined as the Cartesian product $(d_A \times d_B) \times d_C$. This structure represents the index set for the composite system $\mathcal{H}_A \otimes \mathcal{H}_B \otimes \mathcal{H}_C$.

Given three types $d_A, d_B,$ and $d_C$ (typically representing the dimensions or index sets of Hilbert spaces $\mathcal{H}_A, \mathcal{H}_B,$ and $\mathcal{H}_C$), the type $\text{MidIdx}$ is defined as the nested product type $(d_A \times d_B) \times (d_B \times (d_B \times d_C))$. This index set serves as an intermediate structure for defining linear operators and proving operator inequalities such as Strong Subadditivity (SSA) in quantum information theory.

[Nonempty dA] [Nonempty dB] [Nonempty dC] (ρAB : HermitianMat (dA × dB) ℂ) (σBC : HermitianMat (dB × dC) ℂ) (hρ : ρAB.mat.PosDef) (hσ : σBC.mat.PosDef) : (W_mat ρAB σBC)ᴴ * (W_mat ρAB σBC) ≤ 1

Let $\mathcal{H}_A, \mathcal{H}_B, \mathcal{H}_C$ be finite-dimensional Hilbert spaces with dimensions $d_A, d_B, d_C$. Let $\rho_{AB}$ be a positive definite Hermitian matrix on $\mathcal{H}_A \otimes \mathcal{H}_B$ and $\sigma_{BC}$ be a positive definite Hermitian matrix on $\mathcal{H}_B \otimes \mathcal{H}_C$. Let $\rho_A = \text{Tr}_B(\rho_{AB})$ and $\sigma_C = \text{Tr}_B(\sigma_{BC})$ denote the respective partial traces. Then the following operator inequality holds on $\mathcal{H}_A \otimes \mathcal{H}_B \otimes \mathcal{H}_C$: $$\rho_{AB} \otimes \sigma_C^{-1} \le \text{reindex}(\rho_A \otimes \sigma_{BC}^{-1})$$ where the reindexing is performed using the inverse associativity equivalence $(A \times B) \times C \simeq A \times (B \times C)$.

Let $\rho_{AB}$ be a positive definite Hermitian matrix on the Hilbert space $\mathcal{H}_A \otimes \mathcal{H}_B$ and $\sigma_{BC}$ be a positive definite Hermitian matrix on $\mathcal{H}_B \otimes \mathcal{H}_C$. Let $\rho_A = \text{Tr}_B(\rho_{AB})$ and $\sigma_C = \text{Tr}_B(\sigma_{BC})$ denote the respective partial traces. Then the following operator inequality holds: $$\rho_A^{-1} \otimes \sigma_{BC} \le \rho_{AB}^{-1} \otimes \sigma_C$$ where the right-hand side is reindexed via the associator $(d_A \times d_B) \times d_C \simeq d_A \times (d_B \times d_C)$ to match the dimensions of the left-hand side.

For a tripartite quantum mixed state $\rho$ defined on a system with dimensions $d_1 \times d_2 \times d_3$, the von Neumann entropies $S_{vN}$ of its various partial traces satisfy the weak monotonicity inequality: $$S_{vN}(\text{Tr}_{23}(\rho)) + S_{vN}(\text{Tr}_{12}(\rho)) \le S_{vN}(\text{Tr}_3(\rho)) + S_{vN}(\text{Tr}_1(\rho))$$ where $\text{Tr}_{23}(\rho)$ is the partial trace over the second and third subsystems (represented by `ρ.traceRight`), $\text{Tr}_{12}(\rho)$ is the partial trace over the first and second subsystems (represented by `ρ.traceLeft.traceLeft`), $S_{vN}(\text{Tr}_3(\rho))$ corresponds to the entropy of the state on the first two subsystems (represented by `ρ.assoc'.traceRight`), and $S_{vN}(\text{Tr}_1(\rho))$ corresponds to the entropy of the state on the last two subsystems (represented by `ρ.traceLeft`).

For a quantum mixed state $\rho_{123}$ on a tripartite system with state space $d_1 \times d_2 \times d_3$, let $\rho_{12} = \text{Tr}_3(\text{assoc}'(\rho_{123}))$ be the reduced state on the first two subsystems, $\rho_{23} = \text{Tr}_1(\rho_{123})$ be the reduced state on the last two subsystems, and $\rho_2 = \text{Tr}_1(\text{Tr}_3(\rho_{123}))$ be the reduced state on the middle subsystem. Then the von Neumann entropy $S_{vn}$ satisfies the strong subadditivity inequality: $$S_{vn}(\rho_{123}) + S_{vn}(\rho_2) \leq S_{vn}(\rho_{12}) + S_{vn}(\rho_{23})$$

For any quantum mixed state $\rho$ on a composite system with dimensions $d_1 \times d_2$, let $\rho_1 = \text{Tr}_2(\rho)$ be the reduced state on the first subsystem and $\rho_2 = \text{Tr}_1(\rho)$ be the reduced state on the second subsystem. Then the von Neumann entropy $S_{vn}$ of the composite state is less than or equal to the sum of the von Neumann entropies of its reduced states: $$S_{vn}(\rho) \le S_{vn}(\rho_1) + S_{vn}(\rho_2)$$

Let $|\psi\rangle$ be a pure state vector in a tripartite Hilbert space indexed by $(d_1 \times d_2) \times d_3$, and let $\rho = |\psi\rangle\langle\psi|$ be the corresponding density matrix. Let $S(\cdot)$ denote the von Neumann entropy $S_{vn}$. The von Neumann entropy of the reduced state of the first subsystem $d_1$ is bounded by the sum of the entropies of the second and third subsystems, $d_2$ and $d_3$. Specifically, $$S(\text{Tr}_{23}(\rho)) \le S(\text{Tr}_{13}(\rho)) + S(\text{Tr}_{12}(\rho))$$ where $\text{Tr}_{ij}$ denotes the partial trace over the $i$-th and $j$-th subsystems.

Let $\rho$ be a quantum mixed state on a bipartite system with dimensions $d_1 \times d_2$. Let $S_{vn}(\cdot)$ denotes the von Neumann entropy. Let $\rho_1 = \text{Tr}_2(\rho)$ be the reduced density matrix of the first subsystem (obtained by `traceRight`) and $\rho_2 = \text{Tr}_1(\rho)$ be the reduced density matrix of the second subsystem (obtained by `traceLeft`). Then the following inequality holds: $$S_{vn}(\rho_1) \le S_{vn}(\rho_2) + S_{vn}(\rho)$$ This inequality represents one direction of the Araki-Lieb triangle inequality.

Let $\rho$ be a quantum mixed state on a bipartite composite system $d_1 \times d_2$. Let $S_{vN}$ denote the von Neumann entropy. Let $\rho_1 = \text{Tr}_2(\rho)$ be the reduced mixed state obtained by taking the partial trace over the second subsystem, and $\rho_2 = \text{Tr}_1(\rho)$ be the reduced mixed state obtained by taking the partial trace over the first subsystem. Then the following triangle inequality (also known as the Araki-Lieb inequality) holds: $$|S_{vN}(\rho_1) - S_{vN}(\rho_2)| \leq S_{vN}(\rho)$$

Let $\rho$ be a tripartite quantum mixed state on the system $A \otimes (B \otimes C)$. Let $\rho_{AB}$ be the reduced state on $A \otimes B$ obtained by reassociating and tracing out $C$, and let $\rho_{AC}$ be the reduced state on $A \otimes C$ obtained by swapping $A$ and $B$, reassociating, tracing out $B$, and swapping the remaining components. Then the sum of the quantum conditional entropies $S(A|B)$ and $S(A|C)$ is non-negative: $$0 \leq S(A|B)_{\rho_{AB}} + S(A|C)_{\rho_{AC}}$$

For any quantum mixed state $\rho_{123}$ on a tripartite system $d_1 \times d_2 \times d_3$, the conditional entropy of the system satisfies $H(1|23) \leq H(1|2)$, where $H(1|23)$ is the quantum conditional entropy $S(123) - S(23)$ and $H(1|2)$ is the quantum conditional entropy of the reduced state $\rho_{12}$ obtained by taking the partial trace over the third subsystem.

Let $\rho_{123}$ be a quantum mixed state on a tripartite system with dimensions $d_1 \times (d_2 \times d_3)$. Let $I(A;B)$ denote the quantum mutual information of a bipartite state $\rho_{AB}$. If we define the reduced state $\rho_{12}$ as the partial trace over the third subsystem of the reassociated state, i.e., $\rho_{12} = \text{Tr}_3(\text{assoc}'(\rho_{123}))$, then the quantum mutual information of the system satisfies the strong subadditivity inequality: $$I(d_1; d_2 \times d_3)_{\rho_{123}} \geq I(d_1; d_2)_{\rho_{12}}.$$

For any quantum mixed state $\rho$ on a tripartite system with dimensions $d_A \times d_B \times d_C$, the quantum conditional mutual information $I(A:C|B)_\rho$ is non-negative, i.e., $0 \le I(A:C|B)_\rho$.

For any tripartite quantum mixed state $\rho$ defined on a system with dimensions $d_A \times d_B \times d_C$, the quantum conditional mutual information $I(A:C|B)_\rho$ is bounded above by twice the logarithm of the dimension of the first subsystem $A$. That is, $$I(A:C|B)_\rho \le 2 \log |d_A|$$ where $|d_A|$ denotes the cardinality (dimension) of the type $d_A$.

Let $\rho$ be a quantum mixed state on a tripartite system $A \otimes B \otimes C$ with dimensions $d_A, d_B,$ and $d_C$. The quantum conditional mutual information $I(A:C|B)_\rho$, denoted as `qcmi ρ`, satisfies the inequality $$I(A:C|B)_\rho \le 2 \log d_C$$ where $d_C$ is the dimension of the subsystem $C$ (represented by `Fintype.card dC`).