Broadcast channel — absorbing a time-sharing variable into the superposition cloud #

A point of the UV outer region is described by a five-tuple law, whose two information slots I(U; Y₂) and I(X; Y₁ ∣ U) are the corners of a rectangle the superposition inner bound only reaches after the rate pair has been traded along a segment. Time sharing performs that trade: the auxiliary is kept with probability lam and collapsed to a constant with probability 1 - lam, and both branches are carried by the single auxiliary Bool × U, whose first component records which branch was taken.

Because the tag is recoverable from the auxiliary, the mixture identities for the two slots are exact where they need to be. The receiver-2 corner only needs the branch that keeps the auxiliary, so the tag's own contribution is discarded and the slot is bounded below by lam * I(U; Y₂). The satellite slot is an equality, lam * I(X; Y₁ ∣ U) + (1 - lam) * I(X; Y₁), because collapsing the auxiliary turns the conditional information into the unconditional one. The second endpoint therefore contributes I(X; Y₁), and the segment traced by lam stays above the outer point as soon as the rate pair also satisfies max R₁ 0 + R₂ ≤ I(X; Y₁). That sum constraint is all the assembly asks for beyond the three outer inequalities, and it comes for free over a less noisy channel, which forces I(X; Y₁ ∣ U) + I(U; Y₂) ≤ I(X; Y₁) at every law.

Main definitions #

• uvCloudLaw ν and uvSatelliteKernel ν — the achievability pair read off a five-tuple law.
• uvTagTrue ν, uvTagFalse σ, uvMixKernel ν σ and uvMixLaw ν σ lam — two channel laws mixed along a Bernoulli tag carried by the auxiliary, each of them keeping its auxiliary under its own tag.
• uvCollapse ν u₀ and uvTagConst ν u₀ — the law with its auxiliary collapsed to the constant u₀, and its false-tagged copy.
• uvTimeShareLaw ν u₀ lam — the law and its own collapsed copy mixed with weight lam.
• boolProdAuxEquiv m — the tagged auxiliary alphabet re-encoded into Marton.bcAuxAlphabet.

Main statements #

• bcInfo₂_uvCloudLaw, bcInfo₁_uvCloudLaw and bcInfoJoint_uvCloudLaw — the three informations of the achievability pair read off a channel law are the corresponding slots of that law.
• mul_uvInfo₂_le_uvInfo₂_uvMixLaw and mul_condMutualInfo_le_condMutualInfo_uvMixLaw — the two slots of a mixture of two channel laws against the slots of the branch it keeps.
• mul_uvInfo₂_le_uvInfo₂_uvTimeShareLaw and condMutualInfo_uvTimeShareLaw — the two slots of the time-shared law against the slots of the original one.
• uvInfoJoint_uvTimeShareLaw — time sharing leaves the input-output information I(X; Y₁) unchanged.
• exists_bcInfo_ge_sumRate_of_isUVChannelLaw — a rate pair satisfying the three UV outer inequalities of a channel law together with the sum constraint max R₁ 0 + R₂ ≤ I(X; Y₁) is dominated by the three informations of some achievability pair, with no comparison between the two receivers.
• exists_bcInfo_ge_of_lessNoisy_of_isUVChannelLaw — over a less noisy channel, a rate pair satisfying the three UV outer inequalities of a channel law is dominated by the two informations of some achievability pair, the sum constraint coming for free from the comparison.

Implementation notes #

uvMixLaw mixes two arbitrary channel laws along the tag rather than a law and its own collapsed copy, because the same construction carries the perturbation toward the uniform law as well: forgetting the tag turns uvMixLaw ν (uvUniformLaw W v₀) lam into uvPerturbLaw W ν v₀ lam. Time sharing is the case where the second law is uvCollapse ν u₀, so uvTimeShareLaw is defined as that specialization and both mixtures share the lemmas about the tag.

Mixing two channel laws along a Bernoulli tag #

The mixture of two tagged laws #

Time sharing as the mixture with the collapsed law #

The information slots of a mixture and of the time-shared law #

The receiver-2 corner #

The satellite conditional information #

Reading an achievability pair off a channel law #

The cloud law and the satellite kernel #

The three informations of the achievability pair #

Landing in the auxiliary alphabet of the inner bound #

The input-output slot under time sharing #

Time sharing with the sum constraint #

The sum constraint over a less noisy channel #