Shannon.Entropy.Uniform

Phase 1 of the characterization: equiprobable distributions.

Main outputs:

• multiplicative/additive behavior on uniform choices (Apos_mul, Apos_pow);
• logarithmic characterization Apos H n = K H * log n;
• positivity of the scale factor K.

Phase 1: Equiprobable Characterization

theorem LeanPool.Shannon1948Formalization.relabel_compose_uniform_eq_uniform_mul (n m : ℕ+) : relabelProb (sigmaConstFinEquivFinMul n m) (composeProb (uniformPNat n) fun (x : Fin ↑n) => uniformPNat m) = uniformPNat (n * m)

theorem LeanPool.Shannon1948Formalization.Apos_mul (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) (n m : ℕ+) : Apos (fun {α : Type} [Fintype α] => H) (n * m) = Apos (fun {α : Type} [Fintype α] => H) n + Apos (fun {α : Type} [Fintype α] => H) m

theorem LeanPool.Shannon1948Formalization.Apos_one_zero (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) : Apos (fun {α : Type} [Fintype α] => H) 1 = 0

theorem LeanPool.Shannon1948Formalization.Apos_pow (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) (n : ℕ+) (k : ℕ) : Apos (fun {α : Type} [Fintype α] => H) (n ^ k) = ↑k * Apos (fun {α : Type} [Fintype α] => H) n

theorem LeanPool.Shannon1948Formalization.Apos_nonneg (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) (n : ℕ+) : 0 ≤ Apos (fun {α : Type} [Fintype α] => H) n

theorem LeanPool.Shannon1948Formalization.Apos_pos_two (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) : 0 < Apos (fun {α : Type} [Fintype α] => H) 2

theorem LeanPool.Shannon1948Formalization.Apos_pos_of_one_lt (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) {n : ℕ+} (hn : 1 < n) : 0 < Apos (fun {α : Type} [Fintype α] => H) n

Strict monotonicity gives positivity of Apos for any alphabet size > 1.

theorem LeanPool.Shannon1948Formalization.abs_sub_le_of_mem_interval {a b l u : ℝ} (haL : l ≤ a) (haU : a ≤ u) (hbL : l ≤ b) (hbU : b ≤ u) : |a - b| ≤ u - l

If two reals are in the same closed interval, their distance is interval width.

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

The canonical positive scale factor from the two-outcome uniform case.

Equations

• LeanPool.Shannon1948Formalization.K H = LeanPool.Shannon1948Formalization.Apos (fun {α : Type} [Fintype α] => H) 2 / Real.log 2

theorem LeanPool.Shannon1948Formalization.K_pos (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) : 0 < K fun {α : Type} [Fintype α] => H

theorem LeanPool.Shannon1948Formalization.Apos_ratio_logb_close (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) {s t n : ℕ+} (hs : 1 < s) : |Apos (fun {α : Type} [Fintype α] => H) t / Apos (fun {α : Type} [Fintype α] => H) s - Real.logb ↑↑s ↑↑t| ≤ 1 / ↑↑n

theorem LeanPool.Shannon1948Formalization.Apos_ratio_eq_logb (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) {s t : ℕ+} (hs : 1 < s) : Apos (fun {α : Type} [Fintype α] => H) t / Apos (fun {α : Type} [Fintype α] => H) s = Real.logb ↑↑s ↑↑t

theorem LeanPool.Shannon1948Formalization.Apos_eq_K_mul_log (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) (n : ℕ+) : Apos (fun {α : Type} [Fintype α] => H) n = (K fun {α : Type} [Fintype α] => H) * Real.log ↑↑n

theorem LeanPool.Shannon1948Formalization.Apos_pow_two_eq_K_log_pow (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) (k : ℕ) : Apos (fun {α : Type} [Fintype α] => H) (2 ^ k) = (K fun {α : Type} [Fintype α] => H) * Real.log (2 ^ k)

theorem LeanPool.Shannon1948Formalization.A_monotone (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) : Monotone (A fun {α : Type} [Fintype α] => H)

theorem LeanPool.Shannon1948Formalization.Apos_monotone (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) : Monotone (Apos fun {α : Type} [Fintype α] => H)

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

Entropy-form expression with natural logarithm.

Equations

• LeanPool.Shannon1948Formalization.entropyNat p = -∑ a : α, ↑p a * Real.log (↑p a)

noncomputable def LeanPool.Shannon1948Formalization.entropyBase {α : Type} [Fintype α] (b : ℝ) (p : ProbDist α) : ℝ

Entropy-form expression with logarithm base b.

Equations

• LeanPool.Shannon1948Formalization.entropyBase b p = -∑ a : α, ↑p a * Real.logb b (↑p a)

theorem LeanPool.Shannon1948Formalization.continuous_entropyNat {α : Type} [Fintype α] : Continuous fun (p : ProbDist α) => entropyNat p

theorem LeanPool.Shannon1948Formalization.nonempty_of_probDist {α : Type} [Fintype α] (p : ProbDist α) : Nonempty α

theorem LeanPool.Shannon1948Formalization.Apos_eq_K_mul_logb (H : {α : Type} → [inst : Fintype α] → ProbDist α → ℝ) (hH : ShannonEntropyAxioms fun {α : Type} [Fintype α] => H) (b : ℝ) (hb : 1 < b) (n : ℕ+) : Apos (fun {α : Type} [Fintype α] => H) n = (K fun {α : Type} [Fintype α] => H) * Real.log b * Real.logb b ↑↑n