Shannon.Entropy.Joint

Joint distributions on product types, marginals, conditional entropy, and the chain rule for Shannon entropy.

These definitions and theorems support the Section 6 properties by providing the infrastructure for multi-variable entropy identities.

Main definitions

• marginalFst, marginalSnd: marginal distributions from a joint distribution
• prodDist: product (independent) distribution from two marginals
• IsIndependent: predicate for independence of a joint distribution
• condEntropy: conditional entropy H_X(Y) = -∑ p(x,y) log(p(x,y)/p(x))
• mutualInfo: mutual information I(X;Y) = H(X) + H(Y) - H(X,Y)

Main results

• chain_rule: H(X,Y) = H(X) + H_X(Y)
• entropyNat_prodDist: H(X × Y) = H(X) + H(Y) for independent distributions
• marginalFst_prodDist, marginalSnd_prodDist: marginals of product distributions

Marginals and product distributions

def LeanPool.Shannon1948Formalization.marginalFst {α β : Type} [Fintype α] [Fintype β] (p : ProbDist (α × β)) : ProbDist α

First marginal: (marginalFst p)(a) = ∑_b p(a, b).

Equations

• LeanPool.Shannon1948Formalization.marginalFst p = ⟨fun (a : α) => ∑ b : β, ↑p (a, b), ⋯⟩

def LeanPool.Shannon1948Formalization.marginalSnd {α β : Type} [Fintype α] [Fintype β] (p : ProbDist (α × β)) : ProbDist β

Second marginal: (marginalSnd p)(b) = ∑_a p(a, b).

Equations

• LeanPool.Shannon1948Formalization.marginalSnd p = ⟨fun (b : β) => ∑ a : α, ↑p (a, b), ⋯⟩

def LeanPool.Shannon1948Formalization.prodDist {α β : Type} [Fintype α] [Fintype β] (p : ProbDist α) (q : ProbDist β) : ProbDist (α × β)

Product distribution: (prodDist p q)(a, b) = p(a) * q(b).

Equations

• LeanPool.Shannon1948Formalization.prodDist p q = ⟨fun (ab : α × β) => ↑p ab.1 * ↑q ab.2, ⋯⟩

Independence, conditional entropy, mutual information

def LeanPool.Shannon1948Formalization.IsIndependent {α β : Type} [Fintype α] [Fintype β] (p : ProbDist (α × β)) : Prop

A joint distribution is independent when it factors as the product of its marginals.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.Shannon1948Formalization.condEntropy {α β : Type} [Fintype α] [Fintype β] (p : ProbDist (α × β)) : ℝ

Conditional entropy H_X(Y) = -∑_{x,y} p(x,y) log(p(x,y) / p_X(x)).

This measures the average remaining uncertainty in Y once X is known. The formula uses Lean's 0 / 0 = 0 and log 0 = 0 conventions: when p_X(x) = 0 we also have p(x,y) = 0, so the term vanishes.

Equations

• LeanPool.Shannon1948Formalization.condEntropy p = -∑ ab : α × β, ↑p ab * Real.log (↑p ab / ↑(LeanPool.Shannon1948Formalization.marginalFst p) ab.1)

noncomputable def LeanPool.Shannon1948Formalization.mutualInfo {α β : Type} [Fintype α] [Fintype β] (p : ProbDist (α × β)) : ℝ

Mutual information I(X;Y) = H(X) + H(Y) - H(X,Y).

Equations

• One or more equations did not get rendered due to their size.

Support lemmas

theorem LeanPool.Shannon1948Formalization.prob_eq_zero_of_marginalFst_eq_zero {α β : Type} [Fintype α] [Fintype β] (p : ProbDist (α × β)) (a : α) (ha : ↑(marginalFst p) a = 0) (b : β) : ↑p (a, b) = 0

If a first marginal is zero, every joint probability with that first coordinate is zero (since the marginal is a sum of nonnegative terms).

theorem LeanPool.Shannon1948Formalization.marginalFst_pos_of_prob_pos {α β : Type} [Fintype α] [Fintype β] (p : ProbDist (α × β)) (a : α) (b : β) (h : 0 < ↑p (a, b)) : 0 < ↑(marginalFst p) a

A positive joint probability implies a positive first marginal.

Marginals of product distributions

theorem LeanPool.Shannon1948Formalization.marginalFst_prodDist {α β : Type} [Fintype α] [Fintype β] (p : ProbDist α) (q : ProbDist β) : marginalFst (prodDist p q) = p

The first marginal of a product distribution recovers the first factor.

theorem LeanPool.Shannon1948Formalization.marginalSnd_prodDist {α β : Type} [Fintype α] [Fintype β] (p : ProbDist α) (q : ProbDist β) : marginalSnd (prodDist p q) = q

The second marginal of a product distribution recovers the second factor.

Chain rule

theorem LeanPool.Shannon1948Formalization.chain_rule {α β : Type} [Fintype α] [Fintype β] (p : ProbDist (α × β)) : entropyNat p = entropyNat (marginalFst p) + condEntropy p

Chain rule for entropy: H(X,Y) = H(X) + H_X(Y).

The proof expands H(X) over the product type by distributing the marginal weight, then combines termwise using log(p/m) = log p - log m.

Product distribution entropy

theorem LeanPool.Shannon1948Formalization.entropyNat_prodDist {α β : Type} [Fintype α] [Fintype β] (p : ProbDist α) (q : ProbDist β) : entropyNat (prodDist p q) = entropyNat p + entropyNat q

Additivity for independent distributions: H(X × Y) = H(X) + H(Y).

The proof uses log(p(a) * q(b)) = log p(a) + log q(b) for each nonzero term, then separates the double sum using ∑ qᵢ = 1 and ∑ pᵢ = 1.