ExampleConstruction: AI-adaptedVerification: 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.

A finite Bernoulli large-deviation tail

Example

For $p \in [0, 1)$ , let $b_{p}$ be the binary probability vector $b_{p} (1) = p$ , $b_{p} (0) = 1 - p$ . On ${0, 1}^{n}$ use the product law $b_{p}^{\otimes n}$ from Finite product mass on words, and let $X_{i} (x^{n}) = x_{i}$ be its coordinate maps; by The finite product law has iid coordinate maps these are independent Bernoulli $(p)$ variables. Let $a \in (p, 1]$ , define ${\hat{p}}_{n} = n^{- 1} \sum_{i = 1}^{n} X_{i}$ , $q_{n} = ⌈ n a ⌉ / n$ , and $d (q ∥ p) : = q \ln \frac{q}{p} + (1 - q) \ln \frac{1 - q}{1 - p},$ with zero-mass summands omitted, $d (0 ∥ 0) : = 0$ , and $d (q ∥ 0) = + \infty$ for $q > 0$ . Then $(n + 1)^{- 1} e^{- n d (q_{n} ∥ p)} \leq b_{p}^{\otimes n} ({\hat{p}}_{n} \geq a) \leq (n + 1) e^{- n d (a ∥ p)} .$ Consequently $\lim_{n \to \infty} \frac{1}{n} \ln b_{p}^{\otimes n} ({\hat{p}}_{n} \geq a) = - d (a ∥ p),$ including the value $- \infty$ when $p = 0$ . For $p = 1 / 2$ , $a = 3 / 4$ , and $n = 4$ , the exact tail is $5 / 16$ ; under AC, Hoeffding also gives the bound $e^{- 1 / 2}$ for this same event.

Facts & Assumptions

Given: A finite Bernoulli product model with parameter $p \in [0, 1)$ , threshold $a \in (p, 1]$ , and integer $n \geq 1$ . The Hoeffding comparison assumes AC.

[A1]

The Axiom of Choice: every family of nonempty sets has a choice function. The example invokes this axiom only to apply the Hoeffding supplier in step 4.1.

[F1]

Empirical types, n-types, and type classes: the empirical type of a binary word is its fraction of ones, and its type class consists of words with that fraction.

[F2]

Finite distributions, entropy, divergence, and stochastic matrices: finite relative entropy uses natural logarithms, $0 \ln 0 = 0$ , and equals $+ \infty$ if positive mass is placed where the reference law is zero.

[F3]

Finite probability bounds for an empirical type: for each binary $n$ -type $q$ , $(n + 1)^{- 1} e^{- n d (q ∥ p)} \leq P ({\hat{p}}_{n} = q) \leq e^{- n d (q ∥ p)}$ .

[F4]

Finite relative entropy is continuous on a simplex with positive reference law: when $0 < p < 1$ , $q \mapsto d (q ∥ p)$ is continuous on $[0, 1]$ .

[F5]

Finite-alphabet Sanov bounds on the support simplex: on the support simplex, the Sanov liminf uses the infimum over relative interior and the limsup uses the infimum over relative closure; equality of these infima gives the limit.

[F6]

Hoeffding inequality for independent bounded sums: under AC, for independent integrable $X_{i} \in [a_{i}, b_{i}]$ and $t > 0$ , the one-sided bound is $P (\sum_{i} (X_{i} - E X_{i}) \geq t) \leq \exp (- 2 t^{2} / \sum_{i} (b_{i} - a_{i})^{2})$ when the denominator is positive.

[F7]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: for $x > 0$ , $\ln^{'} (x) = 1 / x$ .

[F8]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : if a real function is continuous on a closed interval and differentiable on its interior, its increment equals its derivative at some interior point times the interval length.

[F9]

The type classes partition the word space and have polynomial count: on a binary alphabet there are at most $n + 1$ attainable $n$ -types.

[F10]

The finite product law has iid coordinate maps: the sample law on ${0, 1}^{n}$ is a probability law and its coordinate variables are independent with Bernoulli $(p)$ marginal law.

Verification

Given: The stated Bernoulli model and thresholds.

1.1F1F2F3F10givenalgebra

If $p = 0$ , every coordinate equals $0$ almost surely by [F10], so the tail is zero and $d (q_{n} ∥ p) = d (a ∥ p) = + \infty$ ; both finite bounds have right-hand sides zero. If $0 < p < 1$ , the tail is the union of binary type classes with $q \geq a$ , and the attainable type $q_{n} = ⌈ n a ⌉ / n$ belongs to the event, so [F3] gives the lower bound.

1.2F4F7F8givenalgebra

Suppose $0 < p < 1$ and $0 < a < 1$ . For every $x \in (p, 1)$ , [F7] gives $\frac{d}{d x} d (x ∥ p) = \ln \frac{x (1 - p)}{p (1 - x)} > 0$ . For any $a \leq u < v < 1$ , the finite logarithmic formula is continuous on $[u, v]$ and differentiable on $(u, v)$ , so [F8] gives $d (v ∥ p) > d (u ∥ p)$ . Thus $d (\cdot ∥ p)$ is increasing on $[a, 1)$ , and continuity [F4] extends $d (q ∥ p) \geq d (a ∥ p)$ to $q = 1$ .

2.1F3F9step 1.2algebra

For $0 < p < 1$ and $0 < a < 1$ , there are at most $n + 1$ binary types by [F9]. Each tail type has probability at most $e^{- n d (q ∥ p)}$ by [F3], and step 1.2 gives $d (q ∥ p) \geq d (a ∥ p)$ , so summing the types proves the finite upper bound.

2.2F4F5step 1.1step 1.2algebra

If $0 < p < a < 1$ , then for $Γ = [a, 1]$ the relative interior in $[0, 1]$ is $(a, 1]$ and the closure is $[a, 1]$ . By step 1.2 and continuity [F4], both divergence infima equal $d (a ∥ p)$ , so [F5] gives the stated limit. If $a = 1$ and $0 < p < 1$ , the event is exactly all ones and has probability $p^{n} = e^{- n d (1 ∥ p)}$ , giving the limit directly. The case $p = 0$ is in step 1.1.

3.1step 1.1step 2.1step 2.2algebra

For $0 < p < 1$ and $0 < a < 1$ , summing the type upper bounds from step 2.1 yields the displayed finite upper bound; when $a = 1$ and $0 < p < 1$ , step 2.2 gives the exact value $p^{n} \leq (n + 1) p^{n}$ , while $p = 0$ is covered in step 1.1.

4.1A1F1F6F10givenalgebra∎

For $p = 1 / 2$ , $a = 3 / 4$ , and $n = 4$ , the event contains four words with three ones and one with four, so its probability is $5 / 16$ . By [F10], the four coordinates are independent and take values in $[0, 1]$ , hence are integrable. Thus [F6] applies with $\sum_{i} (X_{i} - E X_{i}) \geq 1$ on the event and $\sum_{i} (b_{i} - a_{i})^{2} = 4$ for bounds $a_{i} = 0, b_{i} = 1$ . Its exponent is $- 2 (1)^{2} / 4 = - 1 / 2$ , giving $b_{1 / 2}^{\otimes 4} ({\hat{p}}_{4} \geq 3 / 4) \leq e^{- 1 / 2}$ . This comparison uses [A1]; the finite type and Sanov calculations in steps 1.1–3.1 are choice-free.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

52 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

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