Finite quantum mutual, conditional, and conditional mutual information

For a finite bipartite state ${\rho }_{AB}$ on the ordered product $H_A\otimes H_B$, write ${\rho }_A={\mathrm{Tr}}_B{\rho }_{AB}$ and ${\rho }_B={\mathrm{Tr}}_A{\rho }_{AB}$, using the partial traces in Partial trace over a finite tensor factor and Partial trace over the first tensor factor. They are states by Partial traces of a finite bipartite state are states. Define

$S(A{)}_{\rho }:=S({\rho }_A),S(A\mid B{)}_{\rho }:=S({\rho }_{AB})-S({\rho }_B),I(A:B{)}_{\rho }:=S({\rho }_A)+S({\rho }_B)-S({\rho }_{AB})\mathrm{.}$

For a finite tripartite state ${\rho }_{ABC}$ on the ordered product $H_A\otimes H_B\otimes H_C$, set ${\rho }_{AB}:={\mathrm{Tr}}_{H_C}{\rho }_{ABC}$ after identifying the factors as $(H_A\otimes H_B)\otimes H_C$, and ${\rho }_{BC}:={\mathrm{Tr}}_{H_A}{\rho }_{ABC}$ after identifying them as $H_A\otimes (H_B\otimes H_C)$. Let $P:H_A\otimes H_B\otimes H_C\to H_A\otimes H_C\otimes H_B$ be the wire permutation taking factor order $A,B,C$ to $A,C,B$ (Ordered tensor registers, their inner product, and wire permutations, Finite wire permutations are unitary basis permutations) whose unique adjoint $P^{\ast }$ exists by Every linear map between finite-dimensional inner product spaces has a unique adjoint, and set ${\rho }_{AC}:={\mathrm{Tr}}_{H_B}(P{\rho }_{ABC}{P}^{\ast })$, tracing out the last factor. Because $P$ is unitary, $P{\rho }_{ABC}{P}^{\ast }$ is a state: unitary conjugation preserves non-negativity by the adjoint identity (The adjoint $T^{\ast }:W\to V$ is characterised by $⟨Tv,w{⟩}_W=⟨v,T^{\ast }w{⟩}_V$, Non-negative and positive operators) and preserves trace by cyclicity (For $A\in M_{m\times n}(F)$ and $B\in M_{n\times m}(F)$, $\mathrm{tr}(AB)=\mathrm{tr}(BA)$). Finally set ${\rho }_C:={\mathrm{Tr}}_{H_B}{\rho }_{BC}$. All these marginals are density operators by applying Partial traces of a finite bipartite state are states after grouping factors. Define

$I(A:B\mid C{)}_{\rho }:=S({\rho }_{AC})+S({\rho }_{BC})-S({\rho }_C)-S({\rho }_{ABC})\mathrm{.}$

These are finite-dimensional definitions only; no non-negativity of conditional entropy or conditional mutual information is part of the notation.