Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generated
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.

Berger-Tung inner bound contains the Slepian-Wolf region

Example

For a finite IID k-source, take X^i=Xi and Hamming distortion at Di=0. Choosing Ui=Xi in the Berger-Tung test-channel construction makes its subset inequalities the Slepian-Wolf inequalities. This is a lossless special case where the inner bound matches the exact rate region; no such equality is asserted for general multiterminal lossy coding.

Facts & Assumptions

Given: A finite IID k-source, identity auxiliary channels Ui=Xi, and zero Hamming distortions.

[F1]

Finite-alphabet Berger-Tung multiterminal lossy inner bound: the finite test-channel subset constraints are ∑i∈SRi≥I(XS;US∣USc) for every nonempty S.

[F2]

Finite-IID k-source Slepian–Wolf rate region: the exact finite-IID lossless rate region is ∑i∈SRi≥H(XS∣XSc) for every nonempty S.

[F3]

Finite conditional mutual information identities and equality: I(A;B∣C)=H(A∣C)+H(B∣C)−H(A,B∣C) for finite variables.

[F4]

Finite conditional entropy: conditional entropy averages the entropies of the conditional laws over positive-mass conditioning values.

[F5]

Finite distributions, entropy, divergence, and stochastic matrices: H(p)=−∑xp(x)ln⁡p(x), with 0ln⁡0=0.

[F6]

Finite fixed-length multiterminal lossless code: separate finite-length encoders send indices to a common decoder, and achievable rates allow vanishing block-error probability.

Verification

1.1F1givenconstruct

With Ui=Xi, every Ui−Xi test channel is the identity and the product factorization is satisfied. The decoder sets X^i=Ui, so all Hamming distortions vanish. The subset right-hand side in [F1] becomes I(XS;XS∣XSc).

2.1F1F2F3F4F5F6step 1.1algebra∎

For each positive-mass value c of XSc, the conditional law of (XS,XS) has mass pXS∣c(x) at (x,x) and zero off the diagonal. Its entropy therefore equals that of XS given c by [F5]. Averaging over c using [F4] gives H(XS,XS∣XSc)=H(XS∣XSc), so [F3] yields I(XS;XS∣XSc)=2H(XS∣XSc)−H(XS,XS∣XSc)=H(XS∣XSc). This also covers S=[k], whose complement is a singleton. These are exactly the inequalities in [F2], under the lossless fixed-length common-decoder convention [F6]; lossless block-error achievability is supplied by [F2]. Therefore the Berger-Tung inner bound contains the exact Slepian-Wolf region for this zero-distortion special case, while its statement remains only an inner bound for general distortions.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 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