Broadcast channel — from a block code to its ambient law #

The canonical ambient probability measure attached to a broadcast block code: a uniform message pair is passed through the per-letter product channel, and the messages and the two receiver outputs are read off the resulting measure as coordinate projections.

Read off that measure are the structural hypotheses of the message-level bound bc_uv_converse — memorylessness and the two Markov chains — together with the identification of the ambient decode error with the code's average error probability; instantiating bc_uv_converse there gives the headline bc_uv_converse_from_code. Two further sections re-encode the per-letter auxiliary variable onto a single alphabet, for an arbitrary ambient measure, and then read the letter-i five-tuple law off the ambient of a code and identify each summand of the bound with an information slot of that law.

Main definitions #

• bcConverseInput — the uniform law on the message pair.
• bcConverseKernel — the per-letter product channel ∏ᵢ W (encoder m i), as a kernel in the message pair.
• bcConverseAmbient — the ambient measure bcConverseInput ⊗ₘ bcConverseKernel.
• bcConverseMsg₁, bcConverseMsg₂ — the two message projections.
• bcConverseYs, bcConverseY₁s, bcConverseY₂s — the output-pair projection and its two per-receiver components.
• bcConverseCodeKernel — the codeword → output-block kernel.
• bcConverseFanoSlack₁, bcConverseFanoSlack₂ — the per-receiver Fano slack of the code.
• uvPadMap, uvUnpadMap — the re-encoding of the letter-i auxiliary alphabet into a fixed one, and its left inverse.
• uvAuxPad — the letter-i auxiliary variable read in that fixed alphabet.
• uvInfo₁, uvInfo₂, uvInfoSum₂, uvInfoSum₁ — the four information slots of the outer bound, as functionals of a five-tuple law (U, V, X, Y₁, Y₂). The subscript of a sum-rate slot names the corner slot it extends, so uvInfoSum₂ leads with uvInfo₂ and uvInfoSum₁ with uvInfo₁.
• uvInfoJoint — the input-output information I(X; Y₁) of the same law. It is not a slot of the outer bound; it is the common upper bound the two comparison bounds of a more capable channel take.
• bcUVTuple — the letter-i five-tuple of the two padded auxiliaries, the input letter and the two output letters.
• bcUVJointDistribution — the law of that five-tuple under the ambient.

Main statements #

• bcConverseKernel_apply — the kernel at a message pair is the code's block output law.
• bcConverseMsg₁_uniform, bcConverseMsg₂_uniform — each message is uniform under the ambient.
• bcConverse_mutualInfo_eq_zero — the two messages are independent under the ambient.
• bcConverse_memoryless₁, bcConverse_memoryless₂ — each output letter is conditionally independent of the other message, the other input letters and all other output letters, given the current input letter. The two same-letter outputs are never decoupled from each other.
• bcConverse_isMarkovChain₁, bcConverse_isMarkovChain₂ — the messages act on a receiver's output block only through the codeword: (W₂, W₁) → (W₂, Xⁿ) → Y₁ⁿ and its mirror.
• bcConverse_errorProb₁_eq, bcConverse_errorProb₂_eq — the ambient decode error at a receiver is the code's average error probability there.
• bc_uv_converse_from_code — the UV outer bound at a bare broadcast code, with the rate pair (log M₁, log M₂) and the Fano slack still symbolic.
• mutualInfo_pair_out₁_eq_uvInfoJoint — pairing the input letter with an auxiliary variable that acts on the first output only through that letter adds nothing: the pair carries exactly uvInfoJoint. This is what identifies the input-output slot of a law with the corresponding information of the achievability pair read off it.
• uvAux_pad_mutualInfo_eq, uvAux_pad_condMutualInfo_eq — re-encoding the auxiliary variable into the fixed alphabet changes neither the mutual information it carries about an output nor the conditional mutual information it conditions.
• bc_uv_mutualInfo_eq_uvInfo₁_at, bc_uv_mutualInfo_eq_uvInfo₂_at, bc_uv_sum_eq_uvInfoSum₂_at, bc_uv_sum_eq_uvInfoSum₁_at — each summand of the four information slots of the code-level bound is the corresponding information slot of the letter's five-tuple law, so the n-letter bound is a sum of single-letter quantities.

Implementation notes #

The output block lives on Fin n → β₁ × β₂, a sequence of output pairs, rather than on a pair of sequences. With that choice the message-to-output kernel is literally BroadcastCode.blockOutputLaw, so the product structure over letters is available to the structural lemmas and the same-letter pair (Y_{1,i}, Y_{2,i}) is never split; the two per-receiver output sequences are recovered as further projections.

The alphabet of uvAux … i depends on the letter i, so different letters produce auxiliary variables of different types. uvAuxPad moves all of them onto one alphabet by padding the prefix and the suffix with a default value and keeping i as a first component; keeping i is what makes the padding invertible, and invertibility is what turns the data processing inequality into an equality of informations.

Together with the uniformity and independence statements the four structural lemmas discharge the structural preconditions of the message-level converse bc_uv_converse. The encoder is measurable for free because the message pair ranges over a finite type, so the only hypotheses bc_uv_converse_from_code keeps are 2 ≤ M₁ and 2 ≤ M₂.

The five-tuple carries both auxiliaries, because the four information slots split two and two between them; keeping them in one law is what lets a single distribution witness all four inequalities. uvInfoSum₂ and uvInfoSum₁ take [IsFiniteMeasure ν] since condMutualInfo does, while the two corner slots need nothing beyond measurability. The four are declared in the field order of InBCOuterRegionUV (bound₁, bound₂, sumBound₂, sumBound₁) rather than by subscript, so that an instantiation reads down the structure. uvInfoJoint comes after them because it mentions neither auxiliary and so answers to no field of that structure.

The ambient measure of a broadcast code #

The input law, the channel kernel and the ambient #

Projections #

Uniformity and independence of the messages #

The codeword kernel #

Structural hypotheses of the message-level converse #

Code-level converse and rate extraction #

Fixed-alphabet form of the auxiliary variable #

Per-letter joint law and its information slots #

The information slots of a five-tuple law #

The per-letter law read off the ambient #