Type-class size lower bound (Cover-Thomas) #

For a count vector c : α → ℕ with ∑ c = n, the type class T(c) := { x : Fin n → α | ∀ a, typeCount x a = c a } satisfies |T(c)| ≥ (n+1)^{-|α|} · exp(n · H(c/n)), where H(c/n) := -∑ (c(a)/n) · log(c(a)/n) is the empirical entropy.

Main definitions #

• entropyByCount — empirical entropy of the count vector.

Main statements #

• pow_div_prod_pow_eq_exp_n_entropyByCount — bridge identity nⁿ / ∏ c(a)^{c(a)} = exp(n · H(c/n)).

Implementation notes #

entropyByCount is defined directly rather than via klDivIndex with a uniform reference, since klDivIndex is asymmetric and the uniform substitution is heavy. The Real.log 0 = 0 convention makes the identity hold without a support restriction; each atom c(a) = 0 contributes 0 to both sides.