InformationTheory.Shannon.CondMutualInfo
Conditional mutual information and Markov chains #
Conditional mutual information condMutualInfo and the Markov chain predicate
IsMarkovChain, together with the chain rule and the implication Markov ⇒ condMI = 0.
Main definitions #
condMutualInfo—I(X; Y | Z) := KL(P_Z ⊗ P_{(X,Y)|Z} ‖ P_Z ⊗ (P_{X|Z} × P_{Y|Z})).IsMarkovChain— joint factorization form (γ-form):μ.map (Z, X, Y)equals(μ.map Z) ⊗ₘ (condDistrib X Z μ ×ₖ condDistrib Y Z μ).
Main statements #
mutualInfo_chain_rule—I((Z, X); Y) = I(Z; Y) + I(X; Y | Z).condMutualInfo_comm—I(X; Y | Z) = I(Y; X | Z).condMutualInfo_ne_top— finiteness over finite alphabets.condMutualInfo_eq_zero_of_markov— Markov chain ⇒I(X; Y | Z) = 0.mutualInfo_le_of_markov—I(X; Y) ≤ I(Z; Y)underX → Z → Y.mutualInfo_le_add_condMutualInfo—I(X; Y) ≤ I(X; Z) + I(X; Y | Z).condMutualInfo_map_left_measurableEquiv—I(e ∘ X; Y | Z) = I(X; Y | Z).condMutualInfo_map_middle_measurableEquiv—I(X; e ∘ Y | Z) = I(X; Y | Z).condMutualInfo_map_cond_measurableEquiv—I(X; Y | e ∘ Z) = I(X; Y | Z).isMarkovChain_map_left— post-processing preserves the Markov property.
Implementation notes #
The γ-form definition of IsMarkovChain (joint measure factorization) is chosen over
the β-form (condDistrib equality via prodMkRight) because the β-form requires
[StandardBorelSpace Ω] on the ambient space, whereas the γ-form avoids this constraint.
The two forms are equivalent under standard Borel hypotheses via Mathlib's
condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight.
InformationTheory.Shannon.condMutualInfo
sourceConditional mutual information via KL divergence (compProd form):
I(X; Y | Z) := KL(P_Z ⊗ P_{(X,Y)|Z} ‖ P_Z ⊗ (P_{X|Z} × P_{Y|Z})).
The compProd form is the defining shape because it connects directly to Mathlib's chain
rule (klDiv_compProd_eq_add) and makes condMutualInfo = 0 under a Markov hypothesis
immediate via klDiv_self.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Used by
InformationTheory.Shannon.condMutualInfo_nonneg
sourceConditional mutual information is non-negative (klDiv is ℝ≥0∞-valued).
Used by
InformationTheory.Shannon.condMutualInfo_congr_measure
sourceUsed by
InformationTheory.Shannon.IsMarkovChain
sourceMarkov chain Xs → Zc → Yo (γ-form, joint factorization): the joint distribution
factors through Zc as the product of the conditional marginals.
Chosen over the β-form (condDistrib equality + prodMkRight) to avoid requiring
[StandardBorelSpace Ω] on the ambient space. The two forms are equivalent under
standard Borel hypotheses.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Used by
InformationTheory.Shannon.mutualInfo_chain_rule
sourceChain rule: I((Z, X); Y) = I(Z; Y) + I(X; Y | Z).
Used by
InformationTheory.Shannon.condMutualInfo_comm
sourceSymmetry of conditional mutual information: I(X; Y | Z) = I(Y; X | Z).
Used by
InformationTheory.Shannon.condMutualInfo_ne_top
sourceOver finite alphabets, conditional mutual information is finite.
Used by
InformationTheory.Shannon.condMutualInfo_eq_zero_of_markov
sourceMarkov chain Xs → Zc → Yo (γ-form) implies I(X; Y | Z) = 0.
Used by
InformationTheory.Shannon.mutualInfo_le_of_markov
sourceMarkov chain Xs → Zc → Yo implies I(Xs; Yo) ≤ I(Zc; Yo).
Used by
InformationTheory.Shannon.mutualInfo_le_add_condMutualInfo
sourceUsed by
MeasurableEquiv invariance of condMutualInfo #
For channel coding arguments involving reshaping such as Y^n ↔ Y_i × Y^{≠i}, the
following lemmas establish invariance of condMutualInfo under MeasurableEquiv on
each argument.
InformationTheory.Shannon.condMutualInfo_map_left_measurableEquiv
sourceReshaping the left argument leaves the CMI fixed: I(e ∘ X; Y | Z) = I(X; Y | Z) for any
MeasurableEquiv e : X ≃ᵐ X'.
Used by
InformationTheory.Shannon.condMutualInfo_map_middle_measurableEquiv
sourceReshaping the right (middle) argument leaves the CMI fixed: I(X; e ∘ Y | Z) = I(X; Y | Z)
for e : Y ≃ᵐ Y'.
Follows from condMutualInfo_comm and condMutualInfo_map_left_measurableEquiv.
Used by
InformationTheory.Shannon.condMutualInfo_map_cond_measurableEquiv
sourceReshaping the conditioner leaves the CMI fixed: I(X; Y | e ∘ Z) = I(X; Y | Z) for any
MeasurableEquiv e : Z ≃ᵐ Z'. The conditioner carries the same information after a
measurable-equiv relabel. Companion to condMutualInfo_map_left_measurableEquiv and
condMutualInfo_map_middle_measurableEquiv (the third argument slot).
@audit:ok
Used by
Stability of IsMarkovChain under post-processing #
InformationTheory.Shannon.isMarkovChain_map_left
sourceMarkov chains are stable under post-processing on the left: if Xs → Zc → Yo is a Markov
chain and f : X → X' is measurable, then f ∘ Xs → Zc → Yo is also a Markov chain.