Conditional mutual information (Definition 10.6.1)
DefinitionWildeQIT_condMutualInfoDefinition 10.6.1 (Conditional mutual information). Let , , and be discrete random variables with joint distribution . The conditional mutual information is
where is the conditional entropy (Definition 10.2.1) of given computed from the marginal , and is the conditional entropy of given the pair computed from regrouped as the pair distribution of . (Wilde also records the equivalent forms and .) Logarithms are base .
The conditional mutual information measures the correlation between and that remains once is known; its non-negativity is the strong subadditivity of classical entropy (Theorem 10.6.1), and it drives the chain rule for mutual information and the data-processing inequality.
Formalization Note. WildeQIT.condMutualInfo p, for p : WildeQIT.FinDist (α × β × γ) (components in this order; note α × β × γ is α × (β × γ)), is condEntropy p.margYZ - condEntropy p.groupY_XZ, where margYZ is the marginal and groupY_XZ presents as the pair distribution of , so that condEntropy (first component given second) yields and respectively. The definition uses the first of Wilde's three displayed forms; the other two are theorems.
import Definitions.Def_WildeQIT_condEntropy
/-!
Wilde, *Quantum Information Theory* (2nd ed.), Definition 10.6.1 (Conditional mutual
information): for discrete random variables `X, Y, Z`, `I(X;Y|Z) ≡ H(Y|Z) - H(Y|X,Z)`.
-/
namespace WildeQIT
/-- Definition 10.6.1. The conditional mutual information of a triple with joint distribution
`p` on `α × β × γ` (components `X, Y, Z`): `I(X;Y|Z) = H(Y|Z) - H(Y|X,Z)`, where `H(Y|Z)` is
the conditional entropy of the marginal pair `(Y,Z)` and `H(Y|X,Z)` is the conditional entropy
of `Y` given the pair `(X,Z)`. -/
noncomputable def condMutualInfo {α β γ : Type} [Fintype α] [Fintype β] [Fintype γ]
(p : FinDist (α × β × γ)) : ℝ :=
condEntropy p.margYZ - condEntropy p.groupY_XZ
end WildeQIT