LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-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-IID lossless source coding above entropy

Statement

Let $P_{S}$ be a probability vector on a finite nonempty alphabet $S$ , and define its entropy in nats by

$H (P_{S}) : = - \sum_{s : P_{S} (s) > 0} P_{S} (s) \ln P_{S} (s) .$

For every $R > H (P_{S})$ , there are deterministic fixed-length codes $f_{k} : S^{k} \to [M_{k}]$ , $g_{k} : [M_{k}] \to S^{k}$ for the IID source $P_{S}^{\otimes k}$ such that $\Pr [g_{k} (f_{k} (S^{k})) \neq S^{k}] \to 0$ and ${lim sup}_{k \to \infty} k^{- 1} \ln M_{k} < R$ .

Facts & Assumptions

Given: A finite nonempty alphabet $S$ , a probability vector $P_{S}$ , and a rate $R > H (P_{S})$ .

[A1]

The letters $S_{1}, S_{2}, \dots$ are IID with law $P_{S}$ ; $S^{k} = (S_{1}, \dots, S_{k})$ .

Proof

1.1A1givenchoosealgebra

Choose $δ$ with $0 < δ < R - H (P_{S})$ . On the support of $P_{S}$ , let $Z_{i} = - \ln P_{S} (S_{i})$ . This is a finite-valued IID sequence with mean $H (P_{S})$ and finite variance $σ^{2}$ . For ${\overline{Z}}_{k} = k^{- 1} \sum_{i = 1}^{k} Z_{i}$ , independence gives $E ({\overline{Z}}_{k} - H (P_{S}))^{2} = σ^{2} / k$ ; the pointwise bound $1_{{∣ {\overline{Z}}_{k} - H (P_{S}) ∣ \geq δ}} \leq ({\overline{Z}}_{k} - H (P_{S}))^{2} / δ^{2}$ therefore yields $\Pr [{\overline{Z}}_{k} > H (P_{S}) + δ] \leq σ^{2} / (k δ^{2}) \to 0$ .

2.1A1step 1.1algebra

Define $T_{k} : = {s^{k} : P_{S}^{\otimes k} (s^{k}) > 0, - k^{- 1} \ln P_{S}^{\otimes k} (s^{k}) \leq H (P_{S}) + δ}$ . By step 1.1, $P_{S}^{\otimes k} (T_{k}) \to 1$ . Every $s^{k} \in T_{k}$ has probability at least $e^{- k (H (P_{S}) + δ)}$ , so $∣ T_{k} ∣ e^{- k (H (P_{S}) + δ)} \leq \sum_{s^{k} \in T_{k}} P_{S}^{\otimes k} (s^{k}) \leq 1$ ; hence $∣ T_{k} ∣ \leq e^{k (H (P_{S}) + δ)}$ .

3.1A1step 2.1construct

Put $M_{k} = ⌈ e^{k (H (P_{S}) + δ)} ⌉$ and inject the finite set $T_{k}$ into $[M_{k}]$ . Encode each $s^{k} \in T_{k}$ by its assigned message and every other source word by message $1$ ; decode an assigned message to its unique word and unused messages to a fixed word of $S^{k}$ . This defines deterministic maps, and decoding is correct on $T_{k}$ , so the block-error probability is at most $P_{S}^{\otimes k} (T_{k}^{c}) \to 0$ .

4.1givenstep 3.1algebra∎

Since $⌈ e^{x} ⌉ \leq 2 e^{x}$ for $x \geq 0$ , $k^{- 1} \ln M_{k} \leq H (P_{S}) + δ + k^{- 1} \ln 2$ . Its limsup is at most $H (P_{S}) + δ < R$ , proving the rate claim.

Used by

Lossless separation for finite IID sources and finite DMCs Theorem

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources

Yury Polyanskiy, MIT OpenCourseWare 6.441 Information Theory, Chapter 20: Advanced Channel Coding and Source-Channel Separation (standard reference, not scraped)
Robert M. Gray, Entropy and Information Theory, author-hosted full text (standard reference, not scraped)