Markov Chains

Turn a Markov hypothesis into a machine-checked information inequality. LeanInfoTheory exposes the familiar chain X → Y → Z through IsMarkovChainOf p X Y Z.

Information cannot increase along a Markov chain

The following complete example proves I(X;Z) ≤ I(X;Y). Only the variable alphabets are assumed finite; the source type Omega is not.

import LeanInfoTheory.Shannon.SemanticBridge.Markov

open LeanInfoTheory.Shannon

example {Omega A B C : Type}
    [Fintype A] [Fintype B] [Fintype C]
    (p : PMF Omega) (X : Omega -> A)
    (Y : Omega -> B) (Z : Omega -> C)
    (h : IsMarkovChainOf p X Y Z) :
    mutualInfoOf p X Z <= mutualInfoOf p X Y := by
  exact mutualInfoOf_dataProcessing p X Y Z h

The zero conditional-information characterization

The same chain is equivalent to I(X;Z | Y) = 0. Notice the order: Y is the middle variable in the chain, but the final conditioning argument in conditional mutual information.

import LeanInfoTheory.Shannon.SemanticBridge.Markov

open LeanInfoTheory.Shannon

example {Omega A B C : Type}
    [Fintype A] [Fintype B] [Fintype C]
    (p : PMF Omega) (X : Omega -> A)
    (Y : Omega -> B) (Z : Omega -> C)
    (h : IsMarkovChainOf p X Y Z) :
    condMutualInfoOf p X Z Y = 0 := by
  exact (condMutualInfoOf_eq_zero_iff_isMarkovChainOf p X Y Z).mpr h

The equivalence also works in the other direction: its .mp direction recovers the Markov condition from zero conditional mutual information.

Stochastic channels and stronger results

Finite channels are ordinary functions A -> PMF B; an input law p produces the output law p.bind W. The library also provides channel composition, KL contraction, posterior decompositions, and equality and recovery characterizations. These have their own assumptions; start with the module guide and inspect the exact statements.

For this guide's two results, use the versioned Markov reference. The basic mathematical source is Cover and Thomas (1991), Section 2.8, with the information identities of Sections 2.4-2.5.