LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

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.

Finite type-class cardinality bounds

Statement

Let $A$ be a finite nonempty alphabet of size $m$ , let $n \geq 1$ , and let $q$ be an attainable empirical distribution with integer counts $n_{a} = n q (a)$ . Its type class $T_{q} : = {a^{n} \in A^{n} : {\hat{P}}_{a^{n}} = q}$ satisfies $(n + 1)^{- m} \exp (n H (q)) \leq ∣ T_{q} ∣ \leq \exp (n H (q)),$ where $H (q) : = - \sum_{a : q (a) > 0} q (a) \ln q (a)$ and $0 \ln 0 : = 0$ .

Facts & Assumptions

Given: The finite alphabet, positive blocklength, and attainable type $q$ .

[F1]

Finite strongly typical sets with support restriction: ${\hat{P}}_{a^{n}} (a)$ is the count of $a$ in $a^{n}$ divided by $n$ , and a type class is the set of sequences with that count vector.

[F2]

Finite distributions, entropy, divergence, and stochastic matrices: for a finite probability vector, $H (q) = - \sum_{a : q (a) > 0} q (a) \ln q (a)$ , with $0 \ln 0 = 0$ .

Proof

1.1F1F2algebra

Under the product law $q^{\otimes n}$ , every $a^{n} \in T_{q}$ has probability $\prod_{a} q (a)^{n_{a}} = \exp (- n H (q))$ , omitting zero-count coordinates. Since the total probability of $T_{q}$ is at most one, $∣ T_{q} ∣ \exp (- n H (q)) \leq 1$ , which gives the upper bound.

1.2F1algebra

To bound the probability of $T_{q}$ below, compare it with an arbitrary attainable type $r$ with counts $m_{a} = n r (a)$ . If $m_{a} > 0 = n_{a}$ for some $a$ , then $\Pr_{q^{\otimes n}} (T_{r}) = 0$ . Otherwise let $k_{a} = m_{a} - n_{a}$ for each $a$ with $n_{a} > 0$ . The ratio is $\frac{\Pr_{q^{\otimes n}} (T_{r})}{\Pr_{q^{\otimes n}} (T_{q})} = \frac{\prod_{a} n_{a}!}{\prod_{a} m_{a}!} \prod_{a : n_{a} > 0} {(\frac{n_{a}}{n})}^{k_{a}} .$ For $k_{a} \geq 0$ , the corresponding factor is at most $n^{- k_{a}}$ because $(n_{a} + 1) \dots (n_{a} + k_{a}) \geq n_{a}^{k_{a}}$ . For $k_{a} = - s_{a} < 0$ , it is at most $n^{s_{a}}$ because $n_{a} (n_{a} - 1) \dots (n_{a} - s_{a} + 1) \leq n_{a}^{s_{a}}$ . The equal-total-count relation gives $\sum_{k_{a} > 0} k_{a} = \sum_{k_{a} < 0} s_{a}$ , so the product of these bounds is at most one. Thus $T_{q}$ has maximum probability among all type classes under $q^{\otimes n}$ .

2.1F1F2step 1.2algebra∎

Each of the $m$ counts has at most $n + 1$ values, so there are at most $(n + 1)^{m}$ types. Their probabilities sum to one; since $T_{q}$ is a most probable type class by step 1.2, its probability is at least $(n + 1)^{- m}$ . Using $\Pr (T_{q}) = ∣ T_{q} ∣ \exp (- n H (q))$ proves the lower bound.

Depends on

Used by

Dependency tree · two levels

3 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

Abbas El Gamal and Young-Han Kim, Network Information Theory, author lecture notes (standard reference, not scraped)
Thomas M. Cover and Joy A. Thomas, Elements of Information Theory, second edition (standard reference, not scraped)