Broadcast channel — the capacity region of a more capable channel #

IsBCMoreCapable compares the two marginal channels under every input law. The converse for a more capable channel needs that comparison in two further shapes: conditioned on an auxiliary variable, and read on a five-tuple law of the UV outer region. Both are averages of the unconditional statement over the conditional input laws, which is exactly what the mixture identity for conditional mutual information delivers, so the comparison transports with no new analysis.

What the comparison buys is the sum-rate inequality I(V; Y₁) + I(X; Y₂ ∣ V) ≤ I(X; Y₁), the fourth constraint of the UV outer region, which the less noisy converse discards and the more capable one needs. The companion bound at the receiver-2 corner, I(U; Y₂) ≤ I(X; Y₁), is the same comparison composed with the data processing inequality along U → X → Y₂; it is what the sum constraint degenerates to once the first rate is clamped at zero.

The right-hand side of both bounds is uvInfoJoint, the information the input carries about the first output. It is the slot of a five-tuple law that the two-constraint inner bound never needed, and this file records the fact the full-support step asks of it beyond its invariance under relabeling: it is concave in the law, so a positive multiple of it survives the mixture that repairs full support.

Keeping that slot is what lets the inner bound keep the sum-rate constraint a general broadcast channel needs, instead of the two-constraint region that is exact only over a less noisy one. Time sharing between a rate pair and the corner where the cloud auxiliary is constant meets the two separate constraints at once, and the sum constraint survives the segment because the input-output slot is the same at both of its endpoints; perturbing the achievability pair the segment lands on toward the uniform law then repairs its support, at a cost one weight covers for all three slots at once. Truncating the auxiliary of a law of the outer region moves that law onto a finite alphabet, and leaves the input-output slot alone as well, so both costs vanish along a single sequence of indices and the inner bound, being a closure, recovers the rate pair itself. Combined with the outer bound and with the achievability of the inner one, this describes the capacity region of a more capable broadcast channel by a single-letter expression. It subsumes the description of a less noisy one, IsBCLessNoisy being the stronger comparison.

The sum constraint is carried with the first rate clamped at zero, max R₁ 0 + R₂, which is the form the achievability theorem takes and the form under which the inner bound is achievable with no comparison between the two receivers. A negative first rate is then met at the receiver-2 corner rather than by the sum-rate slot of the outer region, which is where the second of the two comparison bounds is spent.

Main statements #

• IsBCMoreCapable.condMutualInfo_le — over a more capable channel, the receiver-2 information conditioned on the cloud auxiliary is at most the receiver-1 one.
• uvInfoSum₁_le_uvInfoJoint_of_moreCapable — over a more capable channel, the fourth UV outer slot of a channel law is at most I(X; Y₁).
• uvInfo₂_le_uvInfoJoint_of_moreCapable — over a more capable channel, the receiver-2 slot of a channel law is at most I(X; Y₁).
• mul_uvInfoJoint_le_uvInfoJoint_uvPerturbLaw — perturbing a law toward the uniform one with weight lam keeps at least the fraction lam of I(X; Y₁).
• bc_moreCapable_uv_subset_superposition — the UV outer region of a more capable channel is contained in the three-constraint superposition inner bound.
• bc_moreCapable_capacity_eq_uv — the single-letter characterization: the capacity region of a more capable broadcast channel whose transition law gives every output pair positive mass is its UV outer region bcOuterRegionUV.
• bc_degraded_capacity_eq_uv — the same characterization for a physically degraded channel, degradedness being the strongest of the three comparisons.
• bc_moreCapable_superposition_eq_capacity — the same capacity region read off the superposition inner bound instead of the outer bound.

Implementation notes #

Transporting the comparison means exchanging the measure inside an information, which rw cannot do: condMutualInfo takes the finiteness instance on its measure argument, so rewriting that argument leaves a motive that is not type correct. condMutualInfo_congr_measure performs the exchange by substitution instead, and mutualInfo_congr_pair is the coarser form, where the two ambient measures may differ as long as the joint law of the compared pair agrees. mutualInfo_compProd_out₁ and mutualInfo_compProd_out₂ read a marginal channel off a composition product, which is what puts the comparison in the mutualInfoOfChannel form IsBCMoreCapable is stated in.

The two marginal channels under a single input law #

The conditional form of the more capable comparison #

The Markov chain reaching the second receiver #

The more capable comparison on a channel law #

The input-output slot under mixing #

Repairing the support with the sum constraint #

The reverse inclusion #

The capacity region of a more capable channel #