Shannon.Entropy.Core

Foundational definitions for the Shannon characterization development:

• finite probability distributions (ProbDist);
• Shannon-style condition bundle (ShannonEntropyAxioms);
• basic constructions used in all later phases (uniformPNat, composeProb, relabelProb).

Global roadmap (matching Shannon Appendix 2):

1. Equiprobable case: Apos H (n * m) = Apos H n + Apos H m, then Apos H n = K * log n.
2. Rational case: grouped equiprobable refinement implies H p = -K * ∑ p_i log p_i for rational probabilities.
3. Real case: floor-count rational approximants approxProb p N converge to p; continuity upgrades the rational formula to all real probabilities.

def LeanPool.Shannon1948Formalization.IsProbDist {α : Type} [Fintype α] (p : α → ℝ) : Prop

p has nonnegative masses that sum to one.

Equations

• LeanPool.Shannon1948Formalization.IsProbDist p = ((∀ (a : α), 0 ≤ p a) ∧ ∑ a : α, p a = 1)

@[reducible, inline]

abbrev LeanPool.Shannon1948Formalization.ProbDist (α : Type) [Fintype α] : Type

A probability distribution over a finite type α, bundled with simplex proofs. This keeps API signatures clean (no separate IsProbDist assumptions everywhere).

Equations

• LeanPool.Shannon1948Formalization.ProbDist α = { p : α → ℝ // LeanPool.Shannon1948Formalization.IsProbDist p }

@[implicit_reducible]

instance LeanPool.Shannon1948Formalization.instCoeFunProbDistForallReal {α : Type} [Fintype α] : CoeFun (ProbDist α) fun (x : ProbDist α) => α → ℝ

Equations

• LeanPool.Shannon1948Formalization.instCoeFunProbDistForallReal = { coe := fun (p : LeanPool.Shannon1948Formalization.ProbDist α) => ↑p }

theorem LeanPool.Shannon1948Formalization.prob_nonneg {α : Type} [Fintype α] (p : ProbDist α) (a : α) : 0 ≤ ↑p a

theorem LeanPool.Shannon1948Formalization.prob_sum_eq_one {α : Type} [Fintype α] (p : ProbDist α) : ∑ a : α, ↑p a = 1

theorem LeanPool.Shannon1948Formalization.prob_le_one {α : Type} [Fintype α] (p : ProbDist α) (a : α) : ↑p a ≤ 1

noncomputable def LeanPool.Shannon1948Formalization.uniformFin (n : ℕ) : ProbDist (Fin (n + 1))

Uniform distribution on Fin (n + 1).

Equations

• LeanPool.Shannon1948Formalization.uniformFin n = ⟨fun (x : Fin (n + 1)) => 1 / (↑n + 1), ⋯⟩

noncomputable def LeanPool.Shannon1948Formalization.uniformPNat (n : ℕ+) : ProbDist (Fin ↑n)

Uniform distribution on Fin n for positive natural n : ℕ+. This avoids n + 1 index gymnastics when formalizing Appendix 2.

Equations

• LeanPool.Shannon1948Formalization.uniformPNat n = ⟨fun (x : Fin ↑n) => 1 / ↑↑n, ⋯⟩

def LeanPool.Shannon1948Formalization.composeProb {α : Type} [Fintype α] {β : α → Type} [(a : α) → Fintype (β a)] (p : ProbDist α) (q : (a : α) → ProbDist (β a)) : ProbDist (Sigma β)

Composite distribution for a two-stage random choice.

Equations

• LeanPool.Shannon1948Formalization.composeProb p q = ⟨fun (x : Sigma β) => ↑p x.fst * ↑(q x.fst) x.snd, ⋯⟩

def LeanPool.Shannon1948Formalization.sigmaConstFinEquivFinMul (n m : ℕ+) : (_ : Fin ↑n) × Fin ↑m ≃ Fin ↑(n * m)

Equivalence between two-stage finite outcomes and Fin (n * m).

Equations

• LeanPool.Shannon1948Formalization.sigmaConstFinEquivFinMul n m = (Equiv.sigmaEquivProdOfEquiv fun (x : Fin ↑n) => Equiv.refl (Fin ↑m)).trans finProdFinEquiv

def LeanPool.Shannon1948Formalization.relabelProb {α β : Type} [Fintype α] [Fintype β] (e : α ≃ β) (p : ProbDist α) : ProbDist β

Relabel a distribution along an equivalence of finite types. This is the formal "event names do not matter" transport map.

Equations

• LeanPool.Shannon1948Formalization.relabelProb e p = ⟨fun (b : β) => ↑p (e.symm b), ⋯⟩

structure LeanPool.Shannon1948Formalization.ShannonEntropyAxioms (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) : Prop

Shannon's three conditions for a finite-choice uncertainty functional H. The final theorem will show any such H has entropy form up to a positive scale.

• continuous {α : Type} [Fintype α] : Continuous fun (p : ProbDist α) => H p

  Continuity in probabilities (for each finite alphabet).

• uniformMonotone : StrictMono fun (n : ℕ+) => H (uniformPNat n)

  On uniform distributions, uncertainty is monotone in alphabet size.

• relabelInvariant {α β : Type} [Fintype α] [Fintype β] (e : α ≃ β) (p : ProbDist α) : H (relabelProb e p) = H p

  Invariance under relabeling outcomes by a finite equivalence.

• grouping {α : Type} [Fintype α] {β : α → Type} [(a : α) → Fintype (β a)] (p : ProbDist α) (q : (a : α) → ProbDist (β a)) : H (composeProb p q) = H p + ∑ a : α, ↑p a * H (q a)

  Grouping (recursivity): a two-stage choice decomposes additively.

noncomputable def LeanPool.Shannon1948Formalization.A (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (n : ℕ) : ℝ

A_H(n) is Shannon's notation for uncertainty on the uniform distribution with n + 1 equiprobable outcomes.

Equations

• LeanPool.Shannon1948Formalization.A H n = H (LeanPool.Shannon1948Formalization.uniformFin n)

noncomputable def LeanPool.Shannon1948Formalization.Apos (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (n : ℕ+) : ℝ

Apos H n is uncertainty for exactly n equiprobable outcomes (n : ℕ+).

Equations

• LeanPool.Shannon1948Formalization.Apos H n = H (LeanPool.Shannon1948Formalization.uniformPNat n)