Shannon.Entropy.Rational

Phase 2 of the characterization: rational probabilities.

This module derives the entropy formula for distributions of the form p_i = n_i / N via grouped equiprobable refinement and the grouping condition. It also includes a worked decomposition corresponding to Shannon's (1/2, 1/3, 1/6) narrative.

Phase 2: Rational Probabilities via Grouping

theorem LeanPool.Shannon1948Formalization.relabel_compose_rational_eq_uniform {α : Type} [Fintype α] (p : ProbDist α) (n : α → ℕ) (hpos : ∀ (a : α), 0 < n a) (N : ℕ) (hN : 0 < N) (hp : ∀ (a : α), ↑p a = ↑(n a) / ↑N) (e : (a : α) × Fin (n a) ≃ Fin N) : relabelProb e (composeProb p fun (a : α) => uniformPNat ⟨n a, ⋯⟩) = uniformPNat ⟨N, hN⟩

theorem LeanPool.Shannon1948Formalization.grouping_on_rational_counts (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) {α : Type} [Fintype α] (p : ProbDist α) (n : α → ℕ) (hpos : ∀ (a : α), 0 < n a) (N : ℕ) (hN : 0 < N) (hsum : ∑ a : α, n a = N) (hp : ∀ (a : α), ↑p a = ↑(n a) / ↑N) : Apos (fun {α : Type} [Fintype α] => H) ⟨N, hN⟩ = H p + ∑ a : α, ↑p a * Apos (fun {α : Type} [Fintype α] => H) ⟨n a, ⋯⟩

theorem LeanPool.Shannon1948Formalization.entropyNat_of_rational_counts_aux (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) {α : Type} [Fintype α] (p : ProbDist α) (n : α → ℕ) (hpos : ∀ (a : α), 0 < n a) (N : ℕ) (hN : 0 < N) (hsum : ∑ a : α, n a = N) (hp : ∀ (a : α), ↑p a = ↑(n a) / ↑N) : H p = (K fun {α : Type} [Fintype α] => H) * Real.log ↑N - ∑ a : α, ↑p a * ((K fun {α : Type} [Fintype α] => H) * Real.log ↑(n a))

theorem LeanPool.Shannon1948Formalization.entropyNat_of_rational_counts (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) {α : Type} [Fintype α] (p : ProbDist α) (n : α → ℕ) (hpos : ∀ (a : α), 0 < n a) (N : ℕ) (hN : 0 < N) (hsum : ∑ a : α, n a = N) (hp : ∀ (a : α), ↑p a = ↑(n a) / ↑N) : H p = (-K fun {α : Type} [Fintype α] => H) * ∑ a : α, ↑p a * Real.log (↑p a)

noncomputable def LeanPool.Shannon1948Formalization.workedP : ProbDist Bool

First-stage split used in the (1/2, 1/3, 1/6) worked decomposition.

Equations

• LeanPool.Shannon1948Formalization.workedP = ⟨fun (x : Bool) => 1 / 2, LeanPool.Shannon1948Formalization.workedP._proof_2⟩

def LeanPool.Shannon1948Formalization.workedFib : Bool → Type

Second-stage alphabets for the worked decomposition: true has one outcome; false has two outcomes.

Equations

• LeanPool.Shannon1948Formalization.workedFib true = Fin 1
• LeanPool.Shannon1948Formalization.workedFib false = Fin 2

@[implicit_reducible]

instance LeanPool.Shannon1948Formalization.instFintypeWorkedFib (b : Bool) : Fintype (workedFib b)

Equations

• LeanPool.Shannon1948Formalization.instFintypeWorkedFib true = id inferInstance
• LeanPool.Shannon1948Formalization.instFintypeWorkedFib false = id inferInstance

noncomputable def LeanPool.Shannon1948Formalization.workedQ (b : Bool) : ProbDist (workedFib b)

Second-stage conditional probabilities for the worked decomposition.

Equations

• LeanPool.Shannon1948Formalization.workedQ true = id (LeanPool.Shannon1948Formalization.uniformPNat ⟨1, LeanPool.Shannon1948Formalization.workedQ._proof_1⟩)
• LeanPool.Shannon1948Formalization.workedQ false = id ⟨fun (i : Fin 2) => if i = 0 then 2 / 3 else 1 / 3, LeanPool.Shannon1948Formalization.workedQ._proof_4⟩

noncomputable def LeanPool.Shannon1948Formalization.workedCompose : ProbDist (Sigma workedFib)

The composed distribution in the worked (1/2, 1/3, 1/6) example.

Equations

• LeanPool.Shannon1948Formalization.workedCompose = LeanPool.Shannon1948Formalization.composeProb LeanPool.Shannon1948Formalization.workedP LeanPool.Shannon1948Formalization.workedQ

theorem LeanPool.Shannon1948Formalization.workedCompose_masses : ↑workedCompose ⟨true, 0⟩ = 1 / 2 ∧ ↑workedCompose ⟨false, 0⟩ = 1 / 3 ∧ ↑workedCompose ⟨false, 1⟩ = 1 / 6

Masses in the worked decomposition: (true, 0) has mass 1/2, (false, 0) has mass 1/3, and (false, 1) has mass 1/6.

theorem LeanPool.Shannon1948Formalization.worked_grouping_identity (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) : H workedCompose = H workedP + 1 / 2 * H (workedQ false)

Worked grouping identity corresponding to Shannon's (1/2, 1/3, 1/6) narrative: first choose true/false with probabilities (1/2, 1/2), then if false choose between two outcomes with probabilities (2/3, 1/3).