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

Ideal-real arithmetic coding is within two bits per block

Statement

For an ideal-real arithmetic code of a length- $n$ block from source $p$ , $E [ℓ (X^{n})] \leq n H_{2} (p) + 2.$

Facts & Assumptions

Given: The product block law $p^{n}$ , the pointwise bound of the ideal-real interval theorem, and the entropy definition $H_{2} (p)$ .

[F1]

Ideal-real interval coding is prefix-free and lossless: $ℓ (x^{n}) \leq - \log_{2} p^{n} (x^{n}) + 2$ for every block.

[F2]

Finite discrete sources and product blocks: $p^{n} (x^{n}) = \prod_{t = 1}^{n} p_{x_{t}}$ .

[F3]

Base-two entropy of a finite source: $H_{2} (p) = - \sum_{i} p_{i} \log_{2} p_{i}$ .

[F4]

Information units and logarithm-base convention: $\log_{2} t = \ln t / \ln 2$ .

[F5]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: $\ln (x y) = \ln x + \ln y$ for positive $x, y$ .

Proof

1.1F1F2givenalgebra

Take the expectation of the pointwise inequality in [F1] under $p^{n}$ ; finite summation gives $E [ℓ (X^{n})] \leq E [- \log_{2} p^{n} (X^{n})] + 2$ .

2.1F2F3F4F5step 1.1algebra∎

By [F2], [F4], and [F5], $- \log_{2} p^{n} (X^{n}) = \sum_{t = 1}^{n} - \log_{2} p_{X_{t}}$ . For each coordinate $t$ , summing $p^{n}$ over blocks with $x_{t} = i$ gives $p_{i} (\sum_{j} p_{j})^{n - 1} = p_{i}$ , so $X_{t}$ has law $p$ . Linearity of the finite expectation and [F3] then give $E [- \log_{2} p^{n} (X^{n})] = \sum_{t = 1}^{n} H_{2} (p) = n H_{2} (p)$ . Substitute in step 1.1.

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

Scott D. Roweis, CSC310 Lecture 8x: Arithmetic Coding Without Blocks, version 1.1 (standard reference, not scraped)
Stanford EE376A, Information Theory Course Notes, Chapter 4: Lossless Compression (standard reference, not scraped)