InformationTheory.Shannon.Sanov.MultinomialLowerBound

Imports 3

Multinomial lower bound (Stirling-free) #

The Stirling-free multinomial lower bound for the type class cardinality (Cover-Thomas): (n+1)^{-|α|} · n^n / ∏ c(a)^{c(a)} ≤ |T_c|.

Main statements #

typeClassByCount_card_ge — multinomial lower bound (Stirling-free): (n+1)^{-|α|} · n^n / ∏ c(a)^{c(a)} ≤ |T_c|.
typeClassByCount_Qn_ge — lower bound on Q^n(T_c): Q^n(T_c) ≥ (n+1)^{-|α|} · exp(-n · klDivIndex c n Q).

Implementation notes #

The multinomial lower bound is proved without Stirling's approximation, using only the per-letter inequality c! · c^k ≤ k! · c^c.

References #

T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

Multinomial lower bound (Stirling-free) #

theorem

InformationTheory.Shannon.numTypes_le

source

{α : Type u_1} [Fintype α] [DecidableEq α] (n : ℕ) :

(Finset.univ.piAntidiag n).card ≤ (n + 1) ^ Fintype.card α

The number of types (count vectors c : α → ℕ with ∑ a, c a = n, equivalently the elements of piAntidiag univ n) is at most (n+1)^{|α|}.

Used by

theorem

InformationTheory.Shannon.prod_div_pow_eq_prod_pow_div_npow_of_sum

source

{α : Type u_1} [Fintype α] {n : ℕ} (c k : α → ℕ) (hk_sum : ∑ a : α, k a = n) :

∏ a : α, (↑(c a) / ↑n) ^ k a = (∏ a : α, ↑(c a) ^ k a) / ↑n ^ n

Used by

theorem

InformationTheory.Shannon.inv_mul_div_le_of_one_le_mul_mul_div

source

{B M P x : ℝ} (hB : 0 < B) (hP : 0 < P) (hx : 0 < x) (h : 1 ≤ B * (M * (P / x))) :

B⁻¹ * (x / P) ≤ M

Used by

theorem

InformationTheory.Shannon.multinomial_mul_prod_ratio_pow_le

source

{α : Type u_1} [Fintype α] {n : ℕ} (c k : α → ℕ) (hc_sum : ∑ a : α, c a = n) (hk_sum : ∑ a : α, k a = n) :

↑(Nat.multinomial Finset.univ k) * ∏ a : α, (↑(c a) / ↑n) ^ k a ≤ ↑(Nat.multinomial Finset.univ c) * ∏ a : α, (↑(c a) / ↑n) ^ c a

Used by

theorem

InformationTheory.Shannon.typeClassByCount_card_ge

source

{α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (c : α → ℕ) (hc_sum : ∑ a : α, c a = n) :

((↑n + 1) ^ Fintype.card α)⁻¹ * (↑n ^ n / ∏ a : α, ↑(c a) ^ c a) ≤ ↑⋯.toFinset.card

Multinomial lower bound: (n+1)^{-|α|} · n^n / ∏ c(a)^{c(a)} ≤ |T_c|.

Used by

theorem

InformationTheory.Shannon.typeClassByCount_card_le

source

{α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (c : α → ℕ) (hc_sum : ∑ a : α, c a = n) :

↑⋯.toFinset.card ≤ ↑n ^ n / ∏ a : α, ↑(c a) ^ c a

Multinomial upper bound (method of types): |T_c| ≤ n^n / ∏ c(a)^{c(a)}.

Used by

theorem

InformationTheory.Shannon.typeClassByCount_Qn_ge

source

{α : Type u_1} [Fintype α] [DecidableEq α] [MeasurableSpace α] [MeasurableSingletonClass α] (Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure Q] (hQpos : ∀ (a : α), 0 < Q.real {a}) {n : ℕ} (hn : 0 < n) (c : α → ℕ) (hc_sum : ∑ a : α, c a = n) :

((↑n + 1) ^ Fintype.card α)⁻¹ * Real.exp (-(↑n * klDivIndex c n Q)) ≤ ((MeasureTheory.Measure.pi fun (x : Fin n) => Q) (typeClassByCount c)).toReal

Lower bound on Q^n(T_c): Q^n(T_c) ≥ (n+1)^{-|α|} · exp(-n · klDivIndex c n Q).

Used by