Entropy and asymptotics / Definition

Conditional mutual information definition

Definition statement

For a quantum state $\rho$ on a tripartite system $ABC$, the conditional mutual information between $A$ and $C$ given $B$ is defined as $I(A : C \mid B)_\rho := H(AB)_\rho + H(BC)_\rho - H(B)_\rho - H(ABC)_\rho$.

Sources

  1. Universal recovery map for approximate Markov chains

    David Sutter, Omar Fawzi, Renato Renner, 2015

Lean context

Lean declaration
QIT.State.condMutualInfo

Copy a short prompt with the import, Lean declaration, citations, and public source link.

Open Lean source