Broadcast channel — Marton's inner bound as a union over auxiliary alphabets #

martonRegion is the quadrilateral of one fixed pair of auxiliary alphabets, whereas the UV outer region is a union over five-tuple laws. This file takes the union on the inner side, so that the two regions can be compared as sets, and records what makes the result behave like an inner bound: it is a nonempty lower set, it is unchanged when the auxiliary alphabets are relabeled, and it therefore absorbs the quadrilateral of every pair of finite auxiliary alphabets.

Main definitions #

• bcAuxAlphabet k — the auxiliary alphabet of cardinality k + 1.
• martonRegionUnion W — Marton's inner bound, as the closure of the union of martonRegion over the auxiliary laws on those alphabets.
• martonRegionUnionFullSupport W — the same union restricted to the full-support indices, those whose auxiliary law and auxiliary kernel charge every point.

Main statements #

• martonRegionUnion_subset_uv — the union sits inside the UV outer region.
• martonRegion_subset_union — the union absorbs the quadrilateral of every pair of finite auxiliary alphabets, in every universe.
• martonRegionUnion_isLowerSet / martonRegionUnion_nonempty — the union is a nonempty lower set, as the UV outer region is.
• martonRegion_isLowerSet / martonRegion_convex / martonRegion_nonempty — a single quadrilateral is a nonempty convex lower set. Convexity is claimed of the quadrilaterals only, not of the union.
• martonRegion_map_relabel — the quadrilateral depends on the auxiliary alphabets only through the joint law, so a measurable bijection of either alphabet leaves it unchanged.

Implementation notes #

The auxiliaries range over ULift (Fin (k + 1)), one cardinality at a time, in the universe of the input alphabet: fixing the cardinality avoids quantifying over types, and the universe lift is what lets the comparison classes be applied at a member of the union. Relabeling invariance is what keeps that ladder lossless: an arbitrary pair of finite nonempty auxiliary alphabets is carried onto the rung of its own two cardinalities, so indexing the union by cardinalities rather than by types gives up nothing. A countable auxiliary alphabet is not available here, unlike on the outer side: the dependence between the two auxiliaries is the one information slot reading no output letter, so it is the one that can be infinite, and the toReal convention would then drop the sum-rate penalty.

Order, convexity and nonemptiness #

Relabeling the auxiliary alphabets #