TheoremStatement: 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.

Finite-alphabet Sanov bounds on the support simplex

Statement

Let $A$ be finite, let $p$ be a probability vector on $A$ , and set $S : = supp (p) = {a \in A : p (a) > 0}$ . Then $S$ is finite nonempty and $p (a) > 0$ on $S$ . For each $n \geq 1$ , use the finite product law $p^{\otimes n}$ from Finite product mass on words and The finite product law has iid coordinate maps on $A^{n}$ , and let $X_{1}^{(n)}, \dots, X_{n}^{(n)}$ be its coordinate maps. Let ${\hat{P}}_{n}$ be the empirical type of this coordinate word, viewed as a $Δ (A)$ -valued map. Identify the support simplex $Δ (S) : = {q \in [0, 1]^{S} : \sum_{a \in S} q (a) = 1}$ with the face of $Δ (A)$ whose coordinates outside $S$ vanish. Then ${\hat{P}}_{n} \in Δ (S)$ almost surely under $p^{\otimes n}$ . For any set $Γ \subseteq Δ (S)$ , let $Γ^{\circ}$ and $\overline{Γ}$ denote its interior and closure in the relative topology induced by $∥ \cdot ∥_{1}$ . With $\inf \emptyset = + \infty$ and $\ln 0 = - \infty$ , ${lim inf}_{n \to \infty} \frac{1}{n} \ln p^{\otimes n} ({\hat{P}}_{n} \in Γ) \geq - \inf_{q \in Γ^{\circ}} D (q ∥ p),$ and ${lim sup}_{n \to \infty} \frac{1}{n} \ln p^{\otimes n} ({\hat{P}}_{n} \in Γ) \leq - \inf_{q \in \overline{Γ}} D (q ∥ p) .$ For every $n \geq 1$ the finite upper bound $p^{\otimes n} ({\hat{P}}_{n} \in Γ) \leq (n + 1)^{∣ S ∣ - 1} \exp ⁣ (- n \inf_{q \in \overline{Γ}} D (q ∥ p))$ also holds. If the two infima agree, the limit exists and equals their negative common value. Equivalently, when $S \neq A$ , one may restrict the product sample space to $S^{n}$ without changing these event probabilities, since every word outside $S^{n}$ has zero product mass.

Facts & Assumptions

Given: A finite alphabet $A$ , a probability vector $p$ , its finite product laws and coordinate maps from the statement, and a set $Γ$ of empirical probability vectors. Write $S = supp (p)$ and $k = ∣ S ∣$ .

[F1]

Empirical types, n-types, and type classes: each word $x^{n}$ has empirical vector ${\hat{P}}_{x^{n}}$ , and its type class is $T_{q} = {x^{n} : {\hat{P}}_{x^{n}} = q}$ .

[F2]

Finite distributions, entropy, divergence, and stochastic matrices: $D (q ∥ p) = \sum_{a : q (a) > 0} q (a) \ln (q (a) / p (a))$ , with value $+ \infty$ if $q (a) > 0 = p (a)$ for some $a$ .

[F3]

The type classes partition the word space and have polynomial count: the type classes partition the word space and there are at most $(n + 1)^{k - 1}$ $n$ -types on a $k$ -letter support.

[F4]

Finite probability bounds for an empirical type: each $n$ -type $q$ satisfies $p^{\otimes n} (T_{q}) \leq e^{- n D (q ∥ p)}$ and the corresponding lower bound is $(n + 1)^{- (k - 1)} e^{- n D (q ∥ p)}$ .

[F5]

Every probability vector is approximated by n-types: every probability vector on the fixed finite support is within $k / n$ in $ℓ^{1}$ of an attainable $n$ -type.

[F6]

Finite relative entropy is continuous on a simplex with positive reference law: for a full-support reference vector $p$ on $S$ , $q \mapsto D (q ∥ p)$ is finite and continuous on all of $Δ (S)$ , including coordinates where $q (a) = 0$ .

[F7]

The finite product law has iid coordinate maps: on the finite alphabet $A$ , $p^{\otimes n}$ is a probability law on $A^{n}$ , and its coordinate maps are independent random elements, each with law $p$ .

[F8]

Finite product mass on words: each word $x^{n}$ has mass $\prod_{i = 1}^{n} p (x_{i})$ , and event masses are sums of these atom weights.

Proof

1.1F1F7F8algebra

By [F7], $p^{\otimes n}$ is a probability law on $A^{n}$ . Every word outside $S^{n}$ has a coordinate $a \notin S$ , so its product mass is zero by [F8]; hence $p^{\otimes n} (S^{n}) = 1$ and ${\hat{P}}_{n} \in Δ (S)$ almost surely by [F1]. The event ${{\hat{P}}_{n} \in Γ}$ is the disjoint union of the type classes $T_{q}$ with $q \in Γ \cap P_{n} (S)$ , so its probability is the sum of those finitely many class probabilities.

1.2F5choose

Fix $q \in Γ^{\circ}$ . By the definition of relative interior in the topology on $Δ (S)$ induced by $ℓ^{1}$ , some $ε > 0$ has the property that every $r \in Δ (S)$ with $∥ r - q ∥_{1} < ε$ belongs to $Γ$ . By [F5], the fixed rounding rule supplies an $n$ -type $q_{n}$ with $∥ q_{n} - q ∥_{1} \leq k / n$ for every $n$ , so $q_{n} \in Γ$ for all sufficiently large $n$ .

2.1F2F3F4step 1.1algebra

Every $q \in Γ \cap P_{n} (S)$ lies in $\overline{Γ}$ , so [F2] and the upper half of [F4] give $p^{\otimes n} (T_{q}) \leq e^{- n \inf_{r \in \overline{Γ}} D (r ∥ p)}$ . There are at most $(n + 1)^{k - 1}$ such types by [F3]; summing the classes from step 1.1 proves the finite upper bound, including the empty-set case.

2.2F4F6step 1.2algebra

For all sufficiently large $n$ , the event contains $T_{q_{n}}$ from step 1.2, so [F4] gives probability at least $(n + 1)^{- (k - 1)} e^{- n D (q_{n} ∥ p)}$ . By [F6], $D (q_{n} ∥ p) \to D (q ∥ p)$ ; taking normalized logarithms and the liminf gives at least $- D (q ∥ p)$ .

3.1givenstep 2.1algebra

If the event probability is positive, take logarithms of the finite upper bound in step 2.1 and divide by $n$ . If it is zero, its normalized logarithm is $- \infty$ by convention. Since $(k - 1) \ln (n + 1) / n \to 0$ , both cases yield the limsup inequality.

3.2step 2.2givenalgebra

Since step 2.2 holds for every $q \in Γ^{\circ}$ , the liminf is at least $- \inf_{q \in Γ^{\circ}} D (q ∥ p)$ . If $Γ^{\circ} = \emptyset$ , the right-hand side is $- \infty$ , so the inequality is automatic.

4.1step 1.2step 3.1step 3.2givenalgebra

When the interior and closure infima agree, steps 3.1 and 3.2 bound the limsup above and the liminf below by the same value. Since every liminf is at most the corresponding limsup, the limit exists and equals that common value. The proof covers the empty event by the stated extended-real conventions and uses the explicit rounding construction from step 1.2.

5.1givenF2F7step 4.1algebra∎

If $k = 1$ , then $Δ (S) = {p}$ . For $p \in Γ$ , the empirical law is always $p$ under the product law [F7], both infima are $D (p ∥ p) = 0$ , and the normalized log probability is $0$ ; for $p \notin Γ$ , both infima are $+ \infty$ and the probability is zero. Thus the one-letter support boundary also satisfies the statement.

Depends on

Used by

A finite Bernoulli large-deviation tail Example

Dependency tree · two levels

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