LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Polynomially sharp bounds for type-class cardinality

Statement

Let $A$ be a finite alphabet of size $k \geq 1$ , let $n \geq 1$ , and let $q \in P_{n} (A)$ . With natural logarithms, $(n + 1)^{- (k - 1)} e^{n H (q)} \leq ∣ T_{q} ∣ \leq e^{n H (q)} .$

Facts & Assumptions

Given: The finite alphabet $A$ , the positive integer $n$ , an attainable type $q$ , and the finite entropy convention.

[F1]

Empirical types, n-types, and type classes: $P_{n} (A)$ consists of attainable empirical vectors, and $T_{q}$ is the fiber of type $q$ .

[F2]

The type classes partition the word space and have polynomial count: the type classes partition $A^{n}$ , and there are at most $(n + 1)^{k - 1}$ of them.

[F3]

Finite distributions, entropy, divergence, and stochastic matrices: $H (q) = - \sum_{a : q (a) > 0} q (a) \ln q (a)$ , omitting zero coordinates.

[F4]

The finite product law has iid coordinate maps: for any probability vector $q$ , $q^{\otimes n}$ is a probability law whose word mass is $\prod_{i} q (x_{i})$ .

Proof

1.1F1F3F4algebra

Put $m_{a} = n q (a)$ . The class $T_{q}$ consists of the arrangements of $m_{a}$ copies of each $a$ , so it has $n! / \prod_{a} m_{a}!$ words: there are $n!$ position orders before dividing by the $m_{a}!$ permutations of identical copies for each letter. Under $q^{\otimes n}$ each word has mass $\prod_{a : m_{a} > 0} q (a)^{m_{a}} = e^{- n H (q)}$ by [F3, F4].

1.2F1F3F4algebra

For any nonnegative integer count vector $r = (r_{a})$ summing to $n$ , its class has $n! / \prod_{a} r_{a}!$ arrangements, obtained by permuting $n$ labeled copies and dividing by the $r_{a}!$ permutations of identical letters; each word has product mass $\prod_{a : r_{a} > 0} q (a)^{r_{a}}$ by [F4]. Thus its multinomial probability is $\frac{n!}{\prod_{a} r_{a}!} \prod_{a : r_{a} > 0} q (a)^{r_{a}}$ . It is zero if $r_{a} > 0$ where $m_{a} = 0$ . Otherwise its ratio to the positive probability of count vector $m$ is $\prod_{a : m_{a} > 0} \frac{m_{a}!}{r_{a}!} m_{a}^{r_{a} - m_{a}}$ , since the powers of $n$ cancel using $\sum_{a} (r_{a} - m_{a}) = 0$ . For $r_{a} > m_{a}$ the factor is $\prod_{j = m_{a} + 1}^{r_{a}} m_{a} / j \leq 1$ ; for $0 \leq r_{a} < m_{a}$ it is $\prod_{j = r_{a} + 1}^{m_{a}} j / m_{a} \leq 1$ ; for equality it is $1$ . Hence $m$ is a mode.

2.1F1F3F4step 1.1algebra

Since $q^{\otimes n}$ is a probability law by [F4], $q^{\otimes n} (T_{q}) = ∣ T_{q} ∣ e^{- n H (q)} \leq 1$ by step 1.1. Rearranging gives $∣ T_{q} ∣ \leq e^{n H (q)}$ .

2.2F1F2F4step 1.2algebra

The count-vector events are exactly the type classes in [F1], so they partition the sample space under the probability law $q^{\otimes n}$ from [F4]. By [F2] there are at most $(n + 1)^{k - 1}$ such vectors. Since $m$ is modal by step 1.2, its class has probability at least the average of the class probabilities, so $q^{\otimes n} (T_{q}) \geq (n + 1)^{- (k - 1)}$ .

3.1step 1.1step 2.2algebra∎

Step 1.1 gives $q^{\otimes n} (T_{q}) = ∣ T_{q} ∣ e^{- n H (q)}$ . Combining this equality with step 2.2 and rearranging proves the lower bound.

Depends on

Used by

A balanced binary type class is not exactly exponential in entropy Counterexample
Binary type classes at length ten Example
Conditional type-class cardinality bound Lemma
Finite probability bounds for an empirical type Lemma
Uniform entropy approximation for type-class sizes Theorem

Dependency tree · two levels

12 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Yury Polyanskiy and Yihong Wu, Information Theory: From Coding to Learning, author-hosted book draft (standard reference, not scraped)
Thomas M. Cover and Joy A. Thomas, Elements of Information Theory, second edition, Chapter 11 (standard reference, not scraped)