Broadcast channel — the UV outer region as a subset of the plane #

The four information slots of the UV outer bound are functionals of a five-tuple law (U, V, X, Y₁, Y₂) and do not mention the channel. A region defined as the union of the resulting quadrilaterals over all five-tuple laws would therefore be the whole plane: a law that copies the input into the outputs makes every slot as large as the input alphabet allows, whatever the channel is. The union is therefore indexed by the laws whose output pair is generated from the input letter by the channel and by nothing else, which is one composition product identity, IsUVChannelLaw.

Main definitions #

• IsUVChannelLaw W ν — the conditional law of the output pair (Y₁, Y₂) given the two auxiliaries and the input letter (U, V, X) is W X. This says at once that the output law is the channel and that the auxiliaries reach the outputs only through the input letter.
• uvLawOfInput W ρ — the channel law generated by a law of the auxiliaries and the input letter.
• uvRegion ν — the quadrilateral cut out by the four information slots of a five-tuple law.
• bcOuterRegionUV W — the UV outer region: the closure of the union of uvRegion ν over the channel laws ν on a fixed pair of countable auxiliary alphabets.
• uvConstLaw W x₀ — the channel law with constant auxiliaries and constant input letter x₀, which witnesses that the union is indexed by a nonempty family.
• uvOutputCopiesInputLaw, uvAuxCopiesOutputLaw — two five-tuple laws that the channel constraint rejects, over the channels uvBlindChannel and uvFairBitChannel.

Main statements #

• bcOuterRegionUV_isClosed — the region is closed.
• bcOuterRegionUV_isLowerSet — the region is a lower set, so a rate pair below one of its points belongs to it as well.
• bcOuterRegionUV_nonempty — the region is nonempty, witnessed by uvConstLaw, so the union is indexed by a nonempty family of channel laws.
• isUVChannelLaw_iff — a law is a channel law exactly when it is a law of the auxiliaries and the input letter pushed through the channel, which describes the index of the union directly.
• IsUVChannelLaw.map_input_output — a channel law has the channel joint (ν.map X) ⊗ₘ W as its input-output pair law, which is the constraint a law copying the input letter into the outputs violates.
• IsUVChannelLaw.map_auxiliary_input_output — dropping the second auxiliary leaves the law of the first auxiliary, the input letter and the two outputs in the shape a superposition ensemble has: the law of the pair (U, X) pushed through the channel.
• IsUVChannelLaw.isMarkovChain_UV_X_Y — the two auxiliaries reach the output pair through the input letter only, with IsUVChannelLaw.isMarkovChain_U_X_Y₁ and IsUVChannelLaw.isMarkovChain_V_X_Y₁ reading one auxiliary and one output off it.
• not_isUVChannelLaw_uvOutputCopiesInputLaw and not_isUVChannelLaw_uvAuxCopiesOutputLaw — the constraint rejects two structurally different degenerate laws, one whose outputs copy the input letter and one whose auxiliary copies an output over a one-letter input alphabet.
• IsUVChannelLaw.smul, IsUVChannelLaw.add — mixtures of channel laws are channel laws, so averaging the letter laws of a code stays inside the index of the union.
• IsUVChannelLaw.map_auxiliaries — re-encoding the two auxiliary alphabets keeps a channel law a channel law, which is how a law on the auxiliaries of a code reaches the fixed ones.
• IsUVChannelLaw.swap_auxiliaries — exchanging the two auxiliaries keeps a channel law a channel law, so a law indexing them in the opposite order indexes the union too.

Implementation notes #

IsUVChannelLaw is one composition-product identity between two pushforwards of ν, rather than a conjunction of "the output pair is distributed by the channel" and "the auxiliaries are conditionally independent of the output pair given the input letter". A single identity is the shape the Measure.map and Measure.compProd lemmas consume, so the mixture, re-encoding and marginalization lemmas are each a rewrite chain; the first conjunct is recovered from it as IsUVChannelLaw.map_input_output, and the second is the statement that the conditional law is read at the input coordinate only.

uvLawOfInput is the construction appearing on the right of isUVChannelLaw_iff: together with uvLawOfInput_isUVChannelLaw it says that the channel laws are exactly the laws obtained by pushing a law of (U, V, X) through the channel, which is how a witness such as uvConstLaw is built and shown to index the union.

Both auxiliary alphabets of bcOuterRegionUV are fixed to ℕ instead of being quantified over countable types, so the union ranges over measures rather than over types. The closure is taken because a union of intersections of closed half-planes need not be closed, and because the operational region is itself a closure.

uvRegion imposes no sign constraint on the rate pair, matching the operational region, which contains nonpositive pairs; imposing one would exclude pairs the operational region contains. Both regions being lower sets is what carries the inclusion off the first quadrant, so no intersection with it is needed.

Channel laws of a five-tuple #

The constraint and its characterization #

Mixtures, re-encodings and marginals #

The Markov chains carried by a channel law #

The law generated by a law of the auxiliaries and the input #

The UV outer region #

The channel constraint is not vacuous #

The information slots do not mention the channel, so the constraint is what stops the union from exhausting the plane, and it has to reject two structurally different families of laws.

A law that copies the input letter into both outputs carries a full input alphabet of information in every slot no matter which channel indexes the region, and such laws exist over every alphabet, so the output law has to be pinned to the channel. uvOutputCopiesInputLaw copies a fair bit into both outputs and is rejected over the channel that always outputs (false, false).

Pinning the output law alone would still leave the auxiliaries free to read the outputs directly, which manufactures information about a receiver that the input letter does not carry. uvAuxCopiesOutputLaw lives over a one-letter input alphabet and has the channel joint as its input-output pair law, so it meets the first constraint, yet its first auxiliary is the output bit, and it is rejected as well.