LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Conditional type-class cardinality bound

Statement

Let $U, V$ be finite nonempty alphabets, let $n \geq 1$ , and let $q$ be an attainable joint $n$ -type on $U \times V$ . For $v$ with $q_{V} (v) > 0$ , put $q_{U ∣ v} (u) : = q (u, v) / q_{V} (v)$ ; this is an $n q_{V} (v)$ -type. If $v^{n} \in V^{n}$ has empirical type $q_{V}$ , then $∣ {u^{n} \in U^{n} : {\hat{P}}_{u^{n}, v^{n}} = q} ∣ = \prod_{v : q_{V} (v) > 0} ∣ T_{q_{U ∣ v}} ∣ \leq \exp ⁣ (n H_{q} (U ∣ V)),$ where $T_{q_{U ∣ v}}$ is the type class of length $n q_{V} (v)$ and $H_{q} (U ∣ V)$ is the finite conditional entropy for joint law $q$ .

Facts & Assumptions

Given: The finite alphabets, blocklength, joint type, and fixed sequence $v^{n}$ in the Statement.

[F1]

Empirical types, n-types, and type classes: an empirical type records each symbol count divided by blocklength, and its type class is the set of words with that type.

[F2]

Marginals and positive-mass conditionals of a finite joint law are probability vectors: each conditional vector of a joint probability vector given a positive-mass value is a probability vector.

[F3]

Polynomially sharp bounds for type-class cardinality: for any finite alphabet and attainable type $r$ , $∣ T_{r} ∣ \leq e^{m H (r)}$ , where $m$ is that type's blocklength.

[F4]

Finite conditional entropy: $H_{q} (U ∣ V) = \sum_{v : q_{V} (v) > 0} q_{V} (v) H (q_{U ∣ v})$ , omitting zero-mass conditioning values.

[F5]

Finite distributions, entropy, divergence, and stochastic matrices: $H (r) = - \sum_{u : r (u) > 0} r (u) \ln r (u)$ with $0 \ln 0 = 0$ .

Proof

1.1givenF1F2construct

For each $v$ with $q_{V} (v) > 0$ , let $J_{v} : = {j : v_{j} = v}$ . The sets $J_{v}$ partition the positions of $v^{n}$ . A word $u^{n}$ has joint type $q$ with this fixed $v^{n}$ exactly when, within each $J_{v}$ , it places $n q (u, v)$ copies of symbol $u$ . These counts sum to $n q_{V} (v) = ∣ J_{v} ∣$ , and their ratios define the attainable type $q_{U ∣ v}$ of length $∣ J_{v} ∣$ . Restriction to each $J_{v}$ gives a bijection from the joint-type fiber to the Cartesian product of these local type classes, so their cardinalities multiply and give the displayed product. Values with $q_{V} (v) = 0$ have no positions and contribute factor $1$ .

2.1F3F4F5step 1.1algebra∎

Apply [F3] to each factor in step 1.1, with blocklength $n q_{V} (v)$ , to get $∣ T_{q_{U ∣ v}} ∣ \leq e^{n q_{V} (v) H (q_{U ∣ v})}$ . Multiplying the finite bounds gives $\exp (n \sum_{v : q_{V} (v) > 0} q_{V} (v) H (q_{U ∣ v}))$ , which equals $e^{n H_{q} (U ∣ V)}$ by [F4] and [F5]. The omitted zero-mass rows contribute zero to the entropy sum.

Depends on

Used by

Conditional typical-set fan cardinality bound Lemma

Dependency tree · two levels

13 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)