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.
Fano bound for finite messages and density observations
Statement
Let be uniform on a finite message set of size , let take values in a finite set , and let take values in ; a complex observation space is identified with . Suppose has a Lebesgue density. For every measurable estimator with and error probability , define using its finite posterior vector. Then where and . For , the conditional entropy is zero.
Facts & Assumptions
Given: A finite uniform message, finite side information, conditional observation densities and a measurable estimator.
Finite KL divergence is nonnegative with equality exactly at equal laws: finite relative entropy is nonnegative; in particular a -point law has entropy at most by comparison with the uniform law.
Proof
If and is the conditional density of , then and whenever . This is a finite posterior probability vector, so [F1] makes its entropy well-defined and bounded by .
Put . For each fixed , is a function of ; expanding the finite entropy sum first over and then over gives .
Let . If , [F2] applied to the two-point laws and gives . Rearranging and averaging, using , yields . If or , then almost surely and both binary entropies are zero.
On , and so its conditional entropy is zero; on and fixed , at most message values remain, so [F2] bounds that entropy by . Therefore .
Averaging the identity of step 2.1 and applying steps 3.1 and 3.2 proves the sharp bound. Since and , the weaker displayed bound follows. If , is constant.
Depends on
Used by
- Genie-aided outer bounds for the two-user Gaussian interference channel Lemma
- Cut-dependent Gaussian multicast gap to the cut-set bound Theorem
- Exact strong-interference region for the two-user Gaussian interference channel Theorem
- No-feedback real AWGN MAC capacity region Theorem
- Ozarow capacity region of the two-user real AWGN MAC with feedback Theorem
Dependency tree · two levels
4 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, 2nd ed., Chapter 2, §2.10 (standard reference, not scraped)
- Amos Lapidoth, A Foundation in Digital Communication, Chapter 3, Fano's inequality (standard reference, not scraped)