Shannon.Entropy.Converse

The converse direction: entropyNat satisfies ShannonEntropyAxioms.

Combined with the characterization theorems in Final.lean, this gives a true "if and only if": a functional H satisfies the Shannon conditions iff it is a positive multiple of entropyNat.

Main results

• entropyNat_relabelInvariant: relabeling outcomes preserves entropy
• entropyNat_grouping: two-stage decomposition identity
• entropyNat_shannonAxioms: ShannonEntropyAxioms entropyNat

Relabel invariance

theorem LeanPool.Shannon1948Formalization.entropyNat_relabelInvariant {α β : Type} [Fintype α] [Fintype β] (e : α ≃ β) (p : ProbDist α) : entropyNat (relabelProb e p) = entropyNat p

Entropy is invariant under relabeling outcomes by an equivalence.

Uniform monotonicity

theorem LeanPool.Shannon1948Formalization.entropyNat_uniformMonotone : StrictMono fun (n : ℕ+) => entropyNat (uniformPNat n)

Entropy on uniform distributions is strictly monotone in alphabet size.

Grouping

theorem LeanPool.Shannon1948Formalization.entropyNat_grouping {α : Type} [Fintype α] {β : α → Type} [(a : α) → Fintype (β a)] (p : ProbDist α) (q : (a : α) → ProbDist (β a)) : entropyNat (composeProb p q) = entropyNat p + ∑ a : α, ↑p a * entropyNat (q a)

Two-stage decomposition: H(compose p q) = H(p) + ∑ a, p(a) * H(q a).

Main theorem

theorem LeanPool.Shannon1948Formalization.entropyNat_shannonAxioms : ShannonEntropyAxioms fun {α : Type} [Fintype α] => entropyNat

entropyNat satisfies the Shannon entropy conditions.

This is the converse of the characterization: the characterization shows any H satisfying the conditions must be a positive multiple of entropyNat; this theorem shows entropyNat itself satisfies the conditions, proving the specification is consistent and completing the "if and only if".