TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-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.

KL is the iid type-II testing exponent

Statement

Let $P, Q$ be probability vectors on a finite nonempty alphabet $X$ . For $n \geq 1$ , write $P^{n}, Q^{n}$ for the product vectors on $X^{n}$ , with $P^{n} (x_{1}, \dots, x_{n}) = \prod_{i = 1}^{n} p_{x_{i}}$ and similarly for $Q^{n}$ . For every fixed $ϵ \in (0, 1)$ , with $β_{ϵ}$ oriented as in Finite type-II testing function with explicit orientation, $\lim_{n \to \infty} - \frac{1}{n} \log β_{ϵ} (P^{n}, Q^{n}) = D (P ∥ Q),$ where $- \log 0 : = + \infty$ .

Facts & Assumptions

Given: $P, Q$ as in the Statement and a fixed $ϵ \in (0, 1)$ .

[F1]

Finite probability vectors: $P, Q$ are probability vectors on the same finite alphabet.

[F2]

Finite Kullback–Leibler divergence: $D (P ∥ Q) = + \infty$ if $P ≪̸ Q$ .

[F3]

Finite type-II testing function with explicit orientation: $β_{ϵ} (P, Q)$ is the infimum alternative acceptance probability $E_{Q} [1 - ϕ]$ over randomized rejection functions $ϕ : X \to [0, 1]$ satisfying $E_{P} ϕ \leq ϵ$ .

[F4]

Finite iid log-likelihood averages concentrate: when $P ≪ Q$ , the empirical log-likelihood ratio $L_{n} / n$ converges in probability under $P^{n}$ to $D (P ∥ Q)$ , and on the support $Q^{n} = P^{n} \exp (- L_{n})$ .

Proof

1.1F1F2F3givenconstructalgebra

First suppose $P ≪̸ Q$ . The set $S : = {x : p_{x} > 0 = q_{x}}$ has $r : = P (S) > 0$ . For each $n$ , let $A_{n} \subseteq X^{n}$ be the event that at least one coordinate lies in $S$ , and define a test $ϕ_{n}$ to reject only on $A_{n}^{c}$ . Then $E_{P^{n}} ϕ_{n} = P^{n} (A_{n}^{c}) = (1 - r)^{n} \to 0$ , while $E_{Q^{n}} [1 - ϕ_{n}] = Q^{n} (A_{n}) = 0$ . For every fixed $ϵ > 0$ the test is feasible for all sufficiently large $n$ , so $β_{ϵ} (P^{n}, Q^{n}) = 0$ there and the exponent is $+ \infty = D (P ∥ Q)$ .

1.2F1F3F4givenconstructalgebra

Now suppose $P ≪ Q$ , put $D = D (P ∥ Q)$ , and fix $δ > 0$ . On $supp (P)^{n}$ write $L_{n} (x_{1}, \dots, x_{n}) = \sum_{i = 1}^{n} \log (p_{x_{i}} / q_{x_{i}})$ . Define $A_{n} = {x \in supp (P)^{n} : L_{n} (x) \geq n (D - δ)}$ and reject outside $A_{n}$ . By [F4], $P^{n} (A_{n}) \to 1$ , so this test has type-I error at most $ϵ$ for all sufficiently large $n$ . For each $x \in A_{n}$ , $Q^{n} (x) = P^{n} (x) e^{- L_{n} (x)} \leq P^{n} (x) \exp (- n (D - δ))$ ; summing gives $β_{ϵ} (P^{n}, Q^{n}) \leq Q^{n} (A_{n}) \leq \exp (- n (D - δ))$ .

2.1F1F3F4step 1.2givenalgebra

Let $ψ : X^{n} \to [0, 1]$ be the acceptance probability of any test feasible for $β_{ϵ} (P^{n}, Q^{n})$ , so $E_{P^{n}} ψ \geq 1 - ϵ$ . Set $B_{n} = {x \in supp (P)^{n} : L_{n} (x) \leq n (D + δ)}$ . By [F4], $P^{n} (B_{n}^{c}) \to 0$ . Since the $Q^{n}$ expectation includes all terms on $supp (P)^{n}$ , its nonnegative terms give $E_{Q^{n}} ψ \geq E_{P^{n}} [ψ e^{- L_{n}} 1_{B_{n}}] \geq \exp (- n (D + δ)) (1 - ϵ - P^{n} (B_{n}^{c}))$ . This holds for every feasible test, hence also for the infimum $β_{ϵ} (P^{n}, Q^{n})$ . For all sufficiently large $n$ the last factor is positive.

3.1step 1.1step 1.2step 2.1algebra∎

Steps 1.2 and 2.1 imply $D - δ \leq {lim inf}_{n} - \frac{1}{n} \log β_{ϵ} (P^{n}, Q^{n}) \leq {lim sup}_{n} - \frac{1}{n} \log β_{ϵ} (P^{n}, Q^{n}) \leq D + δ$ , because $- \frac{1}{n} \log (1 - ϵ - P^{n} (B_{n}^{c})) \to 0$ . Since $δ > 0$ was arbitrary, the limit equals $D$ . Together with step 1.1 this proves the extended-real statement.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

17 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, Chapter 14, §14.5, Theorem 14.13 and full proof (standard reference, not scraped)