Chow–Liu trees

12 fully proved

Information Theory

StructureDependence forest#✓fully proved

A dependence forest on the variables ι (Chow–Liu 1968): each variable has at most one parent, and rank strictly increases from parent to child, so the parent relation has no cycles.

structure DependenceForest (ι : Type*) where
  /-- The parent `j(i)` of variable `i`, if any. -/
  parent : ι → Option ι
  /-- A rank certifying acyclicity. -/
  rank : ι → ℕ
  /-- A parent has strictly smaller rank than its child. -/
  rank_lt : ∀ i j, parent i = some j → rank j < rank i

Used by 11

Used byChow–Liu product approximation of a joint law · Nonnegativity of the Chow–Liu approximation · Chow–Liu approximation as a probability mass function · Joint law is absolutely continuous w.r.t. its Chow–Liu approximation · Divergence from the Chow–Liu approximation · Chow–Liu identity · Chow–Liu divergence as a Kullback–Leibler divergence · Chow–Liu optimality · Nonnegativity of the Chow–Liu divergence · Chow–Liu approximation sums to one · Mutual-information weight of a dependence forest

Dependence Forest

DefinitionChow–Liu product approximation of a joint law#✓fully proved

Chow–Liu's product approximation P_τ(x) = ∏_i P(x_i | x_{j(i)}) of a joint law p, with the marginal P(x_i) for a parentless i. The conditional P(x_i | x_j) is P(x_i, x_j) / P(x_j); where P(x_j) = 0 the quotient is 0, and such x have P(x) = 0.

noncomputable def approx (τ : DependenceForest ι) (p : PMF (∀ i, α i)) (x : ∀ i, α i) : ℝ :=
  ∏ i, match τ.parent i with
    | none => ((p.map fun y ↦ y i) (x i)).toReal
    | some j => ((p.map fun y ↦ (y i, y j)) (x i, x j)).toReal / ((p.map fun y ↦ y j) (x j)).toReal

Uses 1 · Used by 7

Statement usesDependence forest

Used byNonnegativity of the Chow–Liu approximation · Chow–Liu approximation as a probability mass function · Joint law is absolutely continuous w.r.t. its Chow–Liu approximation · Divergence from the Chow–Liu approximation · Chow–Liu identity · Chow–Liu divergence as a Kullback–Leibler divergence · Chow–Liu approximation sums to one

TheoremNonnegativity of the Chow–Liu approximation#✓fully proved

The approximation is nonnegative.

theorem approx_nonneg (τ : DependenceForest ι) (p : PMF (∀ i, α i)) (x : ∀ i, α i) :
    0 ≤ τ.approx p x

Uses 2 · Used by 2

Statement usesDependence forest · Chow–Liu product approximation of a joint law

Used byChow–Liu approximation as a probability mass function · Chow–Liu divergence as a Kullback–Leibler divergence

TheoremJoint law is absolutely continuous w.r.t. its Chow–Liu approximation#✓fully proved

P ≪ P_τ: the approximation is positive wherever p is.

theorem approx_pos (τ : DependenceForest ι) (p : PMF (∀ i, α i)) {x : ∀ i, α i} (hx : p x ≠ 0) :
    0 < τ.approx p x

Uses 3 · Used by 1

Statement usesDependence forest · Chow–Liu product approximation of a joint law

Proof usesAtom mass is at most the mass of its image, in reals

Used byChow–Liu divergence as a Kullback–Leibler divergence

TheoremChow–Liu approximation sums to one#✓fully proved

The approximation is a probability law: ∑_x P_τ(x) = 1.

theorem sum_approx (τ : DependenceForest ι) (p : PMF (∀ i, α i)) :
    ∑ x, τ.approx p x = 1

Uses 3 · Used by 1

Statement usesDependence forest · Chow–Liu product approximation of a joint law

Proof usesAtom mass is at most the mass of its image

Used byChow–Liu approximation as a probability mass function

DefinitionChow–Liu approximation as a probability mass function#✓fully proved

Chow–Liu's approximation P_τ as a probability mass function.

noncomputable def approxPMF (τ : DependenceForest ι) (p : PMF (∀ i, α i)) : PMF (∀ i, α i) :=
  PMF.ofFintype (fun x ↦ ENNReal.ofReal (τ.approx p x)) (by
    rw [← ENNReal.ofReal_sum_of_nonneg fun x _ ↦ τ.approx_nonneg p x, sum_approx,
      ENNReal.ofReal_one])

Uses 4 · Used by 2

Statement usesDependence forest · Chow–Liu product approximation of a joint law · Nonnegativity of the Chow–Liu approximation · Chow–Liu approximation sums to one

Used byChow–Liu divergence as a Kullback–Leibler divergence · Nonnegativity of the Chow–Liu divergence

DefinitionMutual-information weight of a dependence forest#✓fully proved

The mutual-information weight ∑_i I(X_i; X_{j(i)}) of a dependence forest, in bits.

noncomputable def weight (τ : DependenceForest ι) (p : PMF (∀ i, α i)) : ℝ :=
  ∑ i, match τ.parent i with
    | none => 0
    | some j => finiteMutualInformation (p.map fun y ↦ (y i, y j))

Uses 2 · Used by 2

Statement usesDependence forest · Mutual information of a finite joint law

Used byChow–Liu identity · Chow–Liu optimality

DefinitionDivergence from the Chow–Liu approximation#✓fully proved

The divergence D(P ‖ P_τ) = ∑_x P(x) log₂ (P(x) / P_τ(x)) of P from Chow–Liu's approximation, in bits (divergence_eq_klDiv).

noncomputable def divergence (τ : DependenceForest ι) (p : PMF (∀ i, α i)) : ℝ :=
  ∑ x, (p x).toReal * logb 2 ((p x).toReal / τ.approx p x)

Uses 2 · Used by 4

Statement usesDependence forest · Chow–Liu product approximation of a joint law

Used byChow–Liu identity · Chow–Liu divergence as a Kullback–Leibler divergence · Chow–Liu optimality · Nonnegativity of the Chow–Liu divergence

TheoremChow–Liu divergence as a Kullback–Leibler divergence#✓fully proved

divergence is Mathlib's Kullback–Leibler divergence klDiv of P relative to P_τ, converted to bits; the finite alphabet carries the discrete σ-algebra.

theorem divergence_eq_klDiv (τ : DependenceForest ι) (p : PMF (∀ i, α i)) :
    letI : MeasurableSpace (∀ i, α i) := ⊤
    τ.divergence p = (klDiv p.toMeasure (τ.approxPMF p).toMeasure).toReal / log 2

Uses 7 · Used by 1

Statement usesDependence forest · Chow–Liu approximation as a probability mass function · Divergence from the Chow–Liu approximation

Proof usesChow–Liu product approximation of a joint law · Nonnegativity of the Chow–Liu approximation · Joint law is absolutely continuous w.r.t. its Chow–Liu approximation · Kullback–Leibler divergence of finite probability laws

Used byNonnegativity of the Chow–Liu divergence

TheoremChow–Liu identity#✓fully proved

D(P ‖ P_τ) = ∑_i H(X_i) - H(X) - ∑_i I(X_i; X_{j(i)}).

theorem divergence_eq (τ : DependenceForest ι) (p : PMF (∀ i, α i)) :
    τ.divergence p =
      ∑ i, shannonEntropy (p.map fun y ↦ y i) - shannonEntropy p - τ.weight p

Uses 10 · Used by 1

Statement usesDependence forest · Divergence from the Chow–Liu approximation · Mutual-information weight of a dependence forest · Shannon entropy

Proof usesChow–Liu product approximation of a joint law · Mutual information of a finite joint law · Mutual information in terms of entropies · Shannon entropy as a p log p sum · Log-sum against a pushforward equals its negative entropy · Atom mass is at most the mass of its image, in reals

Used byChow–Liu optimality

TheoremNonnegativity of the Chow–Liu divergence#✓fully proved

The divergence of P from Chow–Liu's approximation is nonnegative, so ∑_i I(X_i; X_{j(i)}) ≤ ∑_i H(X_i) - H(X) for every dependence forest.

theorem divergence_nonneg (τ : DependenceForest ι) (p : PMF (∀ i, α i)) :
    0 ≤ τ.divergence p

Uses 4

Statement usesDependence forest · Divergence from the Chow–Liu approximation

Proof usesChow–Liu approximation as a probability mass function · Chow–Liu divergence as a Kullback–Leibler divergence

TheoremChow–Liu optimality#✓fully proved

Among dependence forests, a smaller divergence is the same as a larger mutual-information weight, so minimizing D(P ‖ P_τ) over dependence trees is maximizing the total mutual information ∑_i I(X_i; X_{j(i)}) of their edges.

theorem divergence_le_divergence_iff (τ τ' : DependenceForest ι) (p : PMF (∀ i, α i)) :
    τ.divergence p ≤ τ'.divergence p ↔ τ'.weight p ≤ τ.weight p

Uses 5

Statement usesDependence forest · Divergence from the Chow–Liu approximation · Mutual-information weight of a dependence forest

Proof usesChow–Liu identity · Shannon entropy

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.